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

proof

let k be Nat; :: thesis: ( k >= 2 & S₁[k] implies S₁[k + 1] )
assume that
A2: k >= 2 and
A3: S₁[k] ; :: thesis: S₁[k + 1]
k block 2 = (1 / 2) * ((2 |^ k) - 2) by A2, Th47, XXREAL_0:2;
hence (k + 1) block 3 = (3 * (k block (2 + 1))) + ((1 / 2) * ((2 |^ k) - 2)) by Th46
.= (1 / 6) * (((3 * (3 |^ k)) - ((3 * 2) * (2 |^ k))) + 3) by A3
.= (1 / 6) * (((3 |^ (k + 1)) - (3 * (2 * (2 |^ k)))) + 3) by NEWTON:6
.= (1 / 6) * (((3 |^ (k + 1)) - (3 * (2 |^ (k + 1)))) + 3) by NEWTON:6 ;
:: thesis: verum

end;

(1 / 6) * (((3 |^ 2) - (3 * (2 |^ 2))) + 3) = (1 / 6) * (((3 * 3) - (3 * (2 |^ 2))) + 3) by WSIERP_1:1
.= (1 / 6) * (((3 * 3) - (3 * (2 * 2))) + 3) by WSIERP_1:1
.= 2 block 3 by Th29 ;
then A4: S₁[2] ;
for k being Nat st k >= 2 holds
S₁[k] from NAT_1:sch 8(A4, A1);
hence ( n >= 2 implies n block 3 = (1 / 6) * (((3 |^ n) - (3 * (2 |^ n))) + 3) ) ; :: thesis: verum