let n be Nat; :: thesis: ( n >= 3 implies n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4) )
defpred S1[ Nat] means \$1 block 4 = (1 / 24) * ((((4 |^ \$1) - (4 * (3 |^ \$1))) + (6 * (2 |^ \$1))) - 4);
A1: for k being Nat st k >= 3 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 3 & S1[k] implies S1[k + 1] )
assume that
A2: k >= 3 and
A3: S1[k] ; :: thesis: S1[k + 1]
k block 3 = (1 / 6) * (((3 |^ k) - (3 * (2 |^ k))) + 3) by ;
hence (k + 1) block 4 = (4 * (k block (3 + 1))) + ((1 / 6) * (((3 |^ k) - (3 * (2 |^ k))) + 3)) by Th46
.= (1 / 24) * ((((4 * (4 |^ k)) - (4 * (3 * (3 |^ k)))) + (6 * (2 * (2 |^ k)))) - 4) by A3
.= (1 / 24) * ((((4 |^ (k + 1)) - (4 * (3 * (3 |^ k)))) + (6 * (2 * (2 |^ k)))) - 4) by NEWTON:6
.= (1 / 24) * ((((4 |^ (k + 1)) - (4 * (3 |^ (k + 1)))) + (6 * (2 * (2 |^ k)))) - 4) by NEWTON:6
.= (1 / 24) * ((((4 |^ (k + 1)) - (4 * (3 |^ (k + 1)))) + (6 * (2 |^ (k + 1)))) - 4) by NEWTON:6 ;
:: thesis: verum
end;
(1 / 24) * ((((4 |^ 3) - (4 * (3 |^ 3))) + (6 * (2 |^ 3))) - 4) = (1 / 24) * (((((4 * 4) * 4) - (4 * (3 |^ 3))) + (6 * (2 |^ 3))) - 4) by Lm3
.= (1 / 24) * (((64 - (4 * ((3 * 3) * 3))) + (6 * (2 |^ 3))) - 4) by Lm3
.= (1 / 24) * (((64 - (4 * 27)) + (6 * ((2 * 2) * 2))) - 4) by Lm3
.= 3 block 4 by Th29 ;
then A4: S1[3] ;
for k being Nat st k >= 3 holds
S1[k] from NAT_1:sch 8(A4, A1);
hence ( n >= 3 implies n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4) ) ; :: thesis: verum