let G be Group; :: thesis: for a being Element of G
for i being Integer st not a is being_of_order_0 holds
ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
let a be Element of G; :: thesis: for i being Integer st not a is being_of_order_0 holds
ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
let i be Integer; :: thesis: ( not a is being_of_order_0 implies ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i ) )
assume not a is being_of_order_0 ; :: thesis: ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
then ord a <> 0 by GROUP_1:def 11;
then A1: |.i.| <= |.i.| * (ord a) by NAT_1:14, XREAL_1:151;
0 <= (|.i.| * (ord a)) + i
proof
per cases ( i < 0 or 0 <= i ) ;
suppose A2: i < 0 ; :: thesis: 0 <= (|.i.| * (ord a)) + i
A3: |.i.| + i <= (|.i.| * (ord a)) + i by A1, XREAL_1:6;
|.i.| = - i by A2, ABSVALUE:def 1;
hence 0 <= (|.i.| * (ord a)) + i by A3; :: thesis: verum
end;
suppose 0 <= i ; :: thesis: 0 <= (|.i.| * (ord a)) + i
hence 0 <= (|.i.| * (ord a)) + i ; :: thesis: verum
end;
end;
end;
then A4: (|.i.| * (ord a)) + i is Element of NAT by INT_1:3;
a |^ ((|.i.| * (ord a)) + i) = (a |^ (|.i.| * (ord a))) * (a |^ i) by GROUP_1:33
.= ((a |^ (ord a)) |^ |.i.|) * (a |^ i) by GROUP_1:35
.= ((1_ G) |^ |.i.|) * (a |^ i) by GROUP_1:41
.= (1_ G) * (a |^ i) by GROUP_1:31
.= a |^ i by GROUP_1:def 4 ;
hence ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i ) by A4; :: thesis: verum