let n be non zero Integer; :: thesis: ex k being Nat ex j being odd Integer st n = j * (2 |^ k)

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

suppose n > 0 ; :: thesis: ex k being Nat ex j being odd Integer st n = j * (2 |^ k)

then n in NAT by INT_1:3;
then consider k being Nat, j being odd Nat such that
A1: n = j * (2 |^ k) by NAT_6:3;
take k ; :: thesis: ex j being odd Integer st n = j * (2 |^ k)
take j ; :: thesis: n = j * (2 |^ k)
thus n = j * (2 |^ k) by A1; :: thesis: verum

end;

suppose n < 0 ; :: thesis: ex k being Nat ex j being odd Integer st n = j * (2 |^ k)

then - n in NAT by INT_1:3;
then consider k being Nat, j being odd Nat such that
A2: - n = j * (2 |^ k) by NAT_6:3;
take k ; :: thesis: ex j being odd Integer st n = j * (2 |^ k)
take - j ; :: thesis: n = (- j) * (2 |^ k)
thus n = (- j) * (2 |^ k) by A2; :: thesis: verum

end;

end;