Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmreclem3 Structured version   Visualization version   GIF version

Theorem prmreclem3 15669
 Description: Lemma for prmrec 15673. The main inequality established here is #𝑀 ≤ #{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} · √𝑁, where {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} is the set of squarefree numbers in 𝑀. This is demonstrated by the map 𝑦 ↦ ⟨𝑦 / (𝑄‘𝑦)↑2, (𝑄‘𝑦)⟩ where 𝑄‘𝑦 is the largest number whose square divides 𝑦. (Contributed by Mario Carneiro, 5-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
prmrec.2 (𝜑𝐾 ∈ ℕ)
prmrec.3 (𝜑𝑁 ∈ ℕ)
prmrec.4 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
prmreclem2.5 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
Assertion
Ref Expression
prmreclem3 (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
Distinct variable groups:   𝑛,𝑝,𝑟,𝐹   𝑛,𝐾,𝑝   𝑛,𝑀,𝑝   𝜑,𝑛,𝑝   𝑄,𝑛,𝑝,𝑟   𝑛,𝑁,𝑝
Allowed substitution hints:   𝜑(𝑟)   𝐾(𝑟)   𝑀(𝑟)   𝑁(𝑟)

Proof of Theorem prmreclem3
Dummy variables 𝑥 𝑦 𝑧 𝐴 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfi 12811 . . . . . 6 (1...𝑁) ∈ Fin
2 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
3 ssrab2 3720 . . . . . . 7 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)
42, 3eqsstri 3668 . . . . . 6 𝑀 ⊆ (1...𝑁)
5 ssfi 8221 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
61, 4, 5mp2an 708 . . . . 5 𝑀 ∈ Fin
7 hashcl 13185 . . . . 5 (𝑀 ∈ Fin → (#‘𝑀) ∈ ℕ0)
86, 7ax-mp 5 . . . 4 (#‘𝑀) ∈ ℕ0
98nn0rei 11341 . . 3 (#‘𝑀) ∈ ℝ
109a1i 11 . 2 (𝜑 → (#‘𝑀) ∈ ℝ)
11 2nn 11223 . . . . . 6 2 ∈ ℕ
12 prmrec.2 . . . . . . 7 (𝜑𝐾 ∈ ℕ)
1312nnnn0d 11389 . . . . . 6 (𝜑𝐾 ∈ ℕ0)
14 nnexpcl 12913 . . . . . 6 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1511, 13, 14sylancr 696 . . . . 5 (𝜑 → (2↑𝐾) ∈ ℕ)
1615nnnn0d 11389 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ0)
17 prmrec.3 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1817nnrpd 11908 . . . . . . 7 (𝜑𝑁 ∈ ℝ+)
1918rpsqrtcld 14194 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
2019rprege0d 11917 . . . . 5 (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
21 flge0nn0 12661 . . . . 5 (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ0)
2220, 21syl 17 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ0)
2316, 22nn0mulcld 11394 . . 3 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ0)
2423nn0red 11390 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
2515nnred 11073 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
2619rpred 11910 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2725, 26remulcld 10108 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
28 ssrab2 3720 . . . . . . 7 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
29 ssfi 8221 . . . . . . 7 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
306, 28, 29mp2an 708 . . . . . 6 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
31 hashcl 13185 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0)
3230, 31ax-mp 5 . . . . 5 (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0
3332nn0rei 11341 . . . 4 (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ
3422nn0red 11390 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
35 remulcl 10059 . . . 4 (((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
3633, 34, 35sylancr 696 . . 3 (𝜑 → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
37 fzfi 12811 . . . . . . 7 (1...(⌊‘(√‘𝑁))) ∈ Fin
38 xpfi 8272 . . . . . . 7 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
3930, 37, 38mp2an 708 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
40 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → 𝑦𝑀)
414, 40sseldi 3634 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → 𝑦 ∈ (1...𝑁))
42 elfznn 12408 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℕ)
44 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
4544prmreclem1 15667 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
4645simp2d 1094 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → ((𝑄𝑦)↑2) ∥ 𝑦)
4743, 46syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∥ 𝑦)
4845simp1d 1093 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → (𝑄𝑦) ∈ ℕ)
4943, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℕ)
5049nnsqcld 13069 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℕ)
5150nnzd 11519 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℤ)
5250nnne0d 11103 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≠ 0)
5343nnzd 11519 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℤ)
54 dvdsval2 15030 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑦)↑2) ∈ ℤ ∧ ((𝑄𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5551, 52, 53, 54syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5647, 55mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
57 nnre 11065 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58 nngt0 11087 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 0 < 𝑦)
5957, 58jca 553 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60 nnre 11065 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → ((𝑄𝑦)↑2) ∈ ℝ)
61 nngt0 11087 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → 0 < ((𝑄𝑦)↑2))
6260, 61jca 553 . . . . . . . . . . . . . . . . 17 (((𝑄𝑦)↑2) ∈ ℕ → (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2)))
63 divgt0 10929 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2))) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6459, 62, 63syl2an 493 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ ((𝑄𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6543, 50, 64syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
66 elnnz 11425 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄𝑦)↑2))))
6756, 65, 66sylanbrc 699 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ)
6867nnred 11073 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℝ)
6943nnred 11073 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦 ∈ ℝ)
7017nnred 11073 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
7170adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℝ)
72 dvdsmul1 15050 . . . . . . . . . . . . . . . 16 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ ((𝑄𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7356, 51, 72syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7443nncnd 11074 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → 𝑦 ∈ ℂ)
7550nncnd 11074 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℂ)
7674, 75, 52divcan1d 10840 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
7773, 76breqtrd 4711 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
78 dvdsle 15079 . . . . . . . . . . . . . . 15 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
7956, 43, 78syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
8077, 79mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦)
81 elfzle2 12383 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑁) → 𝑦𝑁)
8241, 81syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦𝑁)
8368, 69, 71, 80, 82letrd 10232 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁)
84 nnuz 11761 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8567, 84syl6eleq 2740 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1))
8617nnzd 11519 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
8786adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℤ)
88 elfz5 12372 . . . . . . . . . . . . 13 (((𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
8985, 87, 88syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
9083, 89mpbird 247 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁))
91 breq2 4689 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
9291notbid 307 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
9392ralbidv 3015 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9493, 2elrab2 3399 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9540, 94sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9695simprd 478 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
9777adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
98 eldifi 3765 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99 prmz 15436 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101100adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
10256adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
10353adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104 dvdstr 15065 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
105101, 102, 103, 104syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
10697, 105mpan2d 710 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) → 𝑝𝑦))
107106con3d 148 . . . . . . . . . . . . 13 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
108107ralimdva 2991 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
10996, 108mpd 15 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)))
110 breq2 4689 . . . . . . . . . . . . . 14 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (𝑝𝑛𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
111110notbid 307 . . . . . . . . . . . . 13 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (¬ 𝑝𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
112111ralbidv 3015 . . . . . . . . . . . 12 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
113112, 2elrab2 3399 . . . . . . . . . . 11 ((𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
11490, 109, 113sylanbrc 699 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀)
11544prmreclem1 15667 . . . . . . . . . . . . 13 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝐴 ∈ (ℤ‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2)))))
116115simp2d 1094 . . . . . . . . . . . 12 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
11767, 116syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
118115simp1d 1093 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
11967, 118syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
120 elnn1uz2 11803 . . . . . . . . . . . . . 14 ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
121119, 120sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
122121ord 391 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
12344prmreclem1 15667 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
124123simp3d 1095 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
12543, 122, 124sylsyld 61 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
126117, 125mt4d 152 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1)
127 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = (𝑦 / ((𝑄𝑦)↑2)) → (𝑄𝑥) = (𝑄‘(𝑦 / ((𝑄𝑦)↑2))))
128127eqeq1d 2653 . . . . . . . . . . 11 (𝑥 = (𝑦 / ((𝑄𝑦)↑2)) → ((𝑄𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1))
129128elrab 3396 . . . . . . . . . 10 ((𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀 ∧ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1))
130114, 126, 129sylanbrc 699 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1})
13150nnred 11073 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℝ)
132 dvdsle 15079 . . . . . . . . . . . . . . . 16 ((((𝑄𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13351, 43, 132syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13447, 133mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑦)
135131, 69, 71, 134, 82letrd 10232 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑁)
13671recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → 𝑁 ∈ ℂ)
137136sqsqrtd 14222 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((√‘𝑁)↑2) = 𝑁)
138135, 137breqtrrd 4713 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2))
13949nnrpd 11908 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℝ+)
14019adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ+)
141 rprege0 11885 . . . . . . . . . . . . . 14 ((𝑄𝑦) ∈ ℝ+ → ((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)))
142 rprege0 11885 . . . . . . . . . . . . . 14 ((√‘𝑁) ∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
143 le2sq 12978 . . . . . . . . . . . . . 14 ((((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
144141, 142, 143syl2an 493 . . . . . . . . . . . . 13 (((𝑄𝑦) ∈ ℝ+ ∧ (√‘𝑁) ∈ ℝ+) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
145139, 140, 144syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
146138, 145mpbird 247 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (√‘𝑁))
14726adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ)
14849nnzd 11519 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℤ)
149 flge 12646 . . . . . . . . . . . 12 (((√‘𝑁) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
150147, 148, 149syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
151146, 150mpbid 222 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (⌊‘(√‘𝑁)))
15249, 84syl6eleq 2740 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (ℤ‘1))
15322nn0zd 11518 . . . . . . . . . . . 12 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
154153adantr 480 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
155 elfz5 12372 . . . . . . . . . . 11 (((𝑄𝑦) ∈ (ℤ‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
156152, 154, 155syl2anc 694 . . . . . . . . . 10 ((𝜑𝑦𝑀) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
157151, 156mpbird 247 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))))
158 opelxpi 5182 . . . . . . . . 9 (((𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ (𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁)))) → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
159130, 157, 158syl2anc 694 . . . . . . . 8 ((𝜑𝑦𝑀) → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
160159ex 449 . . . . . . 7 (𝜑 → (𝑦𝑀 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
161 ovex 6718 . . . . . . . . . . . 12 (𝑦 / ((𝑄𝑦)↑2)) ∈ V
162 fvex 6239 . . . . . . . . . . . 12 (𝑄𝑦) ∈ V
163161, 162opth 4974 . . . . . . . . . . 11 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ ((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)))
164 oveq1 6697 . . . . . . . . . . . 12 ((𝑄𝑦) = (𝑄𝑧) → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
165 oveq12 6699 . . . . . . . . . . . 12 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
166164, 165sylan2 490 . . . . . . . . . . 11 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
167163, 166sylbi 207 . . . . . . . . . 10 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
16876adantrr 753 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
16942ssriv 3640 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
1704, 169sstri 3645 . . . . . . . . . . . . . 14 𝑀 ⊆ ℕ
171 simprr 811 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧𝑀)
172170, 171sseldi 3634 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℕ)
173172nncnd 11074 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℂ)
17444prmreclem1 15667 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → ((𝑄𝑧) ∈ ℕ ∧ ((𝑄𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄𝑧)↑2)))))
175174simp1d 1093 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → (𝑄𝑧) ∈ ℕ)
176172, 175syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (𝑄𝑧) ∈ ℕ)
177176nnsqcld 13069 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℕ)
178177nncnd 11074 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℂ)
179177nnne0d 11103 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ≠ 0)
180173, 178, 179divcan1d 10840 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) = 𝑧)
181168, 180eqeq12d 2666 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) ↔ 𝑦 = 𝑧))
182167, 181syl5ib 234 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → 𝑦 = 𝑧))
183 id 22 . . . . . . . . . . 11 (𝑦 = 𝑧𝑦 = 𝑧)
184 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑄𝑦) = (𝑄𝑧))
185184oveq1d 6705 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
186183, 185oveq12d 6708 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)))
187186, 184opeq12d 4441 . . . . . . . . 9 (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩)
188182, 187impbid1 215 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧))
189188ex 449 . . . . . . 7 (𝜑 → ((𝑦𝑀𝑧𝑀) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧)))
190160, 189dom2d 8038 . . . . . 6 (𝜑 → (({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
19139, 190mpi 20 . . . . 5 (𝜑𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
192 hashdom 13206 . . . . . 6 ((𝑀 ∈ Fin ∧ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((#‘𝑀) ≤ (#‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
1936, 39, 192mp2an 708 . . . . 5 ((#‘𝑀) ≤ (#‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
194191, 193sylibr 224 . . . 4 (𝜑 → (#‘𝑀) ≤ (#‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
195 hashxp 13259 . . . . . 6 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (#‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (#‘(1...(⌊‘(√‘𝑁))))))
19630, 37, 195mp2an 708 . . . . 5 (#‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (#‘(1...(⌊‘(√‘𝑁)))))
197 hashfz1 13174 . . . . . . 7 ((⌊‘(√‘𝑁)) ∈ ℕ0 → (#‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
19822, 197syl 17 . . . . . 6 (𝜑 → (#‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
199198oveq2d 6706 . . . . 5 (𝜑 → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (#‘(1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
200196, 199syl5eq 2697 . . . 4 (𝜑 → (#‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
201194, 200breqtrd 4711 . . 3 (𝜑 → (#‘𝑀) ≤ ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
20233a1i 11 . . . 4 (𝜑 → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ)
20322nn0ge0d 11392 . . . 4 (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
204 prmrec.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
205204, 12, 17, 2, 44prmreclem2 15668 . . . 4 (𝜑 → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
206202, 25, 34, 203, 205lemul1ad 11001 . . 3 (𝜑 → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
20710, 36, 24, 201, 206letrd 10232 . 2 (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
20815nnrpd 11908 . . . 4 (𝜑 → (2↑𝐾) ∈ ℝ+)
209208rprege0d 11917 . . 3 (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
210 fllelt 12638 . . . . 5 ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
21126, 210syl 17 . . . 4 (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
212211simpld 474 . . 3 (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
213 lemul2a 10916 . . 3 ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
21434, 26, 209, 212, 213syl31anc 1369 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
21510, 24, 27, 207, 214letrd 10232 1 (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  {crab 2945   ∖ cdif 3604   ⊆ wss 3607  ifcif 4119  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  ‘cfv 5926  (class class class)co 6690   ≼ cdom 7995  Fincfn 7997  supcsup 8387  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   / cdiv 10722  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  ...cfz 12364  ⌊cfl 12631  ↑cexp 12900  #chash 13157  √csqrt 14017   ∥ cdvds 15027  ℙcprime 15432 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-fz 12365  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589 This theorem is referenced by:  prmreclem5  15671
 Copyright terms: Public domain W3C validator