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;
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