let i be Element of NAT ; :: thesis: ( i > 0 implies ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1) )
assume A1: i > 0 ; :: thesis: ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1)
defpred S₁[ Element of NAT ] means for k being Element of NAT st 1 <= k & k <= $1 holds
ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1);
A2: S₁[ 0 ] ;
A3: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
let k be Element of NAT ; :: thesis: ( 1 <= k & k <= i + 1 implies ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) )
assume A5: ( 1 <= k & k <= i + 1 ) ; :: thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)

now

per cases ( ( k = i + 1 & i = 0 ) or ( k = i + 1 & i > 0 ) or k < i + 1 ) by A5, XXREAL_0:1;

suppose A6: ( k = i + 1 & i = 0 ) ; :: thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)

set m = 0 ;
( k = 1 * ((0 * 2) + 1) & 1 = 2 |^ 0 ) by A6, NEWTON:9;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

suppose A7: ( k = i + 1 & i > 0 ) ; :: thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)

per cases ( k mod 2 = 1 or k mod 2 = 0 ) by NAT_D:12;

suppose k mod 2 = 1 ; :: thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)

then consider m being Nat such that
A8: ( k = (2 * m) + 1 & 1 < 2 ) by NAT_D:def 2;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
1 = 2 |^ 0 by NEWTON:9;
then k = (2 |^ 0 ) * ((2 * m) + 1) by A8;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

suppose k mod 2 = 0 ; :: thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)

then consider j being Nat such that
A9: ( k = (2 * j) + 0 & 0 < 2 ) by NAT_D:def 2;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j <> 0 by A7, A9;
then A10: j >= 1 by NAT_1:14;
j <= i

proof

assume j > i ; :: thesis: contradiction
then j + j > i + 1 by NAT_1:14, XREAL_1:10;
hence contradiction by A7, A9; :: thesis: verum

end;

then consider n, m being Element of NAT such that
A11: j = (2 |^ n) * ((2 * m) + 1) by A4, A10;
k = (2 * (2 |^ n)) * ((2 * m) + 1) by A9, A11;
then k = (2 |^ (n + 1)) * ((2 * m) + 1) by NEWTON:11;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

end;

end;

suppose k < i + 1 ; :: thesis: ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1)

then k <= i by NAT_1:13;
hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) by A4, A5; :: thesis: verum

end;

end;

end;

hence ex n, m being Element of NAT st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

A12: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
i >= 1 by A1, NAT_1:14;
hence ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1) by A12; :: thesis: verum