defpred S_{1}[ Nat] means for k being Nat st 1 <= k & k <= $1 holds

ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1);

A1: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

assume i > 0 ; :: thesis: ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1)

then A12: i >= 1 by NAT_1:14;

A13: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A13, A1);

hence ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1) by A12; :: thesis: verum

ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1);

A1: for i being Nat st S

S

proof

let i be Nat; :: thesis: ( i > 0 implies ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1) )
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A2: S_{1}[i]
; :: thesis: S_{1}[i + 1]

let k be Nat; :: thesis: ( 1 <= k & k <= i + 1 implies ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) )

assume that

A3: 1 <= k and

A4: k <= i + 1 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

end;assume A2: S

let k be Nat; :: thesis: ( 1 <= k & k <= i + 1 implies ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) )

assume that

A3: 1 <= k and

A4: k <= i + 1 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

now :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)end;

hence
ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)
; :: thesis: verumper cases
( ( k = i + 1 & i = 0 ) or ( k = i + 1 & i > 0 ) or k < i + 1 )
by A4, XXREAL_0:1;

end;

suppose A5:
( k = i + 1 & i = 0 )
; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

set m = 0 ;

A6: 1 = 2 |^ 0 by NEWTON:4;

k = 1 * ((0 * 2) + 1) by A5;

hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) by A6; :: thesis: verum

end;A6: 1 = 2 |^ 0 by NEWTON:4;

k = 1 * ((0 * 2) + 1) by A5;

hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) by A6; :: thesis: verum

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

end;

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

end;

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

then consider m being Nat such that

A8: k = (2 * m) + 1 and

1 < 2 by NAT_D:def 2;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

1 = 2 |^ 0 by NEWTON:4;

then k = (2 |^ 0) * ((2 * m) + 1) by A8;

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

end;A8: k = (2 * m) + 1 and

1 < 2 by NAT_D:def 2;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

1 = 2 |^ 0 by NEWTON:4;

then k = (2 |^ 0) * ((2 * m) + 1) by A8;

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

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

then consider j being Nat such that

A9: k = (2 * j) + 0 and

0 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A10: j <= i

then j >= 1 by NAT_1:14;

then consider n, m being Nat such that

A11: j = (2 |^ n) * ((2 * m) + 1) by A2, A10;

k = (2 * (2 |^ n)) * ((2 * m) + 1) by A9, A11;

then k = (2 |^ (n + 1)) * ((2 * m) + 1) by NEWTON:6;

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

end;A9: k = (2 * j) + 0 and

0 < 2 by NAT_D:def 2;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A10: j <= i

proof

j <> 0
by A7, A9;
assume
j > i
; :: thesis: contradiction

then j + j > i + 1 by NAT_1:14, XREAL_1:8;

hence contradiction by A7, A9; :: thesis: verum

end;then j + j > i + 1 by NAT_1:14, XREAL_1:8;

hence contradiction by A7, A9; :: thesis: verum

then j >= 1 by NAT_1:14;

then consider n, m being Nat such that

A11: j = (2 |^ n) * ((2 * m) + 1) by A2, A10;

k = (2 * (2 |^ n)) * ((2 * m) + 1) by A9, A11;

then k = (2 |^ (n + 1)) * ((2 * m) + 1) by NEWTON:6;

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

assume i > 0 ; :: thesis: ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1)

then A12: i >= 1 by NAT_1:14;

A13: S

for n being Nat holds S

hence ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1) by A12; :: thesis: verum