let n be natural odd Integer; :: thesis: for k being Nat st n divides 2 |^ k holds
n = 1
let k be Nat; :: thesis: ( n divides 2 |^ k implies n = 1 )
assume A0: n divides 2 |^ k ; :: thesis: n = 1
assume AA: n <> 1 ; :: thesis: contradiction

per cases ( n >= 0 or n < 0 ) ;

suppose n >= 0 ; :: thesis: contradiction

A3: n in NAT by INT_1:3;
2 is Prime by XPRIMES1:2;
then consider r being Nat such that
A4: ( n = 2 |^ r & r <= k ) by A0, A3, GROUPP_1:2;
r = 0 by A4;
hence contradiction by AA, A4, NEWTON:4; :: thesis: verum

end;

suppose n < 0 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

end;