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 )
;

end;

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;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

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

defpred S_{1}[ Nat] means 2 |^ $1 divides n;

then A3: ex m being Nat st S_{1}[m]
by A1;

consider k being Nat such that

A4: ( S_{1}[k] & ( for n being Nat st S_{1}[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;

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;A2: now :: thesis: for m being Nat st S_{1}[m] holds

m <= n

2 |^ 1 = 2
;m <= n

let m be Nat; :: thesis: ( S_{1}[m] implies m <= n )

A3: 2 |^ m > m by NEWTON:86;

assume S_{1}[m]
; :: thesis: m <= n

then 2 |^ m <= n by INT_2:27;

hence m <= n by A3, XXREAL_0:2; :: thesis: verum

end;A3: 2 |^ m > m by NEWTON:86;

assume S

then 2 |^ m <= n by INT_2:27;

hence m <= n by A3, XXREAL_0:2; :: thesis: verum

then A3: ex m being Nat st S

consider k being Nat such that

A4: ( S

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

then reconsider l = l as natural odd number by A6;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 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

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