Metamath Proof Explorer

Theorem prmreclem3

Description: Lemma for prmrec . The main inequality established here is # M <_ # { x e. M | ( Qx ) = 1 } x. sqrt N , where { x e. M | ( Qx ) = 1 } is the set of squarefree numbers in M . This is demonstrated by the map y |-> <. y / ( Qy ) ^ 2 , ( Qy ) >. where Qy is the largest number whose square divides y . (Contributed by Mario Carneiro, 5-Aug-2014)

Ref Expression
Hypotheses prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
prmreclem2.5 ⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
Assertion prmreclem3 ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
2 prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
5 prmreclem2.5 ⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
6 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
7 4 ssrab3 ⊢ 𝑀 ⊆ ( 1 ... 𝑁 )
8 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑀 ⊆ ( 1 ... 𝑁 ) ) → 𝑀 ∈ Fin )
9 6 7 8 mp2an ⊢ 𝑀 ∈ Fin
10 hashcl ⊢ ( 𝑀 ∈ Fin → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
11 9 10 ax-mp ⊢ ( ♯ ‘ 𝑀 ) ∈ ℕ0
12 11 nn0rei ⊢ ( ♯ ‘ 𝑀 ) ∈ ℝ
13 12 a1i ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℝ )
14 2nn ⊢ 2 ∈ ℕ
15 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
16 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ 𝐾 ) ∈ ℕ )
17 14 15 16 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℕ )
18 17 nnnn0d ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℕ0 )
19 3 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
20 19 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ+ )
21 20 rprege0d ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) )
22 flge0nn0 ⊢ ( ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℕ0 )
23 21 22 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℕ0 )
24 18 23 nn0mulcld ⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℕ0 )
25 24 nn0red ⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
26 17 nnred ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℝ )
27 20 rpred ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
28 26 27 remulcld ⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
29 ssrab2 ⊢ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ⊆ 𝑀
30 ssfi ⊢ ( ( 𝑀 ∈ Fin ∧ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ⊆ 𝑀 ) → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin )
31 9 29 30 mp2an ⊢ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin
32 hashcl ⊢ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℕ0 )
33 31 32 ax-mp ⊢ ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℕ0
34 33 nn0rei ⊢ ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℝ
35 23 nn0red ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ )
36 remulcl ⊢ ( ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℝ ∧ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
37 34 35 36 sylancr ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
38 fzfi ⊢ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ Fin
39 xpfi ⊢ ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin ∧ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ Fin ) → ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin )
40 31 38 39 mp2an ⊢ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin
41 fveqeq2 ⊢ ( 𝑥 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( ( 𝑄 ‘ 𝑥 ) = 1 ↔ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ 𝑀 )
43 7 42 sseldi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ( 1 ... 𝑁 ) )
44 elfznn ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ∈ ℕ )
45 43 44 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℕ )
46 5 prmreclem1 ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
47 46 simp2d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 )
48 45 47 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 )
49 46 simp1d ⊢ ( 𝑦 ∈ ℕ → ( 𝑄 ‘ 𝑦 ) ∈ ℕ )
50 45 49 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ℕ )
51 50 nnsqcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ )
52 51 nnzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ )
53 51 nnne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≠ 0 )
54 45 nnzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℤ )
55 dvdsval2 ⊢ ( ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≠ 0 ∧ 𝑦 ∈ ℤ ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ) )
56 52 53 54 55 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ) )
57 48 56 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ )
58 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
59 nngt0 ⊢ ( 𝑦 ∈ ℕ → 0 < 𝑦 )
60 58 59 jca ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
61 nnre ⊢ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ )
62 nngt0 ⊢ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ → 0 < ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) )
63 61 62 jca ⊢ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ ∧ 0 < ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
64 divgt0 ⊢ ( ( ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ∧ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ ∧ 0 < ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) → 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
65 60 63 64 syl2an ⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ ) → 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
66 45 51 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
67 elnnz ⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ ↔ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
68 57 66 67 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ )
69 68 nnred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℝ )
70 45 nnred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℝ )
71 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑁 ∈ ℝ )
73 dvdsmul1 ⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
74 57 52 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
75 45 nncnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℂ )
76 51 nncnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℂ )
77 75 76 53 divcan1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = 𝑦 )
78 74 77 breqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 )
79 dvdsle ⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑦 ) )
80 57 45 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑦 ) )
81 78 80 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑦 )
82 elfzle2 ⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ≤ 𝑁 )
83 43 82 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ≤ 𝑁 )
84 69 70 72 81 83 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑁 )
85 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
86 68 85 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( ℤ≥ ‘ 1 ) )
87 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑁 ∈ ℤ )
89 elfz5 ⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑁 ) )
90 86 88 89 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑁 ) )
91 84 90 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) )
92 breq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦 ) )
93 92 notbid ⊢ ( 𝑛 = 𝑦 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦 ) )
94 93 ralbidv ⊢ ( 𝑛 = 𝑦 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
95 94 4 elrab2 ⊢ ( 𝑦 ∈ 𝑀 ↔ ( 𝑦 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
96 42 95 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
97 96 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 )
98 78 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 )
99 eldifi ⊢ ( 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℙ )
100 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
101 99 100 syl ⊢ ( 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℤ )
102 101 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → 𝑝 ∈ ℤ )
103 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ )
104 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → 𝑦 ∈ ℤ )
105 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∧ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 ) → 𝑝 ∥ 𝑦 ) )
106 102 103 104 105 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∧ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 ) → 𝑝 ∥ 𝑦 ) )
107 98 106 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → 𝑝 ∥ 𝑦 ) )
108 107 con3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
109 108 ralimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
110 97 109 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
111 breq2 ⊢ ( 𝑛 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
112 111 notbid ⊢ ( 𝑛 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
113 112 ralbidv ⊢ ( 𝑛 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
114 113 4 elrab2 ⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑀 ↔ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
115 91 110 114 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑀 )
116 5 prmreclem1 ⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ ∧ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐴 ↑ 2 ) ∥ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) / ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ) ) ) )
117 116 simp2d ⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
118 68 117 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
119 116 simp1d ⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ )
120 68 119 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ )
121 elnn1uz2 ⊢ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ ↔ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 ∨ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
122 120 121 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 ∨ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
123 122 ord ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ¬ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
124 5 prmreclem1 ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ∧ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) → ¬ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
125 124 simp3d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) → ¬ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
126 45 123 125 sylsyld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ¬ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 → ¬ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
127 118 126 mt4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 )
128 41 115 127 elrabd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } )
129 51 nnred ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ )
130 dvdsle ⊢ ( ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑦 ) )
131 52 45 130 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑦 ) )
132 48 131 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑦 )
133 129 70 72 132 83 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑁 )
134 72 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑁 ∈ ℂ )
135 134 sqsqrtd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( √ ‘ 𝑁 ) ↑ 2 ) = 𝑁 )
136 133 135 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) )
137 50 nnrpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ℝ+ )
138 20 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( √ ‘ 𝑁 ) ∈ ℝ+ )
139 rprege0 ⊢ ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ+ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑄 ‘ 𝑦 ) ) )
140 rprege0 ⊢ ( ( √ ‘ 𝑁 ) ∈ ℝ+ → ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) )
141 le2sq ⊢ ( ( ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑄 ‘ 𝑦 ) ) ∧ ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) ) )
142 139 140 141 syl2an ⊢ ( ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ+ ∧ ( √ ‘ 𝑁 ) ∈ ℝ+ ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) ) )
143 137 138 142 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) ) )
144 136 143 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) )
145 27 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( √ ‘ 𝑁 ) ∈ ℝ )
146 50 nnzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ℤ )
147 flge ⊢ ( ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑄 ‘ 𝑦 ) ∈ ℤ ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
148 145 146 147 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
149 144 148 mpbid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
150 50 85 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 1 ) )
151 23 nn0zd ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℤ )
152 151 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℤ )
153 elfz5 ⊢ ( ( ( 𝑄 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( 𝑄 ‘ 𝑦 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
154 150 152 153 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
155 149 154 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
156 128 155 opelxpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ ∈ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
157 156 ex ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑀 → ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ ∈ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
158 ovex ⊢ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ V
159 fvex ⊢ ( 𝑄 ‘ 𝑦 ) ∈ V
160 158 159 opth ⊢ ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ ↔ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ∧ ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) ) )
161 oveq1 ⊢ ( ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) )
162 oveq12 ⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
163 161 162 sylan2 ⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ∧ ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
164 160 163 sylbi ⊢ ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
165 77 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = 𝑦 )
166 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
167 7 166 sstri ⊢ 𝑀 ⊆ ℕ
168 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → 𝑧 ∈ 𝑀 )
169 167 168 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → 𝑧 ∈ ℕ )
170 169 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → 𝑧 ∈ ℂ )
171 5 prmreclem1 ⊢ ( 𝑧 ∈ ℕ → ( ( 𝑄 ‘ 𝑧 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ∥ 𝑧 ∧ ( 2 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 2 ↑ 2 ) ∥ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ) ) )
172 171 simp1d ⊢ ( 𝑧 ∈ ℕ → ( 𝑄 ‘ 𝑧 ) ∈ ℕ )
173 169 172 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( 𝑄 ‘ 𝑧 ) ∈ ℕ )
174 173 nnsqcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ∈ ℕ )
175 174 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ∈ ℂ )
176 174 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ≠ 0 )
177 170 175 176 divcan1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) = 𝑧 )
178 165 177 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ↔ 𝑦 = 𝑧 ) )
179 164 178 syl5ib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ → 𝑦 = 𝑧 ) )
180 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
181 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) )
182 181 oveq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) )
183 180 182 oveq12d ⊢ ( 𝑦 = 𝑧 → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
184 183 181 opeq12d ⊢ ( 𝑦 = 𝑧 → ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ )
185 179 184 impbid1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ ↔ 𝑦 = 𝑧 ) )
186 185 ex ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) → ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ ↔ 𝑦 = 𝑧 ) ) )
187 157 186 dom2d ⊢ ( 𝜑 → ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin → 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
188 40 187 mpi ⊢ ( 𝜑 → 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
189 hashdom ⊢ ( ( 𝑀 ∈ Fin ∧ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑀 ) ≤ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) ↔ 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
190 9 40 189 mp2an ⊢ ( ( ♯ ‘ 𝑀 ) ≤ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) ↔ 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
191 188 190 sylibr ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
192 hashxp ⊢ ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin ∧ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ Fin ) → ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
193 31 38 192 mp2an ⊢ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
194 hashfz1 ⊢ ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
195 23 194 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
196 195 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
197 193 196 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
198 191 197 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
199 34 a1i ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℝ )
200 23 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
201 1 2 3 4 5 prmreclem2 ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( 2 ↑ 𝐾 ) )
202 199 26 35 200 201 lemul1ad ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
203 13 37 25 198 202 letrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
204 17 nnrpd ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℝ+ )
205 204 rprege0d ⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝐾 ) ) )
206 fllelt ⊢ ( ( √ ‘ 𝑁 ) ∈ ℝ → ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) ∧ ( √ ‘ 𝑁 ) < ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) + 1 ) ) )
207 27 206 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) ∧ ( √ ‘ 𝑁 ) < ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) + 1 ) ) )
208 207 simpld ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) )
209 lemul2a ⊢ ( ( ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ ∧ ( √ ‘ 𝑁 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐾 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝐾 ) ) ) ∧ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) ) → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )
210 35 27 205 208 209 syl31anc ⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )
211 13 25 28 203 210 letrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )