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

Theorem prmreclem3 16790
Description: Lemma for prmrec 16794. 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 13877 . . . . . 6 (1...𝑁) ∈ Fin
2 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
32ssrab3 4040 . . . . . 6 𝑀 ⊆ (1...𝑁)
4 ssfi 9117 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
51, 3, 4mp2an 690 . . . . 5 𝑀 ∈ Fin
6 hashcl 14256 . . . . 5 (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ0)
75, 6ax-mp 5 . . . 4 (♯‘𝑀) ∈ ℕ0
87nn0rei 12424 . . 3 (♯‘𝑀) ∈ ℝ
98a1i 11 . 2 (𝜑 → (♯‘𝑀) ∈ ℝ)
10 2nn 12226 . . . . . 6 2 ∈ ℕ
11 prmrec.2 . . . . . . 7 (𝜑𝐾 ∈ ℕ)
1211nnnn0d 12473 . . . . . 6 (𝜑𝐾 ∈ ℕ0)
13 nnexpcl 13980 . . . . . 6 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1410, 12, 13sylancr 587 . . . . 5 (𝜑 → (2↑𝐾) ∈ ℕ)
1514nnnn0d 12473 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ0)
16 prmrec.3 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1716nnrpd 12955 . . . . . . 7 (𝜑𝑁 ∈ ℝ+)
1817rpsqrtcld 15296 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
1918rprege0d 12964 . . . . 5 (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20 flge0nn0 13725 . . . . 5 (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ0)
2119, 20syl 17 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ0)
2215, 21nn0mulcld 12478 . . 3 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ0)
2322nn0red 12474 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
2414nnred 12168 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
2518rpred 12957 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2624, 25remulcld 11185 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27 ssrab2 4037 . . . . . . 7 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
28 ssfi 9117 . . . . . . 7 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
295, 27, 28mp2an 690 . . . . . 6 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
30 hashcl 14256 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0)
3129, 30ax-mp 5 . . . . 5 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0
3231nn0rei 12424 . . . 4 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ
3321nn0red 12474 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34 remulcl 11136 . . . 4 (((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
3532, 33, 34sylancr 587 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36 fzfi 13877 . . . . . . 7 (1...(⌊‘(√‘𝑁))) ∈ Fin
37 xpfi 9261 . . . . . . 7 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
3829, 36, 37mp2an 690 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39 fveqeq2 6851 . . . . . . . . . 10 (𝑥 = (𝑦 / ((𝑄𝑦)↑2)) → ((𝑄𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1))
40 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → 𝑦𝑀)
413, 40sselid 3942 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → 𝑦 ∈ (1...𝑁))
42 elfznn 13470 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℕ)
44 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
4544prmreclem1 16788 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
4645simp2d 1143 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → ((𝑄𝑦)↑2) ∥ 𝑦)
4743, 46syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∥ 𝑦)
4845simp1d 1142 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → (𝑄𝑦) ∈ ℕ)
4943, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℕ)
5049nnsqcld 14147 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℕ)
5150nnzd 12526 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℤ)
5250nnne0d 12203 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≠ 0)
5343nnzd 12526 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℤ)
54 dvdsval2 16139 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑦)↑2) ∈ ℤ ∧ ((𝑄𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5551, 52, 53, 54syl3anc 1371 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5647, 55mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
57 nnre 12160 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58 nngt0 12184 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 0 < 𝑦)
5957, 58jca 512 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60 nnre 12160 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → ((𝑄𝑦)↑2) ∈ ℝ)
61 nngt0 12184 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → 0 < ((𝑄𝑦)↑2))
6260, 61jca 512 . . . . . . . . . . . . . . . . 17 (((𝑄𝑦)↑2) ∈ ℕ → (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2)))
63 divgt0 12023 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2))) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6459, 62, 63syl2an 596 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ ((𝑄𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6543, 50, 64syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
66 elnnz 12509 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄𝑦)↑2))))
6756, 65, 66sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ)
6867nnred 12168 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℝ)
6943nnred 12168 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦 ∈ ℝ)
7016nnred 12168 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
7170adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℝ)
72 dvdsmul1 16160 . . . . . . . . . . . . . . . 16 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ ((𝑄𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7356, 51, 72syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7443nncnd 12169 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → 𝑦 ∈ ℂ)
7550nncnd 12169 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℂ)
7674, 75, 52divcan1d 11932 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
7773, 76breqtrd 5131 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
78 dvdsle 16192 . . . . . . . . . . . . . . 15 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
7956, 43, 78syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
8077, 79mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦)
81 elfzle2 13445 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑁) → 𝑦𝑁)
8241, 81syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦𝑁)
8368, 69, 71, 80, 82letrd 11312 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁)
84 nnuz 12806 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8567, 84eleqtrdi 2848 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1))
8616nnzd 12526 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
8786adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℤ)
88 elfz5 13433 . . . . . . . . . . . . 13 (((𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
8985, 87, 88syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
9083, 89mpbird 256 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁))
91 breq2 5109 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
9291notbid 317 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
9392ralbidv 3174 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9493, 2elrab2 3648 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9540, 94sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9695simprd 496 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
9777adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
98 eldifi 4086 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99 prmz 16551 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101100adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
10256adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
10353adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104 dvdstr 16176 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
105101, 102, 103, 104syl3anc 1371 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
10697, 105mpan2d 692 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) → 𝑝𝑦))
107106con3d 152 . . . . . . . . . . . . 13 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
108107ralimdva 3164 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
10996, 108mpd 15 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)))
110 breq2 5109 . . . . . . . . . . . . . 14 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (𝑝𝑛𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
111110notbid 317 . . . . . . . . . . . . 13 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (¬ 𝑝𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
112111ralbidv 3174 . . . . . . . . . . . 12 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
113112, 2elrab2 3648 . . . . . . . . . . 11 ((𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
11490, 109, 113sylanbrc 583 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀)
11544prmreclem1 16788 . . . . . . . . . . . . 13 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝐴 ∈ (ℤ‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2)))))
116115simp2d 1143 . . . . . . . . . . . 12 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
11767, 116syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
118115simp1d 1142 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
11967, 118syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
120 elnn1uz2 12850 . . . . . . . . . . . . . 14 ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
121119, 120sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
122121ord 862 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
12344prmreclem1 16788 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
124123simp3d 1144 . . . . . . . . . . . 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 3647 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1})
12850nnred 12168 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℝ)
129 dvdsle 16192 . . . . . . . . . . . . . . . 16 ((((𝑄𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13051, 43, 129syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13147, 130mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑦)
132128, 69, 71, 131, 82letrd 11312 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑁)
13371recnd 11183 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → 𝑁 ∈ ℂ)
134133sqsqrtd 15324 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((√‘𝑁)↑2) = 𝑁)
135132, 134breqtrrd 5133 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2))
13649nnrpd 12955 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℝ+)
13718adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ+)
138 rprege0 12930 . . . . . . . . . . . . . 14 ((𝑄𝑦) ∈ ℝ+ → ((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)))
139 rprege0 12930 . . . . . . . . . . . . . 14 ((√‘𝑁) ∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140 le2sq 14039 . . . . . . . . . . . . . 14 ((((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141138, 139, 140syl2an 596 . . . . . . . . . . . . 13 (((𝑄𝑦) ∈ ℝ+ ∧ (√‘𝑁) ∈ ℝ+) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142136, 137, 141syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143135, 142mpbird 256 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (√‘𝑁))
14425adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ)
14549nnzd 12526 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℤ)
146 flge 13710 . . . . . . . . . . . 12 (((√‘𝑁) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
147144, 145, 146syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
148143, 147mpbid 231 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (⌊‘(√‘𝑁)))
14949, 84eleqtrdi 2848 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (ℤ‘1))
15021nn0zd 12525 . . . . . . . . . . . 12 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151150adantr 481 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152 elfz5 13433 . . . . . . . . . . 11 (((𝑄𝑦) ∈ (ℤ‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
153149, 151, 152syl2anc 584 . . . . . . . . . 10 ((𝜑𝑦𝑀) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
154148, 153mpbird 256 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155127, 154opelxpd 5671 . . . . . . . 8 ((𝜑𝑦𝑀) → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156155ex 413 . . . . . . 7 (𝜑 → (𝑦𝑀 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157 ovex 7390 . . . . . . . . . . . 12 (𝑦 / ((𝑄𝑦)↑2)) ∈ V
158 fvex 6855 . . . . . . . . . . . 12 (𝑄𝑦) ∈ V
159157, 158opth 5433 . . . . . . . . . . 11 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ ((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)))
160 oveq1 7364 . . . . . . . . . . . 12 ((𝑄𝑦) = (𝑄𝑧) → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
161 oveq12 7366 . . . . . . . . . . . 12 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
162160, 161sylan2 593 . . . . . . . . . . 11 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
163159, 162sylbi 216 . . . . . . . . . 10 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
16476adantrr 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
165 fz1ssnn 13472 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
1663, 165sstri 3953 . . . . . . . . . . . . . 14 𝑀 ⊆ ℕ
167 simprr 771 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧𝑀)
168166, 167sselid 3942 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℕ)
169168nncnd 12169 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℂ)
17044prmreclem1 16788 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → ((𝑄𝑧) ∈ ℕ ∧ ((𝑄𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄𝑧)↑2)))))
171170simp1d 1142 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → (𝑄𝑧) ∈ ℕ)
172168, 171syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (𝑄𝑧) ∈ ℕ)
173172nnsqcld 14147 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℕ)
174173nncnd 12169 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℂ)
175173nnne0d 12203 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ≠ 0)
176169, 174, 175divcan1d 11932 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) = 𝑧)
177164, 176eqeq12d 2752 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) ↔ 𝑦 = 𝑧))
178163, 177imbitrid 243 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → 𝑦 = 𝑧))
179 id 22 . . . . . . . . . . 11 (𝑦 = 𝑧𝑦 = 𝑧)
180 fveq2 6842 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑄𝑦) = (𝑄𝑧))
181180oveq1d 7372 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
182179, 181oveq12d 7375 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)))
183182, 180opeq12d 4838 . . . . . . . . 9 (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩)
184178, 183impbid1 224 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧))
185184ex 413 . . . . . . 7 (𝜑 → ((𝑦𝑀𝑧𝑀) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧)))
186156, 185dom2d 8933 . . . . . 6 (𝜑 → (({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
18738, 186mpi 20 . . . . 5 (𝜑𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188 hashdom 14279 . . . . . 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 14334 . . . . . 6 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
19229, 36, 191mp2an 690 . . . . 5 (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193 hashfz1 14246 . . . . . . 7 ((⌊‘(√‘𝑁)) ∈ ℕ0 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
19421, 193syl 17 . . . . . 6 (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195194oveq2d 7373 . . . . 5 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
196192, 195eqtrid 2788 . . . 4 (𝜑 → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
197190, 196breqtrd 5131 . . 3 (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
19832a1i 11 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ)
19921nn0ge0d 12476 . . . 4 (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200 prmrec.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201200, 11, 16, 2, 44prmreclem2 16789 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
202198, 24, 33, 199, 201lemul1ad 12094 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
2039, 35, 23, 197, 202letrd 11312 . 2 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
20414nnrpd 12955 . . . 4 (𝜑 → (2↑𝐾) ∈ ℝ+)
205204rprege0d 12964 . . 3 (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206 fllelt 13702 . . . . 5 ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
20725, 206syl 17 . . . 4 (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208207simpld 495 . . 3 (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209 lemul2a 12010 . . 3 ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
21033, 25, 205, 208, 209syl31anc 1373 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
2119, 23, 26, 203, 210letrd 11312 1 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2943  wral 3064  {crab 3407  cdif 3907  wss 3910  ifcif 4486  cop 4592   class class class wbr 5105  cmpt 5188   × cxp 5631  cfv 6496  (class class class)co 7357  cdom 8881  Fincfn 8883  supcsup 9376  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cz 12499  cuz 12763  +crp 12915  ...cfz 13424  cfl 13695  cexp 13967  chash 14230  csqrt 15118  cdvds 16136  cprime 16547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-fz 13425  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-dvds 16137  df-gcd 16375  df-prm 16548  df-pc 16709
This theorem is referenced by:  prmreclem5  16792
  Copyright terms: Public domain W3C validator