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

Theorem prmreclem3 16890
Description: Lemma for prmrec 16894. 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 13973 . . . . . 6 (1...𝑁) ∈ Fin
2 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
32ssrab3 4076 . . . . . 6 𝑀 ⊆ (1...𝑁)
4 ssfi 9198 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
51, 3, 4mp2an 690 . . . . 5 𝑀 ∈ Fin
6 hashcl 14351 . . . . 5 (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ0)
75, 6ax-mp 5 . . . 4 (♯‘𝑀) ∈ ℕ0
87nn0rei 12516 . . 3 (♯‘𝑀) ∈ ℝ
98a1i 11 . 2 (𝜑 → (♯‘𝑀) ∈ ℝ)
10 2nn 12318 . . . . . 6 2 ∈ ℕ
11 prmrec.2 . . . . . . 7 (𝜑𝐾 ∈ ℕ)
1211nnnn0d 12565 . . . . . 6 (𝜑𝐾 ∈ ℕ0)
13 nnexpcl 14075 . . . . . 6 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1410, 12, 13sylancr 585 . . . . 5 (𝜑 → (2↑𝐾) ∈ ℕ)
1514nnnn0d 12565 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ0)
16 prmrec.3 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1716nnrpd 13049 . . . . . . 7 (𝜑𝑁 ∈ ℝ+)
1817rpsqrtcld 15394 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
1918rprege0d 13058 . . . . 5 (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20 flge0nn0 13821 . . . . 5 (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ0)
2119, 20syl 17 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ0)
2215, 21nn0mulcld 12570 . . 3 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ0)
2322nn0red 12566 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
2414nnred 12260 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
2518rpred 13051 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2624, 25remulcld 11276 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27 ssrab2 4073 . . . . . . 7 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
28 ssfi 9198 . . . . . . 7 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
295, 27, 28mp2an 690 . . . . . 6 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
30 hashcl 14351 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0)
3129, 30ax-mp 5 . . . . 5 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0
3231nn0rei 12516 . . . 4 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ
3321nn0red 12566 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34 remulcl 11225 . . . 4 (((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
3532, 33, 34sylancr 585 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36 fzfi 13973 . . . . . . 7 (1...(⌊‘(√‘𝑁))) ∈ Fin
37 xpfi 9343 . . . . . . 7 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
3829, 36, 37mp2an 690 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39 fveqeq2 6905 . . . . . . . . . 10 (𝑥 = (𝑦 / ((𝑄𝑦)↑2)) → ((𝑄𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1))
40 simpr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → 𝑦𝑀)
413, 40sselid 3974 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → 𝑦 ∈ (1...𝑁))
42 elfznn 13565 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℕ)
44 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
4544prmreclem1 16888 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
4645simp2d 1140 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → ((𝑄𝑦)↑2) ∥ 𝑦)
4743, 46syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∥ 𝑦)
4845simp1d 1139 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → (𝑄𝑦) ∈ ℕ)
4943, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℕ)
5049nnsqcld 14242 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℕ)
5150nnzd 12618 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℤ)
5250nnne0d 12295 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≠ 0)
5343nnzd 12618 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℤ)
54 dvdsval2 16237 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑦)↑2) ∈ ℤ ∧ ((𝑄𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5551, 52, 53, 54syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5647, 55mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
57 nnre 12252 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58 nngt0 12276 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 0 < 𝑦)
5957, 58jca 510 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60 nnre 12252 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → ((𝑄𝑦)↑2) ∈ ℝ)
61 nngt0 12276 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → 0 < ((𝑄𝑦)↑2))
6260, 61jca 510 . . . . . . . . . . . . . . . . 17 (((𝑄𝑦)↑2) ∈ ℕ → (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2)))
63 divgt0 12115 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2))) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6459, 62, 63syl2an 594 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ ((𝑄𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6543, 50, 64syl2anc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
66 elnnz 12601 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄𝑦)↑2))))
6756, 65, 66sylanbrc 581 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ)
6867nnred 12260 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℝ)
6943nnred 12260 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦 ∈ ℝ)
7016nnred 12260 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
7170adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℝ)
72 dvdsmul1 16258 . . . . . . . . . . . . . . . 16 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ ((𝑄𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7356, 51, 72syl2anc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7443nncnd 12261 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → 𝑦 ∈ ℂ)
7550nncnd 12261 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℂ)
7674, 75, 52divcan1d 12024 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
7773, 76breqtrd 5175 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
78 dvdsle 16290 . . . . . . . . . . . . . . 15 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
7956, 43, 78syl2anc 582 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
8077, 79mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦)
81 elfzle2 13540 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑁) → 𝑦𝑁)
8241, 81syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦𝑁)
8368, 69, 71, 80, 82letrd 11403 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁)
84 nnuz 12898 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8567, 84eleqtrdi 2835 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1))
8616nnzd 12618 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
8786adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℤ)
88 elfz5 13528 . . . . . . . . . . . . 13 (((𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
8985, 87, 88syl2anc 582 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
9083, 89mpbird 256 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁))
91 breq2 5153 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
9291notbid 317 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
9392ralbidv 3167 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9493, 2elrab2 3682 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9540, 94sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9695simprd 494 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
9777adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
98 eldifi 4123 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99 prmz 16649 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101100adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
10256adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
10353adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104 dvdstr 16274 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
105101, 102, 103, 104syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
10697, 105mpan2d 692 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) → 𝑝𝑦))
107106con3d 152 . . . . . . . . . . . . 13 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
108107ralimdva 3156 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
10996, 108mpd 15 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)))
110 breq2 5153 . . . . . . . . . . . . . 14 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (𝑝𝑛𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
111110notbid 317 . . . . . . . . . . . . 13 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (¬ 𝑝𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
112111ralbidv 3167 . . . . . . . . . . . 12 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
113112, 2elrab2 3682 . . . . . . . . . . 11 ((𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
11490, 109, 113sylanbrc 581 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀)
11544prmreclem1 16888 . . . . . . . . . . . . 13 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝐴 ∈ (ℤ‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2)))))
116115simp2d 1140 . . . . . . . . . . . 12 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
11767, 116syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
118115simp1d 1139 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
11967, 118syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
120 elnn1uz2 12942 . . . . . . . . . . . . . 14 ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
121119, 120sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
122121ord 862 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
12344prmreclem1 16888 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
124123simp3d 1141 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
12543, 122, 124sylsyld 61 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
126117, 125mt4d 117 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1)
12739, 114, 126elrabd 3681 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1})
12850nnred 12260 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℝ)
129 dvdsle 16290 . . . . . . . . . . . . . . . 16 ((((𝑄𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13051, 43, 129syl2anc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13147, 130mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑦)
132128, 69, 71, 131, 82letrd 11403 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑁)
13371recnd 11274 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → 𝑁 ∈ ℂ)
134133sqsqrtd 15422 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((√‘𝑁)↑2) = 𝑁)
135132, 134breqtrrd 5177 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2))
13649nnrpd 13049 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℝ+)
13718adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ+)
138 rprege0 13024 . . . . . . . . . . . . . 14 ((𝑄𝑦) ∈ ℝ+ → ((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)))
139 rprege0 13024 . . . . . . . . . . . . . 14 ((√‘𝑁) ∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140 le2sq 14134 . . . . . . . . . . . . . 14 ((((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141138, 139, 140syl2an 594 . . . . . . . . . . . . 13 (((𝑄𝑦) ∈ ℝ+ ∧ (√‘𝑁) ∈ ℝ+) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142136, 137, 141syl2anc 582 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143135, 142mpbird 256 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (√‘𝑁))
14425adantr 479 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ)
14549nnzd 12618 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℤ)
146 flge 13806 . . . . . . . . . . . 12 (((√‘𝑁) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
147144, 145, 146syl2anc 582 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
148143, 147mpbid 231 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (⌊‘(√‘𝑁)))
14949, 84eleqtrdi 2835 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (ℤ‘1))
15021nn0zd 12617 . . . . . . . . . . . 12 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151150adantr 479 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152 elfz5 13528 . . . . . . . . . . 11 (((𝑄𝑦) ∈ (ℤ‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
153149, 151, 152syl2anc 582 . . . . . . . . . 10 ((𝜑𝑦𝑀) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
154148, 153mpbird 256 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155127, 154opelxpd 5717 . . . . . . . 8 ((𝜑𝑦𝑀) → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156155ex 411 . . . . . . 7 (𝜑 → (𝑦𝑀 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157 ovex 7452 . . . . . . . . . . . 12 (𝑦 / ((𝑄𝑦)↑2)) ∈ V
158 fvex 6909 . . . . . . . . . . . 12 (𝑄𝑦) ∈ V
159157, 158opth 5478 . . . . . . . . . . 11 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ ((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)))
160 oveq1 7426 . . . . . . . . . . . 12 ((𝑄𝑦) = (𝑄𝑧) → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
161 oveq12 7428 . . . . . . . . . . . 12 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
162160, 161sylan2 591 . . . . . . . . . . 11 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
163159, 162sylbi 216 . . . . . . . . . 10 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
16476adantrr 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
165 fz1ssnn 13567 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
1663, 165sstri 3986 . . . . . . . . . . . . . 14 𝑀 ⊆ ℕ
167 simprr 771 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧𝑀)
168166, 167sselid 3974 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℕ)
169168nncnd 12261 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℂ)
17044prmreclem1 16888 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → ((𝑄𝑧) ∈ ℕ ∧ ((𝑄𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄𝑧)↑2)))))
171170simp1d 1139 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → (𝑄𝑧) ∈ ℕ)
172168, 171syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (𝑄𝑧) ∈ ℕ)
173172nnsqcld 14242 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℕ)
174173nncnd 12261 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℂ)
175173nnne0d 12295 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ≠ 0)
176169, 174, 175divcan1d 12024 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) = 𝑧)
177164, 176eqeq12d 2741 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) ↔ 𝑦 = 𝑧))
178163, 177imbitrid 243 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → 𝑦 = 𝑧))
179 id 22 . . . . . . . . . . 11 (𝑦 = 𝑧𝑦 = 𝑧)
180 fveq2 6896 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑄𝑦) = (𝑄𝑧))
181180oveq1d 7434 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
182179, 181oveq12d 7437 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)))
183182, 180opeq12d 4883 . . . . . . . . 9 (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩)
184178, 183impbid1 224 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧))
185184ex 411 . . . . . . 7 (𝜑 → ((𝑦𝑀𝑧𝑀) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧)))
186156, 185dom2d 9014 . . . . . 6 (𝜑 → (({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
18738, 186mpi 20 . . . . 5 (𝜑𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188 hashdom 14374 . . . . . 6 ((𝑀 ∈ Fin ∧ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
1895, 38, 188mp2an 690 . . . . 5 ((♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
190187, 189sylibr 233 . . . 4 (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
191 hashxp 14429 . . . . . 6 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
19229, 36, 191mp2an 690 . . . . 5 (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193 hashfz1 14341 . . . . . . 7 ((⌊‘(√‘𝑁)) ∈ ℕ0 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
19421, 193syl 17 . . . . . 6 (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195194oveq2d 7435 . . . . 5 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
196192, 195eqtrid 2777 . . . 4 (𝜑 → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
197190, 196breqtrd 5175 . . 3 (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
19832a1i 11 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ)
19921nn0ge0d 12568 . . . 4 (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200 prmrec.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201200, 11, 16, 2, 44prmreclem2 16889 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
202198, 24, 33, 199, 201lemul1ad 12186 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
2039, 35, 23, 197, 202letrd 11403 . 2 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
20414nnrpd 13049 . . . 4 (𝜑 → (2↑𝐾) ∈ ℝ+)
205204rprege0d 13058 . . 3 (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206 fllelt 13798 . . . . 5 ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
20725, 206syl 17 . . . 4 (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208207simpld 493 . . 3 (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209 lemul2a 12102 . . 3 ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
21033, 25, 205, 208, 209syl31anc 1370 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
2119, 23, 26, 203, 210letrd 11403 1 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wcel 2098  wne 2929  wral 3050  {crab 3418  cdif 3941  wss 3944  ifcif 4530  cop 4636   class class class wbr 5149  cmpt 5232   × cxp 5676  cfv 6549  (class class class)co 7419  cdom 8962  Fincfn 8964  supcsup 9465  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145   < clt 11280  cle 11281   / cdiv 11903  cn 12245  2c2 12300  0cn0 12505  cz 12591  cuz 12855  +crp 13009  ...cfz 13519  cfl 13791  cexp 14062  chash 14325  csqrt 15216  cdvds 16234  cprime 16645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9467  df-inf 9468  df-dju 9926  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-n0 12506  df-xnn0 12578  df-z 12592  df-uz 12856  df-q 12966  df-rp 13010  df-fz 13520  df-fl 13793  df-mod 13871  df-seq 14003  df-exp 14063  df-hash 14326  df-cj 15082  df-re 15083  df-im 15084  df-sqrt 15218  df-abs 15219  df-dvds 16235  df-gcd 16473  df-prm 16646  df-pc 16809
This theorem is referenced by:  prmreclem5  16892
  Copyright terms: Public domain W3C validator