let n be Nat; :: thesis: (n + 1) block n = (n + 1) choose 2

defpred S_{1}[ Nat] means ($1 + 1) block $1 = ($1 + 1) choose 2;

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

S_{1}[k + 1]

then A3: S_{1}[ 0 ]
by NEWTON:def 3;

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

hence (n + 1) block n = (n + 1) choose 2 ; :: thesis: verum

defpred S

A1: for k being Nat st S

S

proof

1 block 0 = 0
by Th31;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

set k1 = k + 1;

thus ((k + 1) + 1) block (k + 1) = ((k + 1) * ((k + 1) block (k + 1))) + ((k + 1) block k) by Th46

.= ((k + 1) * 1) + ((k + 1) choose 2) by A2, Th26

.= (k + 1) + (((k + 1) * ((k + 1) - 1)) / 2) by Th51

.= (((k + 1) + 1) * (((k + 1) + 1) - 1)) / 2

.= ((k + 1) + 1) choose 2 by Th51 ; :: thesis: verum

end;assume A2: S

set k1 = k + 1;

thus ((k + 1) + 1) block (k + 1) = ((k + 1) * ((k + 1) block (k + 1))) + ((k + 1) block k) by Th46

.= ((k + 1) * 1) + ((k + 1) choose 2) by A2, Th26

.= (k + 1) + (((k + 1) * ((k + 1) - 1)) / 2) by Th51

.= (((k + 1) + 1) * (((k + 1) + 1) - 1)) / 2

.= ((k + 1) + 1) choose 2 by Th51 ; :: thesis: verum

then A3: S

for k being Nat holds S

hence (n + 1) block n = (n + 1) choose 2 ; :: thesis: verum