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

Theorem prmreclem3 16956
Description: Lemma for prmrec 16960. 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 14013 . . . . . 6 (1...𝑁) ∈ Fin
2 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
32ssrab3 4082 . . . . . 6 𝑀 ⊆ (1...𝑁)
4 ssfi 9213 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
51, 3, 4mp2an 692 . . . . 5 𝑀 ∈ Fin
6 hashcl 14395 . . . . 5 (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ0)
75, 6ax-mp 5 . . . 4 (♯‘𝑀) ∈ ℕ0
87nn0rei 12537 . . 3 (♯‘𝑀) ∈ ℝ
98a1i 11 . 2 (𝜑 → (♯‘𝑀) ∈ ℝ)
10 2nn 12339 . . . . . 6 2 ∈ ℕ
11 prmrec.2 . . . . . . 7 (𝜑𝐾 ∈ ℕ)
1211nnnn0d 12587 . . . . . 6 (𝜑𝐾 ∈ ℕ0)
13 nnexpcl 14115 . . . . . 6 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1410, 12, 13sylancr 587 . . . . 5 (𝜑 → (2↑𝐾) ∈ ℕ)
1514nnnn0d 12587 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ0)
16 prmrec.3 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
1716nnrpd 13075 . . . . . . 7 (𝜑𝑁 ∈ ℝ+)
1817rpsqrtcld 15450 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
1918rprege0d 13084 . . . . 5 (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20 flge0nn0 13860 . . . . 5 (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ0)
2119, 20syl 17 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ0)
2215, 21nn0mulcld 12592 . . 3 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ0)
2322nn0red 12588 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
2414nnred 12281 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
2518rpred 13077 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2624, 25remulcld 11291 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27 ssrab2 4080 . . . . . . 7 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
28 ssfi 9213 . . . . . . 7 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
295, 27, 28mp2an 692 . . . . . 6 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
30 hashcl 14395 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0)
3129, 30ax-mp 5 . . . . 5 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℕ0
3231nn0rei 12537 . . . 4 (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ
3321nn0red 12588 . . . 4 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34 remulcl 11240 . . . 4 (((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
3532, 33, 34sylancr 587 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36 fzfi 14013 . . . . . . 7 (1...(⌊‘(√‘𝑁))) ∈ Fin
37 xpfi 9358 . . . . . . 7 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
3829, 36, 37mp2an 692 . . . . . 6 ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39 fveqeq2 6915 . . . . . . . . . 10 (𝑥 = (𝑦 / ((𝑄𝑦)↑2)) → ((𝑄𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1))
40 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → 𝑦𝑀)
413, 40sselid 3981 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → 𝑦 ∈ (1...𝑁))
42 elfznn 13593 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℕ)
44 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
4544prmreclem1 16954 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
4645simp2d 1144 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → ((𝑄𝑦)↑2) ∥ 𝑦)
4743, 46syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∥ 𝑦)
4845simp1d 1143 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → (𝑄𝑦) ∈ ℕ)
4943, 48syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℕ)
5049nnsqcld 14283 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℕ)
5150nnzd 12640 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℤ)
5250nnne0d 12316 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≠ 0)
5343nnzd 12640 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑀) → 𝑦 ∈ ℤ)
54 dvdsval2 16293 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑦)↑2) ∈ ℤ ∧ ((𝑄𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5551, 52, 53, 54syl3anc 1373 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ))
5647, 55mpbid 232 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
57 nnre 12273 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58 nngt0 12297 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 0 < 𝑦)
5957, 58jca 511 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60 nnre 12273 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → ((𝑄𝑦)↑2) ∈ ℝ)
61 nngt0 12297 . . . . . . . . . . . . . . . . . 18 (((𝑄𝑦)↑2) ∈ ℕ → 0 < ((𝑄𝑦)↑2))
6260, 61jca 511 . . . . . . . . . . . . . . . . 17 (((𝑄𝑦)↑2) ∈ ℕ → (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2)))
63 divgt0 12136 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄𝑦)↑2))) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6459, 62, 63syl2an 596 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ ((𝑄𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
6543, 50, 64syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → 0 < (𝑦 / ((𝑄𝑦)↑2)))
66 elnnz 12623 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄𝑦)↑2))))
6756, 65, 66sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ)
6867nnred 12281 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℝ)
6943nnred 12281 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦 ∈ ℝ)
7016nnred 12281 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
7170adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℝ)
72 dvdsmul1 16315 . . . . . . . . . . . . . . . 16 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ ((𝑄𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7356, 51, 72syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)))
7443nncnd 12282 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → 𝑦 ∈ ℂ)
7550nncnd 12282 . . . . . . . . . . . . . . . 16 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℂ)
7674, 75, 52divcan1d 12044 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
7773, 76breqtrd 5169 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
78 dvdsle 16347 . . . . . . . . . . . . . . 15 (((𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
7956, 43, 78syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦))
8077, 79mpd 15 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑦)
81 elfzle2 13568 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑁) → 𝑦𝑁)
8241, 81syl 17 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑦𝑁)
8368, 69, 71, 80, 82letrd 11418 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁)
84 nnuz 12921 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8567, 84eleqtrdi 2851 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1))
8616nnzd 12640 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
8786adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → 𝑁 ∈ ℤ)
88 elfz5 13556 . . . . . . . . . . . . 13 (((𝑦 / ((𝑄𝑦)↑2)) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
8985, 87, 88syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄𝑦)↑2)) ≤ 𝑁))
9083, 89mpbird 257 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁))
91 breq2 5147 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
9291notbid 318 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
9392ralbidv 3178 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9493, 2elrab2 3695 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9540, 94sylib 218 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
9695simprd 495 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
9777adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦)
98 eldifi 4131 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99 prmz 16712 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101100adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
10256adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ)
10353adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104 dvdstr 16331 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
105101, 102, 103, 104syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝑦 / ((𝑄𝑦)↑2)) ∥ 𝑦) → 𝑝𝑦))
10697, 105mpan2d 694 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)) → 𝑝𝑦))
107106con3d 152 . . . . . . . . . . . . 13 (((𝜑𝑦𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
108107ralimdva 3167 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
10996, 108mpd 15 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2)))
110 breq2 5147 . . . . . . . . . . . . . 14 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (𝑝𝑛𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
111110notbid 318 . . . . . . . . . . . . 13 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (¬ 𝑝𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
112111ralbidv 3178 . . . . . . . . . . . 12 (𝑛 = (𝑦 / ((𝑄𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
113112, 2elrab2 3695 . . . . . . . . . . 11 ((𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄𝑦)↑2))))
11490, 109, 113sylanbrc 583 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ 𝑀)
11544prmreclem1 16954 . . . . . . . . . . . . 13 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ∧ (𝐴 ∈ (ℤ‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2)))))
116115simp2d 1144 . . . . . . . . . . . 12 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
11767, 116syl 17 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
118115simp1d 1143 . . . . . . . . . . . . . . 15 ((𝑦 / ((𝑄𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
11967, 118syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ)
120 elnn1uz2 12967 . . . . . . . . . . . . . 14 ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
121119, 120sylib 218 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
122121ord 865 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2)))
12344prmreclem1 16954 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2))) ∈ (ℤ‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
124123simp3d 1145 . . . . . . . . . . . 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 3694 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑦 / ((𝑄𝑦)↑2)) ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1})
12850nnred 12281 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ∈ ℝ)
129 dvdsle 16347 . . . . . . . . . . . . . . . 16 ((((𝑄𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13051, 43, 129syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑀) → (((𝑄𝑦)↑2) ∥ 𝑦 → ((𝑄𝑦)↑2) ≤ 𝑦))
13147, 130mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑦)
132128, 69, 71, 131, 82letrd 11418 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ 𝑁)
13371recnd 11289 . . . . . . . . . . . . . 14 ((𝜑𝑦𝑀) → 𝑁 ∈ ℂ)
134133sqsqrtd 15478 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → ((√‘𝑁)↑2) = 𝑁)
135132, 134breqtrrd 5171 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2))
13649nnrpd 13075 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℝ+)
13718adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ+)
138 rprege0 13050 . . . . . . . . . . . . . 14 ((𝑄𝑦) ∈ ℝ+ → ((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)))
139 rprege0 13050 . . . . . . . . . . . . . 14 ((√‘𝑁) ∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140 le2sq 14174 . . . . . . . . . . . . . 14 ((((𝑄𝑦) ∈ ℝ ∧ 0 ≤ (𝑄𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141138, 139, 140syl2an 596 . . . . . . . . . . . . 13 (((𝑄𝑦) ∈ ℝ+ ∧ (√‘𝑁) ∈ ℝ+) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142136, 137, 141syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ ((𝑄𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143135, 142mpbird 257 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (√‘𝑁))
14425adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (√‘𝑁) ∈ ℝ)
14549nnzd 12640 . . . . . . . . . . . 12 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ ℤ)
146 flge 13845 . . . . . . . . . . . 12 (((√‘𝑁) ∈ ℝ ∧ (𝑄𝑦) ∈ ℤ) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
147144, 145, 146syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → ((𝑄𝑦) ≤ (√‘𝑁) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
148143, 147mpbid 232 . . . . . . . . . 10 ((𝜑𝑦𝑀) → (𝑄𝑦) ≤ (⌊‘(√‘𝑁)))
14949, 84eleqtrdi 2851 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (ℤ‘1))
15021nn0zd 12639 . . . . . . . . . . . 12 (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151150adantr 480 . . . . . . . . . . 11 ((𝜑𝑦𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152 elfz5 13556 . . . . . . . . . . 11 (((𝑄𝑦) ∈ (ℤ‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
153149, 151, 152syl2anc 584 . . . . . . . . . 10 ((𝜑𝑦𝑀) → ((𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄𝑦) ≤ (⌊‘(√‘𝑁))))
154148, 153mpbird 257 . . . . . . . . 9 ((𝜑𝑦𝑀) → (𝑄𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155127, 154opelxpd 5724 . . . . . . . 8 ((𝜑𝑦𝑀) → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156155ex 412 . . . . . . 7 (𝜑 → (𝑦𝑀 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ ∈ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157 ovex 7464 . . . . . . . . . . . 12 (𝑦 / ((𝑄𝑦)↑2)) ∈ V
158 fvex 6919 . . . . . . . . . . . 12 (𝑄𝑦) ∈ V
159157, 158opth 5481 . . . . . . . . . . 11 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ ((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)))
160 oveq1 7438 . . . . . . . . . . . 12 ((𝑄𝑦) = (𝑄𝑧) → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
161 oveq12 7440 . . . . . . . . . . . 12 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
162160, 161sylan2 593 . . . . . . . . . . 11 (((𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)) ∧ (𝑄𝑦) = (𝑄𝑧)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
163159, 162sylbi 217 . . . . . . . . . 10 (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)))
16476adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = 𝑦)
165 fz1ssnn 13595 . . . . . . . . . . . . . . 15 (1...𝑁) ⊆ ℕ
1663, 165sstri 3993 . . . . . . . . . . . . . 14 𝑀 ⊆ ℕ
167 simprr 773 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧𝑀)
168166, 167sselid 3981 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℕ)
169168nncnd 12282 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → 𝑧 ∈ ℂ)
17044prmreclem1 16954 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ℕ → ((𝑄𝑧) ∈ ℕ ∧ ((𝑄𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄𝑧)↑2)))))
171170simp1d 1143 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → (𝑄𝑧) ∈ ℕ)
172168, 171syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (𝑄𝑧) ∈ ℕ)
173172nnsqcld 14283 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℕ)
174173nncnd 12282 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ∈ ℂ)
175173nnne0d 12316 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑄𝑧)↑2) ≠ 0)
176169, 174, 175divcan1d 12044 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) = 𝑧)
177164, 176eqeq12d 2753 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (((𝑦 / ((𝑄𝑦)↑2)) · ((𝑄𝑦)↑2)) = ((𝑧 / ((𝑄𝑧)↑2)) · ((𝑄𝑧)↑2)) ↔ 𝑦 = 𝑧))
178163, 177imbitrid 244 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ → 𝑦 = 𝑧))
179 id 22 . . . . . . . . . . 11 (𝑦 = 𝑧𝑦 = 𝑧)
180 fveq2 6906 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑄𝑦) = (𝑄𝑧))
181180oveq1d 7446 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑄𝑦)↑2) = ((𝑄𝑧)↑2))
182179, 181oveq12d 7449 . . . . . . . . . 10 (𝑦 = 𝑧 → (𝑦 / ((𝑄𝑦)↑2)) = (𝑧 / ((𝑄𝑧)↑2)))
183182, 180opeq12d 4881 . . . . . . . . 9 (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩)
184178, 183impbid1 225 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀𝑧𝑀)) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧))
185184ex 412 . . . . . . 7 (𝜑 → ((𝑦𝑀𝑧𝑀) → (⟨(𝑦 / ((𝑄𝑦)↑2)), (𝑄𝑦)⟩ = ⟨(𝑧 / ((𝑄𝑧)↑2)), (𝑄𝑧)⟩ ↔ 𝑦 = 𝑧)))
186156, 185dom2d 9033 . . . . . 6 (𝜑 → (({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
18738, 186mpi 20 . . . . 5 (𝜑𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188 hashdom 14418 . . . . . 6 ((𝑀 ∈ Fin ∧ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
1895, 38, 188mp2an 692 . . . . 5 ((♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
190187, 189sylibr 234 . . . 4 (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
191 hashxp 14473 . . . . . 6 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
19229, 36, 191mp2an 692 . . . . 5 (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193 hashfz1 14385 . . . . . . 7 ((⌊‘(√‘𝑁)) ∈ ℕ0 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
19421, 193syl 17 . . . . . 6 (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195194oveq2d 7447 . . . . 5 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
196192, 195eqtrid 2789 . . . 4 (𝜑 → (♯‘({𝑥𝑀 ∣ (𝑄𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
197190, 196breqtrd 5169 . . 3 (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))))
19832a1i 11 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ∈ ℝ)
19921nn0ge0d 12590 . . . 4 (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200 prmrec.1 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201200, 11, 16, 2, 44prmreclem2 16955 . . . 4 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
202198, 24, 33, 199, 201lemul1ad 12207 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
2039, 35, 23, 197, 202letrd 11418 . 2 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
20414nnrpd 13075 . . . 4 (𝜑 → (2↑𝐾) ∈ ℝ+)
205204rprege0d 13084 . . 3 (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206 fllelt 13837 . . . . 5 ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
20725, 206syl 17 . . . 4 (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208207simpld 494 . . 3 (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209 lemul2a 12122 . . 3 ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
21033, 25, 205, 208, 209syl31anc 1375 . 2 (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
2119, 23, 26, 203, 210letrd 11418 1 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  wral 3061  {crab 3436  cdif 3948  wss 3951  ifcif 4525  cop 4632   class class class wbr 5143  cmpt 5225   × cxp 5683  cfv 6561  (class class class)co 7431  cdom 8983  Fincfn 8985  supcsup 9480  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296   / cdiv 11920  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  +crp 13034  ...cfz 13547  cfl 13830  cexp 14102  chash 14369  csqrt 15272  cdvds 16290  cprime 16708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-fz 13548  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875
This theorem is referenced by:  prmreclem5  16958
  Copyright terms: Public domain W3C validator