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