let n be non trivial Nat; :: thesis: Sum (Basel-seq,n,1) < Sum (Reci-seq1,n,1)
for k being non trivial Nat st k <= n holds
Basel-seq . k < Reci-seq1 . k

proof

let k be non trivial Nat; :: thesis: ( k <= n implies Basel-seq . k < Reci-seq1 . k )
assume k <= n ; :: thesis: Basel-seq . k < Reci-seq1 . k
Z1: Basel-seq . k = 1 / (k ^2) by BASEL_1:31;
Z2: Reci-seq1 . k = 1 / ((k ^2) - (1 / 4)) by MyDef;
k >= 1 + 1 by NAT_2:29;
then k > 1 by NAT_1:13;
then k ^2 > 1 ^2 by SQUARE_1:16;
then (k ^2) - (1 / 4) > 1 - (1 / 4) by XREAL_1:14;
then (k ^2) - (1 / 4) > 3 / 4 ;
hence Basel-seq . k < Reci-seq1 . k by Z1, Z2, XREAL_1:76, XREAL_1:44; :: thesis: verum

end;

hence Sum (Basel-seq,n,1) < Sum (Reci-seq1,n,1) by Impor3; :: thesis: verum