let G be strict Group; :: thesis: for b being Element of G holds
( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
let b be Element of G; :: thesis: ( b is being_of_order_0 iff for n being Integer st b |^ n = 1_ G holds
n = 0 )
thus ( b is being_of_order_0 implies for n being Integer st b |^ n = 1_ G holds
n = 0 ) :: thesis: ( ( for n being Integer st b |^ n = 1_ G holds
n = 0 ) implies b is being_of_order_0 )

proof

assume A1: b is being_of_order_0 ; :: thesis: for n being Integer st b |^ n = 1_ G holds
n = 0
A2: for m being Nat st b |^ (- m) = 1_ G holds
m = 0

proof

let m be Nat; :: thesis: ( b |^ (- m) = 1_ G implies m = 0 )
assume A3: b |^ (- m) = 1_ G ; :: thesis: m = 0
b |^ (- m) = (b |^ m) " by GROUP_1:36;
then A4: (b ") |^ m = 1_ G by A3, GROUP_1:37;
b " is being_of_order_0 by A1, Th12;
hence m = 0 by A4, GROUP_1:def 10; :: thesis: verum

end;

for n being Integer st b |^ n = 1_ G holds
n = 0

proof

let n be Integer; :: thesis: ( b |^ n = 1_ G implies n = 0 )
assume A5: b |^ n = 1_ G ; :: thesis: n = 0
consider k being Nat such that
A6: ( n = k or n = - k ) by INT_1:2;

per cases ( n = k or n = - k ) by A6;

suppose n = k ; :: thesis: n = 0

hence n = 0 by A1, A5, GROUP_1:def 10; :: thesis: verum

end;

suppose A7: n = - k ; :: thesis: n = 0

then k = 0 by A2, A5;
hence n = 0 by A7; :: thesis: verum

end;

end;

end;

hence for n being Integer st b |^ n = 1_ G holds
n = 0 ; :: thesis: verum

end;

assume for n being Integer st b |^ n = 1_ G holds
n = 0 ; :: thesis: b is being_of_order_0
then for n being Nat st b |^ n = 1_ G holds
n = 0 ;
hence b is being_of_order_0 by GROUP_1:def 10; :: thesis: verum