let n0 be non zero Nat; :: thesis: ( n0 is even implies ex k, m being Nat st

( m is odd & k > 0 & n0 = (2 |^ k) * m ) )

assume A1: n0 is even ; :: thesis: ex k, m being Nat st

( m is odd & k > 0 & n0 = (2 |^ k) * m )

set k = 2 |-count n0;

2 |^ (2 |-count n0) divides n0 by NAT_3:def 7;

then consider m being Nat such that

A2: n0 = (2 |^ (2 |-count n0)) * m by NAT_D:def 3;

take 2 |-count n0 ; :: thesis: ex m being Nat st

( m is odd & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )

take m ; :: thesis: ( m is odd & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )

thus n0 = (2 |^ (2 |-count n0)) * m by A2; :: thesis: verum

( m is odd & k > 0 & n0 = (2 |^ k) * m ) )

assume A1: n0 is even ; :: thesis: ex k, m being Nat st

( m is odd & k > 0 & n0 = (2 |^ k) * m )

set k = 2 |-count n0;

2 |^ (2 |-count n0) divides n0 by NAT_3:def 7;

then consider m being Nat such that

A2: n0 = (2 |^ (2 |-count n0)) * m by NAT_D:def 3;

take 2 |-count n0 ; :: thesis: ex m being Nat st

( m is odd & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )

take m ; :: thesis: ( m is odd & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )

A3: now :: thesis: m is odd

hence
m is odd
; :: thesis: ( 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

assume not m is odd ; :: thesis: contradiction

then consider m99 being Nat such that

A4: m9 = 2 * m99 by ABIAN:def 2;

n0 = ((2 |^ (2 |-count n0)) * 2) * m99 by A2, A4

.= (2 |^ ((2 |-count n0) + 1)) * m99 by NEWTON:6 ;

then 2 |^ ((2 |-count n0) + 1) divides n0 by NAT_D:def 3;

hence contradiction by NAT_3:def 7; :: thesis: verum

end;assume not m is odd ; :: thesis: contradiction

then consider m99 being Nat such that

A4: m9 = 2 * m99 by ABIAN:def 2;

n0 = ((2 |^ (2 |-count n0)) * 2) * m99 by A2, A4

.= (2 |^ ((2 |-count n0) + 1)) * m99 by NEWTON:6 ;

then 2 |^ ((2 |-count n0) + 1) divides n0 by NAT_D:def 3;

hence contradiction by NAT_3:def 7; :: thesis: verum

now :: thesis: not 2 |-count n0 = 0

hence
2 |-count n0 > 0
; :: thesis: n0 = (2 |^ (2 |-count n0)) * massume
2 |-count n0 = 0
; :: thesis: contradiction

then n0 = 1 * m by A2, NEWTON:4;

hence contradiction by A1, A3; :: thesis: verum

end;then n0 = 1 * m by A2, NEWTON:4;

hence contradiction by A1, A3; :: thesis: verum

thus n0 = (2 |^ (2 |-count n0)) * m by A2; :: thesis: verum