let n be non trivial Nat; Sum (Basel-seq,n) < 5 / 3
Z2: Sum (Basel-seq,n) =
((Partial_Sums Basel-seq) . (0 + 1)) + (((Partial_Sums Basel-seq) . n) - ((Partial_Sums Basel-seq) . 1))
.=
(((Partial_Sums Basel-seq) . 0) + (Basel-seq . 1)) + (((Partial_Sums Basel-seq) . n) - ((Partial_Sums Basel-seq) . 1))
by SERIES_1:def 1
.=
((Basel-seq . 0) + (Basel-seq . 1)) + (((Partial_Sums Basel-seq) . n) - ((Partial_Sums Basel-seq) . 1))
by SERIES_1:def 1
.=
((1 / (0 ^2)) + (Basel-seq . 1)) + (Sum (Basel-seq,n,1))
by BASEL_1:31
.=
((1 / 0) + (1 / (1 ^2))) + (Sum (Basel-seq,n,1))
by BASEL_1:31
.=
1 + (Sum (Basel-seq,n,1))
;
Z5:
Sum (Basel-seq,n) < 1 + (Sum (Reci-seq1,n,1))
by Z2, XREAL_1:8, Impor2;
1 + (Sum (Reci-seq1,n,1)) < 1 + (2 / 3)
by XREAL_1:8, Seq3;
hence
Sum (Basel-seq,n) < 5 / 3
by Z5, XXREAL_0:2; verum