Step | Hyp | Ref
| Expression |
1 | | fzfi 12633 |
. . . . . 6
⊢
(1...𝑁) ∈
Fin |
2 | | prmrec.4 |
. . . . . . 7
⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} |
3 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁) |
4 | 2, 3 | eqsstri 3598 |
. . . . . 6
⊢ 𝑀 ⊆ (1...𝑁) |
5 | | ssfi 8065 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin) |
6 | 1, 4, 5 | mp2an 704 |
. . . . 5
⊢ 𝑀 ∈ Fin |
7 | | hashcl 13009 |
. . . . 5
⊢ (𝑀 ∈ Fin →
(#‘𝑀) ∈
ℕ0) |
8 | 6, 7 | ax-mp 5 |
. . . 4
⊢
(#‘𝑀) ∈
ℕ0 |
9 | 8 | nn0rei 11180 |
. . 3
⊢
(#‘𝑀) ∈
ℝ |
10 | 9 | a1i 11 |
. 2
⊢ (𝜑 → (#‘𝑀) ∈ ℝ) |
11 | | 2nn 11062 |
. . . . . 6
⊢ 2 ∈
ℕ |
12 | | prmrec.2 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
13 | 12 | nnnn0d 11228 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
14 | | nnexpcl 12735 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝐾
∈ ℕ0) → (2↑𝐾) ∈ ℕ) |
15 | 11, 13, 14 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (2↑𝐾) ∈ ℕ) |
16 | 15 | nnnn0d 11228 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈
ℕ0) |
17 | | prmrec.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
18 | 17 | nnrpd 11746 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
19 | 18 | rpsqrtcld 13998 |
. . . . . 6
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
20 | 19 | rprege0d 11755 |
. . . . 5
⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤
(√‘𝑁))) |
21 | | flge0nn0 12483 |
. . . . 5
⊢
(((√‘𝑁)
∈ ℝ ∧ 0 ≤ (√‘𝑁)) →
(⌊‘(√‘𝑁)) ∈
ℕ0) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ∈
ℕ0) |
23 | 16, 22 | nn0mulcld 11233 |
. . 3
⊢ (𝜑 → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ∈
ℕ0) |
24 | 23 | nn0red 11229 |
. 2
⊢ (𝜑 → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ∈ ℝ) |
25 | 15 | nnred 10912 |
. . 3
⊢ (𝜑 → (2↑𝐾) ∈ ℝ) |
26 | 19 | rpred 11748 |
. . 3
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
27 | 25, 26 | remulcld 9949 |
. 2
⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ) |
28 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀 |
29 | | ssfi 8065 |
. . . . . . 7
⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin) |
30 | 6, 28, 29 | mp2an 704 |
. . . . . 6
⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin |
31 | | hashcl 13009 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈
ℕ0) |
32 | 30, 31 | ax-mp 5 |
. . . . 5
⊢
(#‘{𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1}) ∈
ℕ0 |
33 | 32 | nn0rei 11180 |
. . . 4
⊢
(#‘{𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ |
34 | 22 | nn0red 11229 |
. . . 4
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ∈ ℝ) |
35 | | remulcl 9900 |
. . . 4
⊢
(((#‘{𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧
(⌊‘(√‘𝑁)) ∈ ℝ) → ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁))) ∈ ℝ) |
36 | 33, 34, 35 | sylancr 694 |
. . 3
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁))) ∈ ℝ) |
37 | | fzfi 12633 |
. . . . . . 7
⊢
(1...(⌊‘(√‘𝑁))) ∈ Fin |
38 | | xpfi 8116 |
. . . . . . 7
⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧
(1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin) |
39 | 30, 37, 38 | mp2an 704 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin |
40 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀) |
41 | 4, 40 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁)) |
42 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ) |
44 | | prmreclem2.5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, <
)) |
45 | 44 | prmreclem1 15458 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ≥‘2)
→ ¬ (𝑛↑2)
∥ (𝑦 / ((𝑄‘𝑦)↑2))))) |
46 | 45 | simp2d 1067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦) |
47 | 43, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦) |
48 | 45 | simp1d 1066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ) |
49 | 43, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ) |
50 | 49 | nnsqcld 12891 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ) |
51 | 50 | nnzd 11357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ) |
52 | 50 | nnne0d 10942 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0) |
53 | 43 | nnzd 11357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ) |
54 | | dvdsval2 14824 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)) |
55 | 51, 52, 53, 54 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)) |
56 | 47, 55 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ) |
57 | | nnre 10904 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
58 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
59 | 57, 58 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 <
𝑦)) |
60 | | nnre 10904 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ) |
61 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 <
((𝑄‘𝑦)↑2)) |
62 | 60, 61 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) |
63 | | divgt0 10770 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℝ ∧ 0 <
𝑦) ∧ (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) → 0 < (𝑦 / ((𝑄‘𝑦)↑2))) |
64 | 59, 62, 63 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∈ ℕ) → 0 <
(𝑦 / ((𝑄‘𝑦)↑2))) |
65 | 43, 50, 64 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 0 < (𝑦 / ((𝑄‘𝑦)↑2))) |
66 | | elnnz 11264 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2)))) |
67 | 56, 65, 66 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ) |
68 | 67 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ) |
69 | 43 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ) |
70 | 17 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ) |
72 | | dvdsmul1 14841 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2))) |
73 | 56, 51, 72 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2))) |
74 | 43 | nncnd 10913 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ) |
75 | 50 | nncnd 10913 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ) |
76 | 74, 75, 52 | divcan1d 10681 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦) |
77 | 73, 76 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) |
78 | | dvdsle 14870 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)) |
79 | 56, 43, 78 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)) |
80 | 77, 79 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦) |
81 | | elfzle2 12216 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁) |
82 | 41, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁) |
83 | 68, 69, 71, 80, 82 | letrd 10073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁) |
84 | | nnuz 11599 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
85 | 67, 84 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈
(ℤ≥‘1)) |
86 | 17 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ) |
88 | | elfz5 12205 |
. . . . . . . . . . . . 13
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)) |
89 | 85, 87, 88 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)) |
90 | 83, 89 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁)) |
91 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦)) |
92 | 91 | notbid 307 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦)) |
93 | 92 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)) |
94 | 93, 2 | elrab2 3333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)) |
95 | 40, 94 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)) |
96 | 95 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦) |
97 | 77 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) |
98 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ (ℙ ∖
(1...𝐾)) → 𝑝 ∈
ℙ) |
99 | | prmz 15227 |
. . . . . . . . . . . . . . . . . 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 14856 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦)) |
105 | 101, 102,
103, 104 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦)) |
106 | 97, 105 | mpan2d 706 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) → 𝑝 ∥ 𝑦)) |
107 | 106 | con3d 147 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
108 | 107 | ralimdva 2945 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
109 | 96, 108 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))) |
110 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
111 | 110 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
112 | 111 | ralbidv 2969 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
113 | 112, 2 | elrab2 3333 |
. . . . . . . . . . 11
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
114 | 90, 109, 113 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀) |
115 | 44 | prmreclem1 15458 |
. . . . . . . . . . . . 13
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ≥‘2)
→ ¬ (𝐴↑2)
∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2))))) |
116 | 115 | simp2d 1067 |
. . . . . . . . . . . 12
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))) |
117 | 67, 116 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))) |
118 | 115 | simp1d 1066 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ) |
119 | 67, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ) |
120 | | elnn1uz2 11641 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2))) |
121 | 119, 120 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2))) |
122 | 121 | ord 391 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2))) |
123 | 44 | prmreclem1 15458 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))) |
124 | 123 | simp3d 1068 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈
(ℤ≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
125 | 43, 122, 124 | sylsyld 59 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))) |
126 | 117, 125 | mt4d 151 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1) |
127 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑄‘𝑥) = (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))) |
128 | 127 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1)) |
129 | 128 | elrab 3331 |
. . . . . . . . . 10
⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ∧ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1)) |
130 | 114, 126,
129 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) |
131 | 50 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ) |
132 | | dvdsle 14870 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦)) |
133 | 51, 43, 132 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦)) |
134 | 47, 133 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑦) |
135 | 131, 69, 71, 134, 82 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁) |
136 | 71 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ) |
137 | 136 | sqsqrtd 14026 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁) |
138 | 135, 137 | breqtrrd 4611 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)) |
139 | 49 | nnrpd 11746 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈
ℝ+) |
140 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈
ℝ+) |
141 | | rprege0 11723 |
. . . . . . . . . . . . . 14
⊢ ((𝑄‘𝑦) ∈ ℝ+ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦))) |
142 | | rprege0 11723 |
. . . . . . . . . . . . . 14
⊢
((√‘𝑁)
∈ ℝ+ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤
(√‘𝑁))) |
143 | | le2sq 12800 |
. . . . . . . . . . . . . 14
⊢ ((((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤
(√‘𝑁))) →
((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))) |
144 | 141, 142,
143 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘𝑦) ∈ ℝ+ ∧
(√‘𝑁) ∈
ℝ+) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))) |
145 | 139, 140,
144 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))) |
146 | 138, 145 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (√‘𝑁)) |
147 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ) |
148 | 49 | nnzd 11357 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ) |
149 | | flge 12468 |
. . . . . . . . . . . 12
⊢
(((√‘𝑁)
∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
150 | 147, 148,
149 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
151 | 146, 150 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))) |
152 | 49, 84 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈
(ℤ≥‘1)) |
153 | 22 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ∈ ℤ) |
154 | 153 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈
ℤ) |
155 | | elfz5 12205 |
. . . . . . . . . . 11
⊢ (((𝑄‘𝑦) ∈ (ℤ≥‘1)
∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
156 | 152, 154,
155 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))) |
157 | 151, 156 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁)))) |
158 | | opelxpi 5072 |
. . . . . . . . 9
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ (𝑄‘𝑦) ∈
(1...(⌊‘(√‘𝑁)))) → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
159 | 130, 157,
158 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
160 | 159 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝑀 → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
161 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V |
162 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑄‘𝑦) ∈ V |
163 | 161, 162 | opth 4871 |
. . . . . . . . . . 11
⊢
(〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧))) |
164 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) |
165 | | oveq12 6558 |
. . . . . . . . . . . 12
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2))) |
166 | 164, 165 | sylan2 490 |
. . . . . . . . . . 11
⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2))) |
167 | 163, 166 | sylbi 206 |
. . . . . . . . . 10
⊢
(〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2))) |
168 | 76 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦) |
169 | 42 | ssriv 3572 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) ⊆
ℕ |
170 | 4, 169 | sstri 3577 |
. . . . . . . . . . . . . 14
⊢ 𝑀 ⊆
ℕ |
171 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀) |
172 | 170, 171 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ) |
173 | 172 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ) |
174 | 44 | prmreclem1 15458 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈
(ℤ≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2))))) |
175 | 174 | simp1d 1066 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ) |
176 | 172, 175 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ) |
177 | 176 | nnsqcld 12891 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ) |
178 | 177 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ) |
179 | 177 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0) |
180 | 173, 178,
179 | divcan1d 10681 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧) |
181 | 168, 180 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧)) |
182 | 167, 181 | syl5ib 233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 → 𝑦 = 𝑧)) |
183 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
184 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧)) |
185 | 184 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) |
186 | 183, 185 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2))) |
187 | 186, 184 | opeq12d 4348 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → 〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉) |
188 | 182, 187 | impbid1 214 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 ↔ 𝑦 = 𝑧)) |
189 | 188 | ex 449 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (〈(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)〉 = 〈(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)〉 ↔ 𝑦 = 𝑧))) |
190 | 160, 189 | dom2d 7882 |
. . . . . 6
⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
191 | 39, 190 | mpi 20 |
. . . . 5
⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
192 | | hashdom 13029 |
. . . . . 6
⊢ ((𝑀 ∈ Fin ∧ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((#‘𝑀) ≤ (#‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
193 | 6, 39, 192 | mp2an 704 |
. . . . 5
⊢
((#‘𝑀) ≤
(#‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) |
194 | 191, 193 | sylibr 223 |
. . . 4
⊢ (𝜑 → (#‘𝑀) ≤ (#‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁)))))) |
195 | | hashxp 13081 |
. . . . . 6
⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧
(1...(⌊‘(√‘𝑁))) ∈ Fin) → (#‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(#‘(1...(⌊‘(√‘𝑁)))))) |
196 | 30, 37, 195 | mp2an 704 |
. . . . 5
⊢
(#‘({𝑥 ∈
𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(#‘(1...(⌊‘(√‘𝑁))))) |
197 | | hashfz1 12996 |
. . . . . . 7
⊢
((⌊‘(√‘𝑁)) ∈ ℕ0 →
(#‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁))) |
198 | 22, 197 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(#‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁))) |
199 | 198 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(#‘(1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁)))) |
200 | 196, 199 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → (#‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ×
(1...(⌊‘(√‘𝑁))))) = ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁)))) |
201 | 194, 200 | breqtrd 4609 |
. . 3
⊢ (𝜑 → (#‘𝑀) ≤ ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁)))) |
202 | 33 | a1i 11 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ) |
203 | 22 | nn0ge0d 11231 |
. . . 4
⊢ (𝜑 → 0 ≤
(⌊‘(√‘𝑁))) |
204 | | prmrec.1 |
. . . . 5
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) |
205 | 204, 12, 17, 2, 44 | prmreclem2 15459 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾)) |
206 | 202, 25, 34, 203, 205 | lemul1ad 10842 |
. . 3
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ·
(⌊‘(√‘𝑁))) ≤ ((2↑𝐾) ·
(⌊‘(√‘𝑁)))) |
207 | 10, 36, 24, 201, 206 | letrd 10073 |
. 2
⊢ (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) ·
(⌊‘(√‘𝑁)))) |
208 | 15 | nnrpd 11746 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈
ℝ+) |
209 | 208 | rprege0d 11755 |
. . 3
⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) |
210 | | fllelt 12460 |
. . . . 5
⊢
((√‘𝑁)
∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1))) |
211 | 26, 210 | syl 17 |
. . . 4
⊢ (𝜑 →
((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1))) |
212 | 211 | simpld 474 |
. . 3
⊢ (𝜑 →
(⌊‘(√‘𝑁)) ≤ (√‘𝑁)) |
213 | | lemul2a 10757 |
. . 3
⊢
((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧
((2↑𝐾) ∈ ℝ
∧ 0 ≤ (2↑𝐾)))
∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁))) |
214 | 34, 26, 209, 212, 213 | syl31anc 1321 |
. 2
⊢ (𝜑 → ((2↑𝐾) ·
(⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁))) |
215 | 10, 24, 27, 207, 214 | letrd 10073 |
1
⊢ (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁))) |