let n be Nat; :: thesis: ( 2 divides (2 |^ n) - 1 iff n = 0 )

L1: ( 2 divides (2 |^ n) - 1 implies n = 0 )

hence ( 2 divides (2 |^ n) - 1 iff n = 0 ) by INT_2:12, L1; :: thesis: verum

L1: ( 2 divides (2 |^ n) - 1 implies n = 0 )

proof

( n = 0 implies (2 |^ n) - 1 = 1 - 1 )
by NEWTON:4;
assume A1:
( 2 divides (2 |^ n) - 1 & not n = 0 )
; :: thesis: contradiction

then ( 2 divides 2 |^ n & not 2 divides - 1 ) by NAT_3:3, INT_2:13;

hence contradiction by A1; :: thesis: verum

end;then ( 2 divides 2 |^ n & not 2 divides - 1 ) by NAT_3:3, INT_2:13;

hence contradiction by A1; :: thesis: verum

hence ( 2 divides (2 |^ n) - 1 iff n = 0 ) by INT_2:12, L1; :: thesis: verum