let n be Nat; :: thesis: ( n >= 3 implies n block 4 = (1 / 24) * ((((4 |^ n) - (4 * (3 |^ n))) + (6 * (2 |^ n))) - 4) )
defpred S₁[ Nat] means $1 block 4 = (1 / 24) * ((((4 |^ $1) - (4 * (3 |^ $1))) + (6 * (2 |^ $1))) - 4);
A1: for k being Nat st k >= 3 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 3 & S₁[k] implies S₁[k + 1] )
assume that
A2: k >= 3 and
A3: S₁[k] ; :: thesis: S₁[k + 1]
k block 3 = (1 / 6) * (((3 |^ k) - (3 * (2 |^ k))) + 3) by A2, Th48, XXREAL_0:2;
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: S₁[3] ;
for k being Nat st k >= 3 holds
S₁[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