let n, m be Nat; :: thesis: ( n < m iff Product (primesFinS n) < Product (primesFinS m) )
thus ( n < m implies Product (primesFinS n) < Product (primesFinS m) ) :: thesis: ( Product (primesFinS n) < Product (primesFinS m) implies n < m )

proof

assume n < m ; :: thesis: Product (primesFinS n) < Product (primesFinS m)
then n + 1 <= m by NAT_1:13;
then A1: Product (primesFinS (n + 1)) <= Product (primesFinS m) by Lm2;
2 <= primenumber n by MOEBIUS2:8, MOEBIUS2:21;
then A2: (Product (primesFinS n)) * 2 <= (Product (primesFinS n)) * (primenumber n) by XREAL_1:66;
(Product (primesFinS n)) * 1 < (Product (primesFinS n)) * 2 by XREAL_1:68;
then Product (primesFinS n) < (Product (primesFinS n)) * (primenumber n) by A2, XXREAL_0:2;
then Product (primesFinS n) < Product (primesFinS (n + 1)) by Th25;
hence Product (primesFinS n) < Product (primesFinS m) by A1, XXREAL_0:2; :: thesis: verum

end;

thus ( Product (primesFinS n) < Product (primesFinS m) implies n < m ) by Lm2; :: thesis: verum