Metamath Proof Explorer

Theorem prmreclem5

Description: Lemma for prmrec . Here we show the inequality N / 2 < # M by decomposing the set ( 1 ... N ) into the disjoint union of the set M of those numbers that are not divisible by any "large" primes (above K ) and the indexed union over K < k of the numbers Wk that divide the prime k . By prmreclem4 the second of these has size less than N times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part M must be at least N / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
prmrec.5 ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
prmrec.6 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) )
prmrec.7 ⊢ 𝑊 = ( 𝑝 ∈ ℕ ↦ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } )
Assertion prmreclem5 ( 𝜑 → ( 𝑁 / 2 ) < ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
2 prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
5 prmrec.5 ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
6 prmrec.6 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) )
7 prmrec.7 ⊢ 𝑊 = ( 𝑝 ∈ ℕ ↦ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } )
8 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
9 8 rehalfcld ⊢ ( 𝜑 → ( 𝑁 / 2 ) ∈ ℝ )
10 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
11 4 ssrab3 ⊢ 𝑀 ⊆ ( 1 ... 𝑁 )
12 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑀 ⊆ ( 1 ... 𝑁 ) ) → 𝑀 ∈ Fin )
13 10 11 12 mp2an ⊢ 𝑀 ∈ Fin
14 hashcl ⊢ ( 𝑀 ∈ Fin → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
15 13 14 ax-mp ⊢ ( ♯ ‘ 𝑀 ) ∈ ℕ0
16 15 nn0rei ⊢ ( ♯ ‘ 𝑀 ) ∈ ℝ
17 16 a1i ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℝ )
18 2nn ⊢ 2 ∈ ℕ
19 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
20 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ 𝐾 ) ∈ ℕ )
21 18 19 20 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℕ )
22 21 nnred ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℝ )
23 3 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
24 23 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ+ )
25 24 rpred ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
26 22 25 remulcld ⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
27 8 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
28 27 2halvesd ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) = 𝑁 )
29 11 a1i ⊢ ( 𝜑 → 𝑀 ⊆ ( 1 ... 𝑁 ) )
30 2 peano2nnd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ )
31 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
32 eluznn ⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ )
33 30 31 32 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℕ )
34 eleq1w ⊢ ( 𝑝 = 𝑘 → ( 𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
35 breq1 ⊢ ( 𝑝 = 𝑘 → ( 𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛 ) )
36 34 35 anbi12d ⊢ ( 𝑝 = 𝑘 → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) ↔ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) ) )
37 36 rabbidv ⊢ ( 𝑝 = 𝑘 → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
38 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
39 38 rabex ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } ∈ V
40 37 7 39 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝑊 ‘ 𝑘 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑊 ‘ 𝑘 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
42 ssrab2 ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } ⊆ ( 1 ... 𝑁 )
43 41 42 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
44 33 43 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
45 44 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
46 iunss ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ↔ ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
47 45 46 sylibr ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
48 29 47 unssd ⊢ ( 𝜑 → ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ⊆ ( 1 ... 𝑁 ) )
49 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛 ) )
50 49 notbid ⊢ ( 𝑝 = 𝑞 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛 ) )
51 50 cbvralvw ⊢ ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑛 )
52 breq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥 ) )
53 52 notbid ⊢ ( 𝑛 = 𝑥 → ( ¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥 ) )
54 53 ralbidv ⊢ ( 𝑛 = 𝑥 → ( ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑛 ↔ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 ) )
55 51 54 bitrid ⊢ ( 𝑛 = 𝑥 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 ) )
56 55 4 elrab2 ⊢ ( 𝑥 ∈ 𝑀 ↔ ( 𝑥 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 ) )
57 elun1 ⊢ ( 𝑥 ∈ 𝑀 → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
58 56 57 sylbir ⊢ ( ( 𝑥 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 ) → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
59 58 ex ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → ( ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
61 dfrex2 ⊢ ( ∃ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) 𝑞 ∥ 𝑥 ↔ ¬ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 )
62 2 nnzd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
63 62 peano2zd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℤ )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
65 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑁 ∈ ℤ )
67 eldifi ⊢ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑞 ∈ ℙ )
68 67 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∈ ℙ )
69 prmz ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
70 68 69 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∈ ℤ )
71 eldifn ⊢ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → ¬ 𝑞 ∈ ( 1 ... 𝐾 ) )
72 71 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ¬ 𝑞 ∈ ( 1 ... 𝐾 ) )
73 prmnn ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℕ )
74 68 73 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∈ ℕ )
75 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
76 74 75 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∈ ( ℤ≥ ‘ 1 ) )
77 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝐾 ∈ ℤ )
78 elfz5 ⊢ ( ( 𝑞 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑞 ∈ ( 1 ... 𝐾 ) ↔ 𝑞 ≤ 𝐾 ) )
79 76 77 78 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝑞 ∈ ( 1 ... 𝐾 ) ↔ 𝑞 ≤ 𝐾 ) )
80 72 79 mtbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ¬ 𝑞 ≤ 𝐾 )
81 2 nnred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
82 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝐾 ∈ ℝ )
83 74 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∈ ℝ )
84 82 83 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾 ) )
85 80 84 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝐾 < 𝑞 )
86 zltp1le ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝐾 < 𝑞 ↔ ( 𝐾 + 1 ) ≤ 𝑞 ) )
87 77 70 86 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝐾 < 𝑞 ↔ ( 𝐾 + 1 ) ≤ 𝑞 ) )
88 85 87 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝐾 + 1 ) ≤ 𝑞 )
89 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
90 89 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ ℕ )
91 90 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ ℝ )
92 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑁 ∈ ℝ )
93 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∥ 𝑥 )
94 dvdsle ⊢ ( ( 𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ ) → ( 𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥 ) )
95 70 90 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥 ) )
96 93 95 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ≤ 𝑥 )
97 elfzle2 ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ≤ 𝑁 )
98 97 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ≤ 𝑁 )
99 83 91 92 96 98 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ≤ 𝑁 )
100 64 66 70 88 99 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑞 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) )
101 52 anbi2d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) ↔ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥 ) ) )
102 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ ( 1 ... 𝑁 ) )
103 68 93 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥 ) )
104 101 102 103 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) } )
105 eleq1w ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ ) )
106 105 49 anbi12d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) ↔ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) ) )
107 106 rabbidv ⊢ ( 𝑝 = 𝑞 → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) } )
108 38 rabex ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) } ∈ V
109 107 7 108 fvmpt ⊢ ( 𝑞 ∈ ℕ → ( 𝑊 ‘ 𝑞 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) } )
110 74 109 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → ( 𝑊 ‘ 𝑞 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛 ) } )
111 104 110 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ ( 𝑊 ‘ 𝑞 ) )
112 fveq2 ⊢ ( 𝑘 = 𝑞 → ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ 𝑞 ) )
113 112 eliuni ⊢ ( ( 𝑞 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑊 ‘ 𝑞 ) ) → 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) )
114 100 111 113 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) )
115 elun2 ⊢ ( 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
116 114 115 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ∧ 𝑞 ∥ 𝑥 ) ) → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
117 116 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ∃ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) 𝑞 ∥ 𝑥 → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
118 61 117 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ¬ ∀ 𝑞 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
119 60 118 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
120 48 119 eqelssd ⊢ ( 𝜑 → ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) = ( 1 ... 𝑁 ) )
121 120 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) )
122 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
123 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
124 122 123 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
125 121 124 eqtr2d ⊢ ( 𝜑 → 𝑁 = ( ♯ ‘ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
126 13 a1i ⊢ ( 𝜑 → 𝑀 ∈ Fin )
127 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin )
128 10 47 127 sylancr ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin )
129 breq1 ⊢ ( 𝑝 = 𝑘 → ( 𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥 ) )
130 129 notbid ⊢ ( 𝑝 = 𝑘 → ( ¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥 ) )
131 breq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥 ) )
132 131 notbid ⊢ ( 𝑛 = 𝑥 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥 ) )
133 132 ralbidv ⊢ ( 𝑛 = 𝑥 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑥 ) )
134 133 4 elrab2 ⊢ ( 𝑥 ∈ 𝑀 ↔ ( 𝑥 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑥 ) )
135 134 simprbi ⊢ ( 𝑥 ∈ 𝑀 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑥 )
136 135 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑥 )
137 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → 𝑘 ∈ ℙ )
138 noel ⊢ ¬ 𝑘 ∈ ∅
139 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) )
140 139 biantrud ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ( 𝑘 ∈ ( 1 ... 𝐾 ) ↔ ( 𝑘 ∈ ( 1 ... 𝐾 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) )
141 elin ⊢ ( 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ↔ ( 𝑘 ∈ ( 1 ... 𝐾 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) )
142 140 141 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ( 𝑘 ∈ ( 1 ... 𝐾 ) ↔ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ) )
143 81 ltp1d ⊢ ( 𝜑 → 𝐾 < ( 𝐾 + 1 ) )
144 fzdisj ⊢ ( 𝐾 < ( 𝐾 + 1 ) → ( ( 1 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) = ∅ )
145 143 144 syl ⊢ ( 𝜑 → ( ( 1 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) = ∅ )
146 145 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ( ( 1 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) = ∅ )
147 146 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ( 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ( ( 𝐾 + 1 ) ... 𝑁 ) ) ↔ 𝑘 ∈ ∅ ) )
148 142 147 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ( 𝑘 ∈ ( 1 ... 𝐾 ) ↔ 𝑘 ∈ ∅ ) )
149 138 148 mtbiri ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ¬ 𝑘 ∈ ( 1 ... 𝐾 ) )
150 137 149 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → 𝑘 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) )
151 130 136 150 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ∧ 𝑘 ∈ ℙ ) ) → ¬ 𝑘 ∥ 𝑥 )
152 151 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥 ) )
153 imnan ⊢ ( ( 𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥 ) ↔ ¬ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥 ) )
154 152 153 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ¬ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥 ) )
155 33 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℕ )
156 155 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑊 ‘ 𝑘 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
157 156 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑊 ‘ 𝑘 ) ↔ 𝑥 ∈ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } ) )
158 breq2 ⊢ ( 𝑛 = 𝑥 → ( 𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥 ) )
159 158 anbi2d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) ↔ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥 ) ) )
160 159 elrab ⊢ ( 𝑥 ∈ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } ↔ ( 𝑥 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥 ) ) )
161 160 simprbi ⊢ ( 𝑥 ∈ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } → ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥 ) )
162 157 161 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑥 ∈ ( 𝑊 ‘ 𝑘 ) → ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥 ) ) )
163 154 162 mtod ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ¬ 𝑥 ∈ ( 𝑊 ‘ 𝑘 ) )
164 163 nrexdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ¬ ∃ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) 𝑥 ∈ ( 𝑊 ‘ 𝑘 ) )
165 eliun ⊢ ( 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) 𝑥 ∈ ( 𝑊 ‘ 𝑘 ) )
166 164 165 sylnibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) )
167 166 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
168 imnan ⊢ ( ( 𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ↔ ¬ ( 𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
169 167 168 sylib ⊢ ( 𝜑 → ¬ ( 𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
170 elin ⊢ ( 𝑥 ∈ ( 𝑀 ∩ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ↔ ( 𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
171 169 170 sylnibr ⊢ ( 𝜑 → ¬ 𝑥 ∈ ( 𝑀 ∩ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
172 171 eq0rdv ⊢ ( 𝜑 → ( 𝑀 ∩ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) = ∅ )
173 hashun ⊢ ( ( 𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin ∧ ( 𝑀 ∩ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) = ∅ ) → ( ♯ ‘ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) = ( ( ♯ ‘ 𝑀 ) + ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
174 126 128 172 173 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑀 ∪ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) = ( ( ♯ ‘ 𝑀 ) + ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
175 28 125 174 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) = ( ( ♯ ‘ 𝑀 ) + ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) )
176 hashcl ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℕ0 )
177 128 176 syl ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℕ0 )
178 177 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℝ )
179 fzfid ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ... 𝑁 ) ∈ Fin )
180 30 32 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ )
181 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
182 0re ⊢ 0 ∈ ℝ
183 ifcl ⊢ ( ( ( 1 / 𝑘 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
184 181 182 183 sylancl ⊢ ( 𝑘 ∈ ℕ → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
185 180 184 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
186 31 185 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
187 179 186 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
188 8 187 remulcld ⊢ ( 𝜑 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ∈ ℝ )
189 1 2 3 4 5 6 7 prmreclem4 ⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
190 eluz ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝐾 ) )
191 65 62 190 syl2anc ⊢ ( 𝜑 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝐾 ) )
192 nnleltp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑁 ≤ 𝐾 ↔ 𝑁 < ( 𝐾 + 1 ) ) )
193 3 2 192 syl2anc ⊢ ( 𝜑 → ( 𝑁 ≤ 𝐾 ↔ 𝑁 < ( 𝐾 + 1 ) ) )
194 fzn ⊢ ( ( ( 𝐾 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 < ( 𝐾 + 1 ) ↔ ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ ) )
195 63 65 194 syl2anc ⊢ ( 𝜑 → ( 𝑁 < ( 𝐾 + 1 ) ↔ ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ ) )
196 191 193 195 3bitrd ⊢ ( 𝜑 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ ) )
197 0le0 ⊢ 0 ≤ 0
198 27 mul01d ⊢ ( 𝜑 → ( 𝑁 · 0 ) = 0 )
199 197 198 breqtrrid ⊢ ( 𝜑 → 0 ≤ ( 𝑁 · 0 ) )
200 iuneq1 ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ∅ ( 𝑊 ‘ 𝑘 ) )
201 0iun ⊢ ∪ 𝑘 ∈ ∅ ( 𝑊 ‘ 𝑘 ) = ∅
202 200 201 eqtrdi ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) = ∅ )
203 202 fveq2d ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ∅ ) )
204 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
205 203 204 eqtrdi ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) = 0 )
206 sumeq1 ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ∅ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
207 sum0 ⊢ Σ 𝑘 ∈ ∅ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = 0
208 206 207 eqtrdi ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = 0 )
209 208 oveq2d ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · 0 ) )
210 205 209 breq12d ⊢ ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ 0 ≤ ( 𝑁 · 0 ) ) )
211 199 210 syl5ibrcom ⊢ ( 𝜑 → ( ( ( 𝐾 + 1 ) ... 𝑁 ) = ∅ → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
212 196 211 sylbid ⊢ ( 𝜑 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
213 uztric ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∨ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
214 62 65 213 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∨ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
215 189 212 214 mpjaod ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
216 eqid ⊢ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) = ( ℤ≥ ‘ ( 𝐾 + 1 ) )
217 eleq1w ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
218 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
219 217 218 ifbieq1d ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
220 ovex ⊢ ( 1 / 𝑘 ) ∈ V
221 c0ex ⊢ 0 ∈ V
222 220 221 ifex ⊢ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ V
223 219 1 222 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
224 180 223 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
225 184 recnd ⊢ ( 𝑘 ∈ ℕ → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
226 223 225 eqeltrd ⊢ ( 𝑘 ∈ ℕ → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
227 226 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
228 75 30 227 iserex ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq ( 𝐾 + 1 ) ( + , 𝐹 ) ∈ dom ⇝ ) )
229 5 228 mpbid ⊢ ( 𝜑 → seq ( 𝐾 + 1 ) ( + , 𝐹 ) ∈ dom ⇝ )
230 216 63 224 185 229 isumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
231 halfre ⊢ ( 1 / 2 ) ∈ ℝ
232 231 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
233 fzssuz ⊢ ( ( 𝐾 + 1 ) ... 𝑁 ) ⊆ ( ℤ≥ ‘ ( 𝐾 + 1 ) )
234 233 a1i ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ... 𝑁 ) ⊆ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
235 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
236 235 rpreccld ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ+ )
237 236 rpge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( 1 / 𝑘 ) )
238 breq2 ⊢ ( ( 1 / 𝑘 ) = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) → ( 0 ≤ ( 1 / 𝑘 ) ↔ 0 ≤ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
239 breq2 ⊢ ( 0 = if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
240 238 239 ifboth ⊢ ( ( 0 ≤ ( 1 / 𝑘 ) ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
241 237 197 240 sylancl ⊢ ( 𝑘 ∈ ℕ → 0 ≤ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
242 180 241 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
243 216 63 179 234 224 185 242 229 isumless ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
244 187 230 232 243 6 lelttrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) )
245 3 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
246 ltmul2 ⊢ ( ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) ↔ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) < ( 𝑁 · ( 1 / 2 ) ) ) )
247 187 232 8 245 246 syl112anc ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) ↔ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) < ( 𝑁 · ( 1 / 2 ) ) ) )
248 244 247 mpbid ⊢ ( 𝜑 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) < ( 𝑁 · ( 1 / 2 ) ) )
249 2cn ⊢ 2 ∈ ℂ
250 2ne0 ⊢ 2 ≠ 0
251 divrec ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 𝑁 / 2 ) = ( 𝑁 · ( 1 / 2 ) ) )
252 249 250 251 mp3an23 ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 / 2 ) = ( 𝑁 · ( 1 / 2 ) ) )
253 27 252 syl ⊢ ( 𝜑 → ( 𝑁 / 2 ) = ( 𝑁 · ( 1 / 2 ) ) )
254 248 253 breqtrrd ⊢ ( 𝜑 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) < ( 𝑁 / 2 ) )
255 178 188 9 215 254 lelttrd ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) < ( 𝑁 / 2 ) )
256 178 9 17 255 ltadd2dd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑀 ) + ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ) < ( ( ♯ ‘ 𝑀 ) + ( 𝑁 / 2 ) ) )
257 175 256 eqbrtrd ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) < ( ( ♯ ‘ 𝑀 ) + ( 𝑁 / 2 ) ) )
258 9 17 9 ltadd1d ⊢ ( 𝜑 → ( ( 𝑁 / 2 ) < ( ♯ ‘ 𝑀 ) ↔ ( ( 𝑁 / 2 ) + ( 𝑁 / 2 ) ) < ( ( ♯ ‘ 𝑀 ) + ( 𝑁 / 2 ) ) ) )
259 257 258 mpbird ⊢ ( 𝜑 → ( 𝑁 / 2 ) < ( ♯ ‘ 𝑀 ) )
260 oveq1 ⊢ ( 𝑘 = 𝑟 → ( 𝑘 ↑ 2 ) = ( 𝑟 ↑ 2 ) )
261 260 breq1d ⊢ ( 𝑘 = 𝑟 → ( ( 𝑘 ↑ 2 ) ∥ 𝑥 ↔ ( 𝑟 ↑ 2 ) ∥ 𝑥 ) )
262 261 cbvrabv ⊢ { 𝑘 ∈ ℕ ∣ ( 𝑘 ↑ 2 ) ∥ 𝑥 } = { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑥 }
263 breq2 ⊢ ( 𝑥 = 𝑛 → ( ( 𝑟 ↑ 2 ) ∥ 𝑥 ↔ ( 𝑟 ↑ 2 ) ∥ 𝑛 ) )
264 263 rabbidv ⊢ ( 𝑥 = 𝑛 → { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑥 } = { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } )
265 262 264 eqtrid ⊢ ( 𝑥 = 𝑛 → { 𝑘 ∈ ℕ ∣ ( 𝑘 ↑ 2 ) ∥ 𝑥 } = { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } )
266 265 supeq1d ⊢ ( 𝑥 = 𝑛 → sup ( { 𝑘 ∈ ℕ ∣ ( 𝑘 ↑ 2 ) ∥ 𝑥 } , ℝ , < ) = sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
267 266 cbvmptv ⊢ ( 𝑥 ∈ ℕ ↦ sup ( { 𝑘 ∈ ℕ ∣ ( 𝑘 ↑ 2 ) ∥ 𝑥 } , ℝ , < ) ) = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
268 1 2 3 4 267 prmreclem3 ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )
269 9 17 26 259 268 ltletrd ⊢ ( 𝜑 → ( 𝑁 / 2 ) < ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )