| Step | Hyp | Ref
| Expression |
| 1 | | fzfi 14013 |
. . . . . 6
⊢
(1...𝑁) ∈
Fin |
| 2 | | prmrec.4 |
. . . . . . 7
⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} |
| 3 | 2 | ssrab3 4082 |
. . . . . 6
⊢ 𝑀 ⊆ (1...𝑁) |
| 4 | | ssfi 9213 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin) |
| 5 | 1, 3, 4 | mp2an 692 |
. . . . 5
⊢ 𝑀 ∈ Fin |
| 6 | | hashcl 14395 |
. . . . 5
⊢ (𝑀 ∈ Fin →
(♯‘𝑀) ∈
ℕ0) |
| 7 | 5, 6 | ax-mp 5 |
. . . 4
⊢
(♯‘𝑀)
∈ ℕ0 |
| 8 | 7 | nn0rei 12537 |
. . 3
⊢
(♯‘𝑀)
∈ ℝ |
| 9 | 8 | a1i 11 |
. 2
⊢ (𝜑 → (♯‘𝑀) ∈
ℝ) |
| 10 | | 2nn 12339 |
. . . . . 6
⊢ 2 ∈
ℕ |
| 11 | | prmrec.2 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 12 | 11 | nnnn0d 12587 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 13 | | nnexpcl 14115 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝐾
∈ ℕ0) → (2↑𝐾) ∈ ℕ) |
| 14 | 10, 12, 13 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (2↑𝐾) ∈ ℕ) |
| 15 | 14 | nnnn0d 12587 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈
ℕ0) |
| 16 | | prmrec.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 17 | 16 | nnrpd 13075 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
| 18 | 17 | rpsqrtcld 15450 |
. . . . . 6
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
| 19 | 18 | rprege0d 13084 |
. . . . 5
⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤
(√‘𝑁))) |
| 20 | | flge0nn0 13860 |
. . . . 5
⊢
(((√‘𝑁)
∈ ℝ ∧ 0 ≤ (√‘𝑁)) →
(⌊‘(√‘𝑁)) ∈
ℕ0) |
| 21 | 19, 20 | syl 17 |
. . . 4
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ∈
ℕ0) |
| 22 | 15, 21 | nn0mulcld 12592 |
. . 3
⊢ (𝜑 → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ∈
ℕ0) |
| 23 | 22 | nn0red 12588 |
. 2
⊢ (𝜑 → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ∈ ℝ) |
| 24 | 14 | nnred 12281 |
. . 3
⊢ (𝜑 → (2↑𝐾) ∈ ℝ) |
| 25 | 18 | rpred 13077 |
. . 3
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
| 26 | 24, 25 | remulcld 11291 |
. 2
⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ) |
| 27 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀 |
| 28 | | ssfi 9213 |
. . . . . . 7
⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin) |
| 29 | 5, 27, 28 | mp2an 692 |
. . . . . 6
⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin |
| 30 | | hashcl 14395 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin →
(♯‘{𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1}) ∈
ℕ0) |
| 31 | 29, 30 | ax-mp 5 |
. . . . 5
⊢
(♯‘{𝑥
∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈
ℕ0 |
| 32 | 31 | nn0rei 12537 |
. . . 4
⊢
(♯‘{𝑥
∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ |
| 33 | 21 | nn0red 12588 |
. . . 4
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ∈ ℝ) |
| 34 | | remulcl 11240 |
. . . 4
⊢
(((♯‘{𝑥
∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧
(⌊‘(√‘𝑁)) ∈ ℝ) →
((♯‘{𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁))) ∈ ℝ) |
| 35 | 32, 33, 34 | sylancr 587 |
. . 3
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁))) ∈ ℝ) |
| 36 | | fzfi 14013 |
. . . . . . 7
⊢
(1...(⌊‘(√‘𝑁))) ∈ Fin |
| 37 | | xpfi 9358 |
. . . . . . 7
⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧
(1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin) |
| 38 | 29, 36, 37 | mp2an 692 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin |
| 39 | | fveqeq2 6915 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1)) |
| 40 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀) |
| 41 | 3, 40 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁)) |
| 42 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ) |
| 44 | | prmreclem2.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, <
)) |
| 45 | 44 | prmreclem1 16954 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ≥‘2)
→ ¬ (𝑛↑2)
∥ (𝑦 / ((𝑄‘𝑦)↑2))))) |
| 46 | 45 | simp2d 1144 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦) |
| 47 | 43, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦) |
| 48 | 45 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ) |
| 49 | 43, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ) |
| 50 | 49 | nnsqcld 14283 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ) |
| 51 | 50 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ) |
| 52 | 50 | nnne0d 12316 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0) |
| 53 | 43 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ) |
| 54 | | dvdsval2 16293 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)) |
| 55 | 51, 52, 53, 54 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)) |
| 56 | 47, 55 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ) |
| 57 | | nnre 12273 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
| 58 | | nngt0 12297 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
| 59 | 57, 58 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 <
𝑦)) |
| 60 | | nnre 12273 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ) |
| 61 | | nngt0 12297 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 <
((𝑄‘𝑦)↑2)) |
| 62 | 60, 61 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) |
| 63 | | divgt0 12136 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℝ ∧ 0 <
𝑦) ∧ (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) → 0 < (𝑦 / ((𝑄‘𝑦)↑2))) |
| 64 | 59, 62, 63 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∈ ℕ) → 0 <
(𝑦 / ((𝑄‘𝑦)↑2))) |
| 65 | 43, 50, 64 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 0 < (𝑦 / ((𝑄‘𝑦)↑2))) |
| 66 | | elnnz 12623 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 67 | 56, 65, 66 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ) |
| 68 | 67 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ) |
| 69 | 43 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ) |
| 70 | 16 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ) |
| 72 | | dvdsmul1 16315 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2))) |
| 73 | 56, 51, 72 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2))) |
| 74 | 43 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ) |
| 75 | 50 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ) |
| 76 | 74, 75, 52 | divcan1d 12044 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦) |
| 77 | 73, 76 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) |
| 78 | | dvdsle 16347 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)) |
| 79 | 56, 43, 78 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)) |
| 80 | 77, 79 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦) |
| 81 | | elfzle2 13568 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁) |
| 82 | 41, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁) |
| 83 | 68, 69, 71, 80, 82 | letrd 11418 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁) |
| 84 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 85 | 67, 84 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈
(ℤ≥‘1)) |
| 86 | 16 | nnzd 12640 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 87 | 86 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ) |
| 88 | | elfz5 13556 |
. . . . . . . . . . . . 13
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)) |
| 89 | 85, 87, 88 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)) |
| 90 | 83, 89 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁)) |
| 91 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦)) |
| 92 | 91 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦)) |
| 93 | 92 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)) |
| 94 | 93, 2 | elrab2 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)) |
| 95 | 40, 94 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)) |
| 96 | 95 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦) |
| 97 | 77 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) |
| 98 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ (ℙ ∖
(1...𝐾)) → 𝑝 ∈
ℙ) |
| 99 | | prmz 16712 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
| 100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ (ℙ ∖
(1...𝐾)) → 𝑝 ∈
ℤ) |
| 101 | 100 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ) |
| 102 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ) |
| 103 | 53 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ) |
| 104 | | dvdstr 16331 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦)) |
| 105 | 101, 102,
103, 104 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦)) |
| 106 | 97, 105 | mpan2d 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) → 𝑝 ∥ 𝑦)) |
| 107 | 106 | con3d 152 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 108 | 107 | ralimdva 3167 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 109 | 96, 108 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))) |
| 110 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 111 | 110 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 112 | 111 | ralbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 113 | 112, 2 | elrab2 3695 |
. . . . . . . . . . 11
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 114 | 90, 109, 113 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀) |
| 115 | 44 | prmreclem1 16954 |
. . . . . . . . . . . . 13
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ≥‘2)
→ ¬ (𝐴↑2)
∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2))))) |
| 116 | 115 | simp2d 1144 |
. . . . . . . . . . . 12
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))) |
| 117 | 67, 116 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))) |
| 118 | 115 | simp1d 1143 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ) |
| 119 | 67, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ) |
| 120 | | elnn1uz2 12967 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2))) |
| 121 | 119, 120 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2))) |
| 122 | 121 | ord 865 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2))) |
| 123 | 44 | prmreclem1 16954 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))) |
| 124 | 123 | simp3d 1145 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 125 | 43, 122, 124 | sylsyld 61 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
| 126 | 117, 125 | mt4d 117 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1) |
| 127 | 39, 114, 126 | elrabd 3694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) |
| 128 | 50 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ) |
| 129 | | dvdsle 16347 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦)) |
| 130 | 51, 43, 129 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦)) |
| 131 | 47, 130 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑦) |
| 132 | 128, 69, 71, 131, 82 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁) |
| 133 | 71 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ) |
| 134 | 133 | sqsqrtd 15478 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁) |
| 135 | 132, 134 | breqtrrd 5171 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)) |
| 136 | 49 | nnrpd 13075 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈
ℝ+) |
| 137 | 18 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈
ℝ+) |
| 138 | | rprege0 13050 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘𝑦) ∈ ℝ+ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦))) |
| 139 | | rprege0 13050 |
. . . . . . . . . . . . . 14
⊢
((√‘𝑁)
∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤
(√‘𝑁))) |
| 140 | | le2sq 14174 |
. . . . . . . . . . . . . 14
⊢ ((((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤
(√‘𝑁))) →
((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))) |
| 141 | 138, 139,
140 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘𝑦) ∈ ℝ+ ∧
(√‘𝑁) ∈
ℝ+) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))) |
| 142 | 136, 137,
141 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))) |
| 143 | 135, 142 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (√‘𝑁)) |
| 144 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ) |
| 145 | 49 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ) |
| 146 | | flge 13845 |
. . . . . . . . . . . 12
⊢
(((√‘𝑁)
∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
| 147 | 144, 145,
146 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
| 148 | 143, 147 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))) |
| 149 | 49, 84 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈
(ℤ≥‘1)) |
| 150 | 21 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ∈ ℤ) |
| 151 | 150 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈
ℤ) |
| 152 | | elfz5 13556 |
. . . . . . . . . . 11
⊢ (((𝑄‘𝑦) ∈ (ℤ≥‘1)
∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
| 153 | 149, 151,
152 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
| 154 | 148, 153 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁)))) |
| 155 | 127, 154 | opelxpd 5724 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
| 156 | 155 | ex 412 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑀 → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
| 157 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V |
| 158 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑄‘𝑦) ∈ V |
| 159 | 157, 158 | opth 5481 |
. . . . . . . . . . 11
⊢
(〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧))) |
| 160 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) |
| 161 | | oveq12 7440 |
. . . . . . . . . . . 12
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2))) |
| 162 | 160, 161 | sylan2 593 |
. . . . . . . . . . 11
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2))) |
| 163 | 159, 162 | sylbi 217 |
. . . . . . . . . 10
⊢
(〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2))) |
| 164 | 76 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦) |
| 165 | | fz1ssnn 13595 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) ⊆
ℕ |
| 166 | 3, 165 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ 𝑀 ⊆
ℕ |
| 167 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀) |
| 168 | 166, 167 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ) |
| 169 | 168 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ) |
| 170 | 44 | prmreclem1 16954 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈
(ℤ≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2))))) |
| 171 | 170 | simp1d 1143 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ) |
| 172 | 168, 171 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ) |
| 173 | 172 | nnsqcld 14283 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ) |
| 174 | 173 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ) |
| 175 | 173 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0) |
| 176 | 169, 174,
175 | divcan1d 12044 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧) |
| 177 | 164, 176 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧)) |
| 178 | 163, 177 | imbitrid 244 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 → 𝑦 = 𝑧)) |
| 179 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
| 180 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧)) |
| 181 | 180 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) |
| 182 | 179, 181 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2))) |
| 183 | 182, 180 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉) |
| 184 | 178, 183 | impbid1 225 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 ↔ 𝑦 = 𝑧)) |
| 185 | 184 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 ↔ 𝑦 = 𝑧))) |
| 186 | 156, 185 | dom2d 9033 |
. . . . . 6
⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
| 187 | 38, 186 | mpi 20 |
. . . . 5
⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
| 188 | | hashdom 14418 |
. . . . . 6
⊢ ((𝑀 ∈ Fin ∧ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin) →
((♯‘𝑀) ≤
(♯‘({𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
| 189 | 5, 38, 188 | mp2an 692 |
. . . . 5
⊢
((♯‘𝑀)
≤ (♯‘({𝑥
∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
| 190 | 187, 189 | sylibr 234 |
. . . 4
⊢ (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
| 191 | | hashxp 14473 |
. . . . . 6
⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧
(1...(⌊‘(√‘𝑁))) ∈ Fin) →
(♯‘({𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(♯‘(1...(⌊‘(√‘𝑁)))))) |
| 192 | 29, 36, 191 | mp2an 692 |
. . . . 5
⊢
(♯‘({𝑥
∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(♯‘(1...(⌊‘(√‘𝑁))))) |
| 193 | | hashfz1 14385 |
. . . . . . 7
⊢
((⌊‘(√‘𝑁)) ∈ ℕ0 →
(♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁))) |
| 194 | 21, 193 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁))) |
| 195 | 194 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁)))) |
| 196 | 192, 195 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁)))) |
| 197 | 190, 196 | breqtrd 5169 |
. . 3
⊢ (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁)))) |
| 198 | 32 | a1i 11 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ) |
| 199 | 21 | nn0ge0d 12590 |
. . . 4
⊢ (𝜑 → 0 ≤
(⌊‘(√‘𝑁))) |
| 200 | | prmrec.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) |
| 201 | 200, 11, 16, 2, 44 | prmreclem2 16955 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾)) |
| 202 | 198, 24, 33, 199, 201 | lemul1ad 12207 |
. . 3
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁))) ≤ ((2↑𝐾) ·
(⌊‘(√‘𝑁)))) |
| 203 | 9, 35, 23, 197, 202 | letrd 11418 |
. 2
⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) ·
(⌊‘(√‘𝑁)))) |
| 204 | 14 | nnrpd 13075 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈
ℝ+) |
| 205 | 204 | rprege0d 13084 |
. . 3
⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) |
| 206 | | fllelt 13837 |
. . . . 5
⊢
((√‘𝑁)
∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1))) |
| 207 | 25, 206 | syl 17 |
. . . 4
⊢ (𝜑 →
((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1))) |
| 208 | 207 | simpld 494 |
. . 3
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ≤ (√‘𝑁)) |
| 209 | | lemul2a 12122 |
. . 3
⊢
((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧
((2↑𝐾) ∈ ℝ
∧ 0 ≤ (2↑𝐾)))
∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁))) |
| 210 | 33, 25, 205, 208, 209 | syl31anc 1375 |
. 2
⊢ (𝜑 → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁))) |
| 211 | 9, 23, 26, 203, 210 | letrd 11418 |
1
⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁))) |