let X be BCI-algebra; :: thesis: for x being Element of X
for m, n being Nat st x is finite-period & x |^ m is finite-period & ord x = n & m > 0 holds
ord (x |^ m) = n div (m gcd n)
let x be Element of X; :: thesis: for m, n being Nat st x is finite-period & x |^ m is finite-period & ord x = n & m > 0 holds
ord (x |^ m) = n div (m gcd n)
let m, n be Nat; :: thesis: ( x is finite-period & x |^ m is finite-period & ord x = n & m > 0 implies ord (x |^ m) = n div (m gcd n) )
assume A1: ( x is finite-period & x |^ m is finite-period & ord x = n & m > 0 ) ; :: thesis: ord (x |^ m) = n div (m gcd n)
Aa: m gcd n divides n by INT_2:32;
A4: n gcd m > 0 by A1, NEWTON:71;
reconsider mgn = m gcd n as Element of NAT ;
consider vn being Nat such that
A5: n = mgn * vn by Aa, NAT_D:def 3;
reconsider vn = vn as Element of NAT by ORDINAL1:def 13;
m gcd n divides m by INT_2:31;
then consider i being Nat such that
A6: m = mgn * i by NAT_D:def 3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
n = (mgn * vn) + 0 by A5;
then A9: n div mgn = vn by A4, NAT_D:def 1;
A13: vn,i are_relative_prime

proof

i gcd vn divides vn by NAT_D:def 5;
then consider b1 being Nat such that
B1: vn = (i gcd vn) * b1 by NAT_D:def 3;
i gcd vn divides i by NAT_D:def 5;
then consider b2 being Nat such that
B3: i = (i gcd vn) * b2 by NAT_D:def 3;
B5: n = ((m gcd n) * (i gcd vn)) * b1 by A5, B1;
m = ((m gcd n) * (i gcd vn)) * b2 by A6, B3;
then ( (m gcd n) * (i gcd vn) divides n & (m gcd n) * (i gcd vn) divides m ) by B5, NAT_D:def 3;
then (m gcd n) * (i gcd vn) divides m gcd n by NAT_D:def 5;
then consider c being Nat such that
B7: m gcd n = ((m gcd n) * (i gcd vn)) * c by NAT_D:def 3;
B9: (m gcd n) * 1 = (m gcd n) * ((i gcd vn) * c) by B7;
m gcd n <> 0 by A1, INT_2:35;
then 1 = i gcd vn by B9, NAT_1:15, XCMPLX_1:5;
hence vn,i are_relative_prime by INT_2:def 4; :: thesis: verum

end;

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 C12: 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 ) ;
A12: (x |^ m) |^ vn in BCK-part X

proof

((x |^ m) |^ vn) ` = ((x |^ m) ` ) |^ vn by Th17b
.= ((b |^ m) ` ) |^ vn by Th19
.= ((b |^ m) |^ vn) ` by Th17b
.= (b |^ ((mgn * i) * vn)) ` by A6, Th21
.= (b |^ (n * i)) ` by A5
.= ((b |^ n) |^ i) ` by Th21
.= ((b |^ n) ` ) |^ i by Th17b
.= (0. X) |^ i by C13, BCIALG_1:def 11
.= 0. X by Th6 ;
then 0. X <= (x |^ m) |^ vn by BCIALG_1:def 11;
hence (x |^ m) |^ vn in BCK-part X ; :: thesis: verum

end;

A11: for mm being Element of NAT st (x |^ m) |^ mm in BCK-part X & mm <> 0 holds
vn <= mm

proof

let mm be Element of NAT ; :: thesis: ( (x |^ m) |^ mm in BCK-part X & mm <> 0 implies vn <= mm )
assume D1: ( (x |^ m) |^ mm in BCK-part X & mm <> 0 ) ; :: thesis: vn <= mm
then consider z being Element of X such that
D3: ( z = (x |^ m) |^ mm & 0. X <= z ) ;
((x |^ m) |^ mm) ` = 0. X by D3, BCIALG_1:def 11;
then ((x |^ m) ` ) |^ mm = 0. X by Th17b;
then ((b |^ m) ` ) |^ mm = 0. X by Th19;
then ((b |^ m) |^ mm) ` = 0. X by Th17b;
then (b |^ (m * mm)) ` = 0. X by Th21;
then 0. X <= b |^ (m * mm) by BCIALG_1:def 11;
then b |^ (m * mm) in BCK-part X ;
then mgn * vn divides (mgn * i) * mm by A5, A6, C12, Th26, C8;
then consider c being Nat such that
D5: (mgn * i) * mm = (mgn * vn) * c by NAT_D:def 3;
D6: mgn * (i * mm) = mgn * (vn * c) by D5;
mgn <> 0 by A1, INT_2:35;
then i * mm = vn * c by D6, XCMPLX_1:5;
then vn divides i * mm by NAT_D:def 3;
then vn divides mm by A13, INT_2:40;
then consider cc being Nat such that
D7: mm = vn * cc by NAT_D:def 3;
cc <> 0 by D1, D7;
hence vn <= mm by D7, NAT_1:24; :: thesis: verum

end;

vn <> 0 by A5, A1, Def8a;
hence ord (x |^ m) = n div (m gcd n) by A9, A12, Def8a, A1, A11; :: thesis: verum