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

proof

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;

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