let k, n be Nat; :: thesis: ( n > 0 implies ( 0 <= (bseq k) . n & (bseq k) . n <= 1 / (k !) & (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k ) )
defpred S1[ Nat] means (bseq $1) . n <= 1 / ($1 !);
assume A1: n > 0 ; :: thesis: ( 0 <= (bseq k) . n & (bseq k) . n <= 1 / (k !) & (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k )
then A2: n ^ (- k) > 0 by POWER:34;
A3: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
per cases ( k < n or k >= n ) ;
suppose A5: k < n ; :: thesis: S1[k + 1]
(1 / (k + 1)) * ((bseq k) . n) <= (1 / (k + 1)) * (1 / (k !)) by A4, XREAL_1:64;
then A6: (1 / (k + 1)) * ((bseq k) . n) <= 1 / ((k + 1) !) by Th11;
(aseq k) . n >= 0 by A5, Th13;
then A7: ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) <= (1 / ((k + 1) !)) * ((aseq k) . n) by A6, XREAL_1:64;
(aseq k) . n <= 1 by A5, Th13;
then A8: (1 / ((k + 1) !)) * ((aseq k) . n) <= 1 / ((k + 1) !) by XREAL_1:153;
(bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) by A1, Th6;
hence S1[k + 1] by A7, A8, XXREAL_0:2; :: thesis: verum
end;
suppose k >= n ; :: thesis: S1[k + 1]
then A9: k + 1 > n by NAT_1:13;
(bseq (k + 1)) . n = (n choose (k + 1)) * (n ^ (- (k + 1))) by Def2
.= 0 * (n ^ (- (k + 1))) by A9, NEWTON:def 3
.= 0 ;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
end;
A10: (bseq k) . n = (n choose k) * (n ^ (- k)) by Def2;
hence 0 <= (bseq k) . n by A2; :: thesis: ( (bseq k) . n <= 1 / (k !) & (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k )
A11: S1[ 0 ] by Th10, NEWTON:12;
for k being Nat holds S1[k] from NAT_1:sch 2(A11, A3);
 hence A12: (bseq k) . n <= 1 / (k !) ; :: thesis: ( (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k )
hence (bseq k) . n <= eseq . k by Def5; :: thesis: ( 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k )
hence ( 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k ) by A10, A2, A12, Th3; :: thesis: verum