let X be BCI-algebra; :: thesis: for x being Element of X
for n, m being Nat st x is finite-period & ord x = n holds
( x |^ m in BCK-part X iff n divides m )
let x be Element of X; :: thesis: for n, m being Nat st x is finite-period & ord x = n holds
( x |^ m in BCK-part X iff n divides m )
let n, m be Nat; :: thesis: ( x is finite-period & ord x = n implies ( x |^ m in BCK-part X iff n divides m ) )
assume A1: ( x is finite-period & ord x = n ) ; :: thesis: ( x |^ m in BCK-part X iff n divides m )
thus ( x |^ m in BCK-part X implies n divides m ) :: thesis: ( n divides m implies x |^ m in BCK-part X )

proof

defpred S₁[ Nat] means ( x |^ $1 in BCK-part X implies n divides $1 );
C1: for m being Nat st ( for k being Nat st k < m holds
S₁[k] ) holds
S₁[m]

proof

let m be Nat; :: thesis: ( ( for k being Nat st k < m holds
S₁[k] ) implies S₁[m] )
assume C2: for k being Nat st k < m holds
S₁[k] ; :: thesis: S₁[m]
assume C3: x |^ m in BCK-part X ; :: thesis: n divides m

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: n divides m

hence n divides m by INT_2:16; :: thesis: verum

end;

suppose C4: m <> 0 ; :: thesis: n divides m

reconsider mm = m as Element of NAT by ORDINAL1:def 13;
( m <> 0 & x |^ mm in BCK-part X ) by C3, C4;
then n <= m by Def8a, A1;
then consider k being Nat such that
C6: m = n + k by NAT_1:10;
reconsider b = (x ` ) ` as Element of AtomSet X by BCIALG_1:34;
C8: b is finite-period by Thx22, A1;
b \ x = 0. X by BCIALG_1:1;
then b <= x by BCIALG_1:def 11;
then x in BranchV b ;
then n = ord b by Th25, C8, A1;
then b |^ n in BCK-part X by Def8a, C8;
then consider z being Element of X such that
C13: ( z = b |^ n & 0. X <= z ) ;
C15: (b |^ n) ` = 0. X by C13, BCIALG_1:def 11;
reconsider a = b |^ m as Element of AtomSet X by Th12;
consider zz being Element of X such that
C17: ( zz = x |^ m & 0. X <= zz ) by C3;
(x |^ m) ` = 0. X by C17, BCIALG_1:def 11;
then (b |^ (n + k)) ` = 0. X by C6, Th19;
then ((b |^ n) \ ((b |^ k) ` )) ` = 0. X by Th22;
then (((b |^ k) ` ) ` ) ` = 0. X by C15, BCIALG_1:9;
then (b |^ k) ` = 0. X by BCIALG_1:8;
then (x |^ k) ` = 0. X by Th19;
then 0. X <= x |^ k by BCIALG_1:def 11;
then DD: x |^ k in BCK-part X ;
n <> 0 by Def8a, A1;
then n divides k by C2, DD, C6, NAT_1:16;
then consider i being Nat such that
C8: k = n * i by NAT_D:def 3;
m = n * (1 + i) by C6, C8;
hence n divides m by NAT_D:def 3; :: thesis: verum

end;

end;

end;

for m being Nat holds S₁[m] from NAT_1:sch 4(C1);
hence ( x |^ m in BCK-part X implies n divides m ) ; :: thesis: verum

end;

assume n divides m ; :: thesis: x |^ m in BCK-part X
then consider i being Nat such that
D3: m = n * i by NAT_D:def 3;
reconsider b = (x ` ) ` as Element of AtomSet X by BCIALG_1:34;
D5: b is finite-period by Thx22, A1;
b \ x = 0. X by BCIALG_1:1;
then b <= x by BCIALG_1:def 11;
then x in BranchV b ;
then n = ord b by Th25, D5, A1;
then b |^ n in BCK-part X by Def8a, D5;
then consider z being Element of X such that
D13: ( z = b |^ n & 0. X <= z ) ;
D15: (b |^ n) ` = 0. X by D13, BCIALG_1:def 11;
reconsider bn = b |^ n as Element of AtomSet X by Th12;
(b |^ m) ` = (bn |^ i) ` by Th21, D3;
then (b |^ m) ` = (0. X) |^ i by D15, Th17;
then (b |^ m) ` = 0. X by Th6;
then (x |^ m) ` = 0. X by Th19;
then 0. X <= x |^ m by BCIALG_1:def 11;
hence x |^ m in BCK-part X ; :: thesis: verum