let n be natural non zero number ; :: thesis: ex k being natural number ex l being natural odd number st n = l * (2 |^ k)

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: ex k being natural number ex l being natural odd number st n = l * (2 |^ k)

then reconsider l = n as natural odd number ;
take k = 0 ; :: thesis: ex l being natural odd number st n = l * (2 |^ k)
take l ; :: thesis: n = l * (2 |^ k)
thus l * (2 |^ k) = l * 1 by NEWTON:4
.= n ; :: thesis: verum

end;

suppose A1: n is even ; :: thesis: ex k being natural number ex l being natural odd number st n = l * (2 |^ k)

defpred S₁[ Nat] means 2 |^ $1 divides n;

A2: now :: thesis: for m being Nat st S₁[m] holds
m <= n

let m be Nat; :: thesis: ( S₁[m] implies m <= n )
A3: 2 |^ m > m by NEWTON:86;
assume S₁[m] ; :: thesis: m <= n
then 2 |^ m <= n by INT_2:27;
hence m <= n by A3, XXREAL_0:2; :: thesis: verum

end;

2 |^ 1 = 2 ;
then A3: ex m being Nat st S₁[m] by A1;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A2, A3);
consider l being Integer such that
A5: n = (2 |^ k) * l by A4, INT_1:def 3;
l >= 0 by A5;
then A6: l in NAT by INT_1:3;

now :: thesis: not l is even

assume l is even ; :: thesis: contradiction
then consider u being Integer such that
A7: l = 2 * u by INT_1:def 3;
n = ((2 |^ k) * 2) * u by A5, A7
.= (2 |^ (k + 1)) * u by NEWTON:6 ;
then 2 |^ (k + 1) divides n ;
hence contradiction by A4, NAT_1:16; :: thesis: verum

end;

then reconsider l = l as natural odd number by A6;
take k ; :: thesis: ex l being natural odd number st n = l * (2 |^ k)
take l ; :: thesis: n = l * (2 |^ k)
thus n = l * (2 |^ k) by A5; :: thesis: verum

end;

end;