let s be non zero Nat; :: thesis: for n being Nat st n > Product (primesFinS s) holds
ex p being Nat st
( n < p & p < 2 * n & rng (prime_exponents p) c= {0,1} & card (support (prime_exponents p)) = s )
let n be Nat; :: thesis: ( n > Product (primesFinS s) implies ex p being Nat st
( n < p & p < 2 * n & rng (prime_exponents p) c= {0,1} & card (support (prime_exponents p)) = s ) )
assume A1: n > Product (primesFinS s) ; :: thesis: ex p being Nat st
( n < p & p < 2 * n & rng (prime_exponents p) c= {0,1} & card (support (prime_exponents p)) = s )
reconsider s1 = s - 1 as Nat ;
set Ps = Product (primesFinS s1);
set k = n div (Product (primesFinS s1));
set r = n mod (Product (primesFinS s1));
A2: n = ((n div (Product (primesFinS s1))) * (Product (primesFinS s1))) + (n mod (Product (primesFinS s1))) by INT_1:59;
A3: s = s1 + 1 ;
A4: ((n div (Product (primesFinS s1))) * (Product (primesFinS s1))) + (Product (primesFinS s1)) > ((n div (Product (primesFinS s1))) * (Product (primesFinS s1))) + (n mod (Product (primesFinS s1))) by INT_1:58, XREAL_1:6;
((n div (Product (primesFinS s1))) * (Product (primesFinS s1))) + (n mod (Product (primesFinS s1))) > (Product (primesFinS s1)) * (primenumber s1) by A3, A1, A2, Th25;
then ((n div (Product (primesFinS s1))) + 1) * (Product (primesFinS s1)) > (Product (primesFinS s1)) * (primenumber s1) by A4, XXREAL_0:2;
then (n div (Product (primesFinS s1))) + 1 > primenumber s1 by XREAL_1:66;
then A5: n div (Product (primesFinS s1)) >= primenumber s1 by NAT_1:13;
then consider p being Prime such that
A6: ( n div (Product (primesFinS s1)) < p & p <= 2 * (n div (Product (primesFinS s1))) ) by NAT_1:14, NAT_4:56;
take pP = p * (Product (primesFinS s1)); :: thesis: ( n < pP & pP < 2 * n & rng (prime_exponents pP) c= {0,1} & card (support (prime_exponents pP)) = s )
A7: p <> 2 * (n div (Product (primesFinS s1)))

proof

assume p = 2 * (n div (Product (primesFinS s1))) ; :: thesis: contradiction
then p = 1 + 1 by NUMBER06:2;
then n div (Product (primesFinS s1)) <= 1 by A6, NAT_1:13;
hence contradiction by INT_2:def 4, A5, XXREAL_0:2; :: thesis: verum

end;

(n div (Product (primesFinS s1))) + 1 <= p by A6, NAT_1:13;
then ((n div (Product (primesFinS s1))) + 1) * (Product (primesFinS s1)) <= p * (Product (primesFinS s1)) by XREAL_1:66;
hence n < pP by A2, A4, XXREAL_0:2; :: thesis: ( pP < 2 * n & rng (prime_exponents pP) c= {0,1} & card (support (prime_exponents pP)) = s )
p < 2 * (n div (Product (primesFinS s1))) by A6, A7, XXREAL_0:1;
then A8: p * (Product (primesFinS s1)) < (2 * (n div (Product (primesFinS s1)))) * (Product (primesFinS s1)) by XREAL_1:68;
((2 * (n div (Product (primesFinS s1)))) * (Product (primesFinS s1))) + 0 <= ((2 * (n div (Product (primesFinS s1)))) * (Product (primesFinS s1))) + (2 * (n mod (Product (primesFinS s1)))) by XREAL_1:7;
hence pP < 2 * n by A2, A8, XXREAL_0:2; :: thesis: ( rng (prime_exponents pP) c= {0,1} & card (support (prime_exponents pP)) = s )
A9: (support (pfexp p)) \/ (support (pfexp (Product (primesFinS s1)))) = support (pfexp pP) by NAT_3:46;
A10: primeindex p <> s1 by A5, A6, NUMBER10:def 4;
A11: s1 < primeindex p

proof

assume s1 >= primeindex p ; :: thesis: contradiction
then s1 > primeindex p by A10, XXREAL_0:1;
then primenumber s1 > p by NUMBER13:12;
hence contradiction by A5, A6, XXREAL_0:2; :: thesis: verum

end;

then support (pfexp p) misses support (pfexp (Product (primesFinS s1))) by Th30, NAT_3:44;
then A12: card (support (pfexp pP)) = (card (support (pfexp p))) + (card (support (pfexp (Product (primesFinS s1))))) by A9, CARD_2:40;
A13: rng (pfexp (p * (Product (primesFinS s1)))) = (rng (pfexp p)) \/ (rng (pfexp (Product (primesFinS s1)))) by A11, Th30, Th24;
A14: rng (pfexp p) c= {0,1} by Th22;
rng (pfexp (Product (primesFinS s1))) c= {0,1} by Th31;
hence rng (pfexp pP) c= {0,1} by A13, A14, XBOOLE_1:8; :: thesis: card (support (prime_exponents pP)) = s
card (support (pfexp p)) = 1 by Th22;
hence card (support (pfexp pP)) = s by A3, Th31, A12; :: thesis: verum