defpred S1[ 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 S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; :: thesis: S1[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)
now :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)
per cases ( ( k = i + 1 & i = 0 ) or ( k = i + 1 & i > 0 ) or k < i + 1 ) by ;
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;
suppose A7: ( k = i + 1 & i > 0 ) ; :: thesis: ex n, m being 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 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;
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
proof
assume j > i ; :: thesis: contradiction
then j + j > i + 1 by ;
hence contradiction by A7, A9; :: thesis: verum
end;
j <> 0 by A7, A9;
then j >= 1 by NAT_1:14;
then consider n, m being Nat such that
A11: j = (2 |^ n) * ((2 * m) + 1) by ;
k = (2 * (2 |^ n)) * ((2 * m) + 1) by ;
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;
end;
end;
suppose k < i + 1 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)
then k <= i by NAT_1:13;
hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) by A2, A3; :: thesis: verum
end;
end;
end;
hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum
end;
let i be Nat; :: thesis: ( i > 0 implies ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 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: S1[ 0 ] ;
for n being Nat holds S1[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