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

Theorem prmreclem3 16026
Description: Lemma for prmrec 16030. 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 13090 . . . . . 6 (1...𝑁) ∈ Fin
2 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
32ssrab3 3909 . . . . . 6 𝑀 ⊆ (1...𝑁)
4 ssfi 8468 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
51, 3, 4mp2an 682 . . . . 5 𝑀 ∈ Fin
6 hashcl 13462 . . . . 5 (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ0)
75, 6ax-mp 5 . . . 4 (♯‘𝑀) ∈ ℕ0
87nn0rei 11654 . . 3 (♯‘𝑀) ∈ ℝ
98a1i 11 . 2 (𝜑 → (♯‘𝑀) ∈ ℝ)
10 2nn 11448 . . . . . 6 2 ∈ ℕ
11 prmrec.2 . . . . . . 7 (𝜑𝐾 ∈ ℕ)
1211nnnn0d 11702 . . . . . 6 (𝜑𝐾 ∈ ℕ0)
13 nnexpcl 13191 . . . . . 6 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1410, 12, 13sylancr 581 . . . . 5 (𝜑 → (2↑𝐾) ∈ ℕ)
1514nnnn0d 11702 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ0)
16 prmrec.3 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1716nnrpd 12179 . . . . . . 7 (𝜑𝑁 ∈ ℝ+)
1817rpsqrtcld 14558 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
1918rprege0d 12188 . . . . 5 (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20 flge0nn0 12940 . . . . 5 (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ0)
2119, 20syl 17 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ0)
2215, 21nn0mulcld 11707 . . 3 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ0)
2322nn0red 11703 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
2414nnred 11391 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
2518rpred 12181 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2624, 25remulcld 10407 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27 ssrab2 3908 . . . . . . 7 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
28 ssfi 8468 . . . . . . 7 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
295, 27, 28mp2an 682 . . . . . 6 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
30 hashcl 13462 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0)
3129, 30ax-mp 5 . . . . 5 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0
3231nn0rei 11654 . . . 4 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ
3321nn0red 11703 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34 remulcl 10357 . . . 4 (((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
3532, 33, 34sylancr 581 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36 fzfi 13090 . . . . . . 7 (1...(⌊‘(√‘𝑁))) ∈ Fin
37 xpfi 8519 . . . . . . 7 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
3829, 36, 37mp2an 682 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39 fveqeq2 6455 . . . . . . . . . 10 (𝑥 = (𝑦 / ((𝑄𝑦)↑2)) → ((𝑄𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1))
40 simpr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → 𝑦𝑀)
413, 40sseldi 3819 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → 𝑦 ∈ (1...𝑁))
42 elfznn 12687 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℕ)
44 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
4544prmreclem1 16024 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
4645simp2d 1134 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → ((𝑄𝑦)↑2) ∥ 𝑦)
4743, 46syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∥ 𝑦)
4845simp1d 1133 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → (𝑄𝑦) ∈ ℕ)
4943, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℕ)
5049nnsqcld 13350 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℕ)
5150nnzd 11833 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℤ)
5250nnne0d 11425 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≠ 0)
5343nnzd 11833 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℤ)
54 dvdsval2 15390 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑦)↑2) ∈ ℤ ∧ ((𝑄𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5551, 52, 53, 54syl3anc 1439 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5647, 55mpbid 224 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
57 nnre 11382 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58 nngt0 11407 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 0 < 𝑦)
5957, 58jca 507 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60 nnre 11382 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → ((𝑄𝑦)↑2) ∈ ℝ)
61 nngt0 11407 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → 0 < ((𝑄𝑦)↑2))
6260, 61jca 507 . . . . . . . . . . . . . . . . 17 (((𝑄𝑦)↑2) ∈ ℕ → (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2)))
63 divgt0 11245 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2))) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6459, 62, 63syl2an 589 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ ((𝑄𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6543, 50, 64syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
66 elnnz 11738 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄𝑦)↑2))))
6756, 65, 66sylanbrc 578 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ)
6867nnred 11391 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℝ)
6943nnred 11391 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦 ∈ ℝ)
7016nnred 11391 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
7170adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℝ)
72 dvdsmul1 15410 . . . . . . . . . . . . . . . 16 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ ((𝑄𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7356, 51, 72syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7443nncnd 11392 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → 𝑦 ∈ ℂ)
7550nncnd 11392 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℂ)
7674, 75, 52divcan1d 11152 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
7773, 76breqtrd 4912 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
78 dvdsle 15439 . . . . . . . . . . . . . . 15 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
7956, 43, 78syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
8077, 79mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦)
81 elfzle2 12662 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑁) → 𝑦𝑁)
8241, 81syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦𝑁)
8368, 69, 71, 80, 82letrd 10533 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁)
84 nnuz 12029 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8567, 84syl6eleq 2869 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1))
8616nnzd 11833 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
8786adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℤ)
88 elfz5 12651 . . . . . . . . . . . . 13 (((𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
8985, 87, 88syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
9083, 89mpbird 249 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁))
91 breq2 4890 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
9291notbid 310 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
9392ralbidv 3168 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9493, 2elrab2 3576 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9540, 94sylib 210 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9695simprd 491 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
9777adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
98 eldifi 3955 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99 prmz 15794 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101100adantl 475 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
10256adantr 474 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
10353adantr 474 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104 dvdstr 15425 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
105101, 102, 103, 104syl3anc 1439 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
10697, 105mpan2d 684 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) → 𝑝𝑦))
107106con3d 150 . . . . . . . . . . . . 13 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
108107ralimdva 3144 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
10996, 108mpd 15 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)))
110 breq2 4890 . . . . . . . . . . . . . 14 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (𝑝𝑛𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
111110notbid 310 . . . . . . . . . . . . 13 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (¬ 𝑝𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
112111ralbidv 3168 . . . . . . . . . . . 12 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
113112, 2elrab2 3576 . . . . . . . . . . 11 ((𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
11490, 109, 113sylanbrc 578 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀)
11544prmreclem1 16024 . . . . . . . . . . . . 13 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝐴 ∈ (ℤ‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2)))))
116115simp2d 1134 . . . . . . . . . . . 12 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
11767, 116syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
118115simp1d 1133 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
11967, 118syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
120 elnn1uz2 12072 . . . . . . . . . . . . . 14 ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
121119, 120sylib 210 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
122121ord 853 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
12344prmreclem1 16024 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
124123simp3d 1135 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
12543, 122, 124sylsyld 61 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
126117, 125mt4d 154 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1)
12739, 114, 126elrabd 3575 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1})
12850nnred 11391 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℝ)
129 dvdsle 15439 . . . . . . . . . . . . . . . 16 ((((𝑄𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13051, 43, 129syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13147, 130mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑦)
132128, 69, 71, 131, 82letrd 10533 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑁)
13371recnd 10405 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → 𝑁 ∈ ℂ)
134133sqsqrtd 14586 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((√‘𝑁)↑2) = 𝑁)
135132, 134breqtrrd 4914 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2))
13649nnrpd 12179 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℝ+)
13718adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ+)
138 rprege0 12154 . . . . . . . . . . . . . 14 ((𝑄𝑦) ∈ ℝ+ → ((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)))
139 rprege0 12154 . . . . . . . . . . . . . 14 ((√‘𝑁) ∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140 le2sq 13257 . . . . . . . . . . . . . 14 ((((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141138, 139, 140syl2an 589 . . . . . . . . . . . . 13 (((𝑄𝑦) ∈ ℝ+ ∧ (√‘𝑁) ∈ ℝ+) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142136, 137, 141syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143135, 142mpbird 249 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (√‘𝑁))
14425adantr 474 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ)
14549nnzd 11833 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℤ)
146 flge 12925 . . . . . . . . . . . 12 (((√‘𝑁) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
147144, 145, 146syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
148143, 147mpbid 224 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (⌊‘(√‘𝑁)))
14949, 84syl6eleq 2869 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (ℤ‘1))
15021nn0zd 11832 . . . . . . . . . . . 12 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151150adantr 474 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152 elfz5 12651 . . . . . . . . . . 11 (((𝑄𝑦) ∈ (ℤ‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
153149, 151, 152syl2anc 579 . . . . . . . . . 10 ((𝜑𝑦𝑀) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
154148, 153mpbird 249 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155127, 154opelxpd 5393 . . . . . . . 8 ((𝜑𝑦𝑀) → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156155ex 403 . . . . . . 7 (𝜑 → (𝑦𝑀 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157 ovex 6954 . . . . . . . . . . . 12 (𝑦 / ((𝑄𝑦)↑2)) ∈ V
158 fvex 6459 . . . . . . . . . . . 12 (𝑄𝑦) ∈ V
159157, 158opth 5176 . . . . . . . . . . 11 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ ((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)))
160 oveq1 6929 . . . . . . . . . . . 12 ((𝑄𝑦) = (𝑄𝑧) → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
161 oveq12 6931 . . . . . . . . . . . 12 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
162160, 161sylan2 586 . . . . . . . . . . 11 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
163159, 162sylbi 209 . . . . . . . . . 10 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
16476adantrr 707 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
165 fz1ssnn 12689 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
1663, 165sstri 3830 . . . . . . . . . . . . . 14 𝑀 ⊆ ℕ
167 simprr 763 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧𝑀)
168166, 167sseldi 3819 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℕ)
169168nncnd 11392 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℂ)
17044prmreclem1 16024 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → ((𝑄𝑧) ∈ ℕ ∧ ((𝑄𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄𝑧)↑2)))))
171170simp1d 1133 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → (𝑄𝑧) ∈ ℕ)
172168, 171syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (𝑄𝑧) ∈ ℕ)
173172nnsqcld 13350 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℕ)
174173nncnd 11392 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℂ)
175173nnne0d 11425 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ≠ 0)
176169, 174, 175divcan1d 11152 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) = 𝑧)
177164, 176eqeq12d 2793 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) ↔ 𝑦 = 𝑧))
178163, 177syl5ib 236 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → 𝑦 = 𝑧))
179 id 22 . . . . . . . . . . 11 (𝑦 = 𝑧𝑦 = 𝑧)
180 fveq2 6446 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑄𝑦) = (𝑄𝑧))
181180oveq1d 6937 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
182179, 181oveq12d 6940 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)))
183182, 180opeq12d 4644 . . . . . . . . 9 (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩)
184178, 183impbid1 217 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧))
185184ex 403 . . . . . . 7 (𝜑 → ((𝑦𝑀𝑧𝑀) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧)))
186156, 185dom2d 8282 . . . . . 6 (𝜑 → (({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
18738, 186mpi 20 . . . . 5 (𝜑𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188 hashdom 13483 . . . . . 6 ((𝑀 ∈ Fin ∧ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
1895, 38, 188mp2an 682 . . . . 5 ((♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
190187, 189sylibr 226 . . . 4 (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
191 hashxp 13535 . . . . . 6 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
19229, 36, 191mp2an 682 . . . . 5 (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193 hashfz1 13451 . . . . . . 7 ((⌊‘(√‘𝑁)) ∈ ℕ0 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
19421, 193syl 17 . . . . . 6 (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195194oveq2d 6938 . . . . 5 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
196192, 195syl5eq 2826 . . . 4 (𝜑 → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
197190, 196breqtrd 4912 . . 3 (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
19832a1i 11 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ)
19921nn0ge0d 11705 . . . 4 (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200 prmrec.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201200, 11, 16, 2, 44prmreclem2 16025 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
202198, 24, 33, 199, 201lemul1ad 11317 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
2039, 35, 23, 197, 202letrd 10533 . 2 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
20414nnrpd 12179 . . . 4 (𝜑 → (2↑𝐾) ∈ ℝ+)
205204rprege0d 12188 . . 3 (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206 fllelt 12917 . . . . 5 ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
20725, 206syl 17 . . . 4 (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208207simpld 490 . . 3 (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209 lemul2a 11232 . . 3 ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
21033, 25, 205, 208, 209syl31anc 1441 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
2119, 23, 26, 203, 210letrd 10533 1 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 836   = wceq 1601  wcel 2107  wne 2969  wral 3090  {crab 3094  cdif 3789  wss 3792  ifcif 4307  cop 4404   class class class wbr 4886  cmpt 4965   × cxp 5353  cfv 6135  (class class class)co 6922  cdom 8239  Fincfn 8241  supcsup 8634  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277   < clt 10411  cle 10412   / cdiv 11032  cn 11374  2c2 11430  0cn0 11642  cz 11728  cuz 11992  +crp 12137  ...cfz 12643  cfl 12910  cexp 13178  chash 13435  csqrt 14380  cdvds 15387  cprime 15790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-q 12096  df-rp 12138  df-fz 12644  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-dvds 15388  df-gcd 15623  df-prm 15791  df-pc 15946
This theorem is referenced by:  prmreclem5  16028
  Copyright terms: Public domain W3C validator