let n be Nat; :: thesis: ln . ((Partial_Product Reci-seq2) . n) <= (Partial_Sums ReciPrime) . n
defpred S₁[ Nat] means ln . ((Partial_Product Reci-seq2) . $1) <= (Partial_Sums ReciPrime) . $1;
B1: (Partial_Product Reci-seq2) . 0 = Reci-seq2 . 0 by SERIES_3:def 1
.= 1 + (1 / 2) by MOEBIUS2:8, My3Def ;
(Partial_Sums ReciPrime) . 0 = ReciPrime . 0 by SERIES_1:def 1
.= 1 / 2 by MOEBIUS2:8, MOEBIUS2:def 1 ;
then A1: S₁[ 0 ] by B1, Diesel1;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
C1: (Partial_Product Reci-seq2) . k > 0 by GreaterProduct;
C2: Reci-seq2 . (k + 1) > 0

proof

Reci-seq2 . (k + 1) = 1 + (1 / (primenumber (k + 1))) by My3Def;
hence Reci-seq2 . (k + 1) > 0 ; :: thesis: verum

end;

(Partial_Product Reci-seq2) . (k + 1) = ((Partial_Product Reci-seq2) . k) * (Reci-seq2 . (k + 1)) by SERIES_3:def 1;
then ln . ((Partial_Product Reci-seq2) . (k + 1)) = (ln . ((Partial_Product Reci-seq2) . k)) + (ln . (Reci-seq2 . (k + 1))) by LogAdd, C1, C2;
then D5: ln . ((Partial_Product Reci-seq2) . (k + 1)) <= ((Partial_Sums ReciPrime) . k) + (ln . (Reci-seq2 . (k + 1))) by XREAL_1:7, B1;
D3: (Partial_Sums ReciPrime) . (k + 1) = ((Partial_Sums ReciPrime) . k) + (ReciPrime . (k + 1)) by SERIES_1:def 1;
ln . (Reci-seq2 . (k + 1)) < ReciPrime . (k + 1)

proof

D1: Reci-seq2 . (k + 1) = 1 + (1 / (primenumber (k + 1))) by My3Def;
ReciPrime . (k + 1) = 1 / (primenumber (k + 1)) by MOEBIUS2:def 1;
hence ln . (Reci-seq2 . (k + 1)) < ReciPrime . (k + 1) by D1, Diesel1; :: thesis: verum

end;

then ((Partial_Sums ReciPrime) . k) + (ln . (Reci-seq2 . (k + 1))) < ((Partial_Sums ReciPrime) . k) + (ReciPrime . (k + 1)) by XREAL_1:8;
hence S₁[k + 1] by D5, XXREAL_0:2, D3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence ln . ((Partial_Product Reci-seq2) . n) <= (Partial_Sums ReciPrime) . n ; :: thesis: verum