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 that
A1: x is finite-period and
A2: x |^ m is finite-period and
A3: ord x = n and
A4: m > 0 ; :: thesis: ord (x |^ m) = n div (m gcd n)
reconsider b = (x `) ` as Element of AtomSet X by BCIALG_1:34;
A5: b is finite-period by A1, Th25;
b \ x = 0. X by BCIALG_1:1;
then b <= x ;
then x in BranchV b ;
then A6: n = ord b by A1, A3, A5, Th28;
then b |^ n in BCK-part X by A5, Def5;
then A7: ex z being Element of X st
( z = b |^ n & 0. X <= z ) ;
reconsider mgn = m gcd n as Element of NAT ;
m gcd n divides n by INT_2:21;
then consider vn being Nat such that
A8: n = mgn * vn by NAT_D:def 3;
reconsider vn = vn as Element of NAT by ORDINAL1:def 12;
m gcd n divides m by INT_2:21;
then consider i being Nat such that
A9: m = mgn * i by NAT_D:def 3;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A10: n = (mgn * vn) + 0 by A8;
A11: vn,i are_coprime

proof

i gcd vn divides i by NAT_D:def 5;
then consider b2 being Nat such that
A12: i = (i gcd vn) * b2 by NAT_D:def 3;
m = ((m gcd n) * (i gcd vn)) * b2 by A9, A12;
then A13: (m gcd n) * (i gcd vn) divides m by NAT_D:def 3;
i gcd vn divides vn by NAT_D:def 5;
then consider b1 being Nat such that
A14: vn = (i gcd vn) * b1 by NAT_D:def 3;
n = ((m gcd n) * (i gcd vn)) * b1 by A8, A14;
then (m gcd n) * (i gcd vn) divides n by NAT_D:def 3;
then (m gcd n) * (i gcd vn) divides m gcd n by A13, NAT_D:def 5;
then consider c being Nat such that
A15: m gcd n = ((m gcd n) * (i gcd vn)) * c by NAT_D:def 3;
A16: m gcd n <> 0 by A4, INT_2:5;
(m gcd n) * 1 = (m gcd n) * ((i gcd vn) * c) by A15;
then 1 = i gcd vn by A16, NAT_1:15, XCMPLX_1:5;
hence vn,i are_coprime by INT_2:def 3; :: thesis: verum

end;

A17: 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 that
A18: (x |^ m) |^ mm in BCK-part X and
A19: mm <> 0 ; :: thesis: vn <= mm
ex z being Element of X st
( z = (x |^ m) |^ mm & 0. X <= z ) by A18;
then ((x |^ m) |^ mm) ` = 0. X ;
then ((x |^ m) `) |^ mm = 0. X by Th18;
then ((b |^ m) `) |^ mm = 0. X by Th21;
then ((b |^ m) |^ mm) ` = 0. X by Th18;
then (b |^ (m * mm)) ` = 0. X by Th23;
then 0. X <= b |^ (m * mm) ;
then b |^ (m * mm) in BCK-part X ;
then mgn * vn divides (mgn * i) * mm by A8, A9, A5, A6, Th29;
then consider c being Nat such that
A20: (mgn * i) * mm = (mgn * vn) * c by NAT_D:def 3;
A21: mgn <> 0 by A4, INT_2:5;
mgn * (i * mm) = mgn * (vn * c) by A20;
then i * mm = vn * c by A21, XCMPLX_1:5;
then vn divides i * mm by NAT_D:def 3;
then vn divides mm by A11, INT_2:25;
then consider cc being Nat such that
A22: mm = vn * cc by NAT_D:def 3;
cc <> 0 by A19, A22;
hence vn <= mm by A22, NAT_1:24; :: thesis: verum

end;

((x |^ m) |^ vn) ` = ((x |^ m) `) |^ vn by Th18
.= ((b |^ m) `) |^ vn by Th21
.= ((b |^ m) |^ vn) ` by Th18
.= (b |^ ((mgn * i) * vn)) ` by A9, Th23
.= (b |^ (n * i)) ` by A8
.= ((b |^ n) |^ i) ` by Th23
.= ((b |^ n) `) |^ i by Th18
.= (0. X) |^ i by A7
.= 0. X by Th7 ;
then 0. X <= (x |^ m) |^ vn ;
then A23: (x |^ m) |^ vn in BCK-part X ;
n gcd m > 0 by A4, NEWTON:58;
then A24: n div mgn = vn by A10, NAT_D:def 1;
vn <> 0 by A1, A3, A8, Def5;
hence ord (x |^ m) = n div (m gcd n) by A2, A24, A23, A17, Def5; :: thesis: verum