let m be odd Nat; :: thesis: for k being Nat st m divides 2 |^ k holds
m = 1
let k be Nat; :: thesis: ( m divides 2 |^ k implies m = 1 )
assume A1: m divides 2 |^ k ; :: thesis: m = 1
A2: 2 is Prime by INT_2:28;
assume m <> 1 ; :: thesis: contradiction
then not m is trivial by NAT_2:28;
then 2 divides m by A1, A2, NEWTON03:47;
hence contradiction ; :: thesis: verum