let X be BCI-algebra; :: thesis: for x being Element of X
for m, n 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 m, n being Nat st x is finite-period & ord x = n holds
( x |^ m in BCK-part X iff n divides m )
let m, n be Nat; :: thesis: ( x is finite-period & ord x = n implies ( x |^ m in BCK-part X iff n divides m ) )
reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34;
reconsider bn = b |^ n as Element of AtomSet X by Th13;
assume that
A1: x is finite-period and
A2: ord x = n ; :: thesis: ( x |^ m in BCK-part X iff n divides m )
A3: b is finite-period by A1, Th25;
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 );
A4: 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 A5: for k being Nat st k < m holds
S₁[k] ; :: thesis: S₁[m]
assume A6: 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:12; :: thesis: verum

end;

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

reconsider mm = m as Element of NAT by ORDINAL1:def 12;
x |^ mm in BCK-part X by A6;
then n <= m by A1, A2, A7, Def5;
then consider k being Nat such that
A8: m = n + k by NAT_1:10;
reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34;
A9: b is finite-period by A1, Th25;
b \ x = 0. X by BCIALG_1:1;
then b <= x ;
then x in BranchV b ;
then n = ord b by A1, A2, A9, Th28;
then b |^ n in BCK-part X by A9, Def5;
then ex z being Element of X st
( z = b |^ n & 0. X <= z ) ;
then A10: (b |^ n) ` = 0. X ;
ex zz being Element of X st
( zz = x |^ m & 0. X <= zz ) by A6;
then (x |^ m) ` = 0. X ;
then (b |^ (n + k)) ` = 0. X by A8, Th21;
then ((b |^ n) \ ((b |^ k) `)) ` = 0. X by Th24;
then (((b |^ k) `) `) ` = 0. X by A10, BCIALG_1:9;
then (b |^ k) ` = 0. X by BCIALG_1:8;
then (x |^ k) ` = 0. X by Th21;
then 0. X <= x |^ k ;
then A11: x |^ k in BCK-part X ;
n <> 0 by A1, A2, Def5;
then n divides k by A5, A8, A11, NAT_1:16;
then consider i being Nat such that
A12: k = n * i by NAT_D:def 3;
m = n * (1 + i) by A8, A12;
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(A4);
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
A13: m = n * i by NAT_D:def 3;
b \ x = 0. X by BCIALG_1:1;
then b <= x ;
then x in BranchV b ;
then n = ord b by A1, A2, A3, Th28;
then b |^ n in BCK-part X by A3, Def5;
then ex z being Element of X st
( z = b |^ n & 0. X <= z ) ;
then A14: (b |^ n) ` = 0. X ;
(b |^ m) ` = (bn |^ i) ` by A13, Th23;
then (b |^ m) ` = (0. X) |^ i by A14, Th17;
then (b |^ m) ` = 0. X by Th7;
then (x |^ m) ` = 0. X by Th21;
then 0. X <= x |^ m ;
hence x |^ m in BCK-part X ; :: thesis: verum