| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → 𝑞 = 𝑟) |
| 2 | | aks6d1c7.7 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∥ 𝑁) |
| 3 | 2 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → 𝑃 ∥ 𝑁) |
| 4 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑃 → (𝑠 ∥ 𝑁 ↔ 𝑃 ∥ 𝑁)) |
| 5 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑃 → (𝑠 = 𝑟 ↔ 𝑃 = 𝑟)) |
| 6 | 4, 5 | bibi12d 345 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑃 → ((𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟) ↔ (𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟))) |
| 7 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑠(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟) |
| 8 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑝(𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟) |
| 9 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑠 → (𝑝 ∥ 𝑁 ↔ 𝑠 ∥ 𝑁)) |
| 10 | | equequ1 2024 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑠 → (𝑝 = 𝑟 ↔ 𝑠 = 𝑟)) |
| 11 | 9, 10 | bibi12d 345 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑠 → ((𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟) ↔ (𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟))) |
| 12 | 7, 8, 11 | cbvralw 3306 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑝 ∈
ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟) ↔ ∀𝑠 ∈ ℙ (𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟)) |
| 13 | 12 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢
(∀𝑝 ∈
ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟) → ∀𝑠 ∈ ℙ (𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟)) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → ∀𝑠 ∈ ℙ (𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟)) |
| 15 | | aks6d1c7.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → 𝑃 ∈ ℙ) |
| 17 | 6, 14, 16 | rspcdva 3623 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → (𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟)) |
| 18 | 17 | biimpd 229 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → (𝑃 ∥ 𝑁 → 𝑃 = 𝑟)) |
| 19 | 3, 18 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → 𝑃 = 𝑟) |
| 20 | 19 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → 𝑃 = 𝑟) |
| 21 | 20 | eqcomd 2743 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → 𝑟 = 𝑃) |
| 22 | 1, 21 | eqtrd 2777 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → 𝑞 = 𝑃) |
| 23 | 22 | oveq1d 7446 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑞 pCnt 𝑁) = (𝑃 pCnt 𝑁)) |
| 24 | | aks6d1c7.6 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
| 25 | | eluzelz 12888 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 27 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈
ℝ) |
| 28 | | 3re 12346 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
ℝ |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 3 ∈
ℝ) |
| 30 | 26 | zred 12722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 31 | | 3pos 12371 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
3 |
| 32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 3) |
| 33 | | eluzle 12891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
| 34 | 24, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 3 ≤ 𝑁) |
| 35 | 27, 29, 30, 32, 34 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < 𝑁) |
| 36 | 26, 35 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 0 < 𝑁)) |
| 37 | | elnnz 12623 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |
| 38 | 36, 37 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 39 | | pcelnn 16908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) |
| 40 | 15, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) |
| 41 | 2, 40 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈ ℕ) |
| 42 | 41 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈ ℂ) |
| 43 | 42 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 pCnt 𝑁) · 1) = (𝑃 pCnt 𝑁)) |
| 44 | 43 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 pCnt 𝑁) = ((𝑃 pCnt 𝑁) · 1)) |
| 45 | | 1nn0 12542 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
| 46 | 45 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℕ0) |
| 47 | | pcidlem 16910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ 1 ∈
ℕ0) → (𝑃 pCnt (𝑃↑1)) = 1) |
| 48 | 15, 46, 47 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 pCnt (𝑃↑1)) = 1) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 = (𝑃 pCnt (𝑃↑1))) |
| 50 | | prmnn 16711 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 51 | 15, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 52 | 51 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 53 | 52 | exp1d 14181 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃↑1) = 𝑃) |
| 54 | 53 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 pCnt (𝑃↑1)) = (𝑃 pCnt 𝑃)) |
| 55 | 49, 54 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 = (𝑃 pCnt 𝑃)) |
| 56 | 55 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 pCnt 𝑁) · 1) = ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃))) |
| 57 | 44, 56 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt 𝑁) = ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃))) |
| 58 | 57 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑃 pCnt 𝑁) = ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃))) |
| 59 | 58 | ad3antrrr 730 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 pCnt 𝑁) = ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃))) |
| 60 | 16 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → 𝑃 ∈ ℙ) |
| 61 | | nnq 13004 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℚ) |
| 62 | 51, 61 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℚ) |
| 63 | 51 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ≠ 0) |
| 64 | 62, 63 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 ∈ ℚ ∧ 𝑃 ≠ 0)) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑃 ∈ ℚ ∧ 𝑃 ≠ 0)) |
| 66 | 65 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 ∈ ℚ ∧ 𝑃 ≠ 0)) |
| 67 | 41 | nnzd 12640 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈ ℤ) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑃 pCnt 𝑁) ∈ ℤ) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → (𝑃 pCnt 𝑁) ∈ ℤ) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑃 pCnt 𝑁) ∈ ℤ) |
| 71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 pCnt 𝑁) ∈ ℤ) |
| 72 | | pcexp 16897 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 ∈ ℚ ∧ 𝑃 ≠ 0) ∧ (𝑃 pCnt 𝑁) ∈ ℤ) → (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝑁))) = ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃))) |
| 73 | 60, 66, 71, 72 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝑁))) = ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃))) |
| 74 | 73 | eqcomd 2743 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → ((𝑃 pCnt 𝑁) · (𝑃 pCnt 𝑃)) = (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 75 | 59, 74 | eqtrd 2777 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 pCnt 𝑁) = (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 76 | 22 | eqcomd 2743 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → 𝑃 = 𝑞) |
| 77 | 76 | oveq1d 7446 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝑁))) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 78 | 75, 77 | eqtrd 2777 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑃 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 79 | 23, 78 | eqtrd 2777 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ 𝑞 = 𝑟) → (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 80 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑞 → (𝑠 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁)) |
| 81 | | equequ1 2024 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑞 → (𝑠 = 𝑟 ↔ 𝑞 = 𝑟)) |
| 82 | 80, 81 | bibi12d 345 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑞 → ((𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟) ↔ (𝑞 ∥ 𝑁 ↔ 𝑞 = 𝑟))) |
| 83 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → ∀𝑠 ∈ ℙ (𝑠 ∥ 𝑁 ↔ 𝑠 = 𝑟)) |
| 84 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ) |
| 85 | 82, 83, 84 | rspcdva 3623 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑁 ↔ 𝑞 = 𝑟)) |
| 86 | 85 | bicomd 223 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑞 = 𝑟 ↔ 𝑞 ∥ 𝑁)) |
| 87 | 86 | notbid 318 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (¬ 𝑞 = 𝑟 ↔ ¬ 𝑞 ∥ 𝑁)) |
| 88 | 87 | biimpa 476 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → ¬ 𝑞 ∥ 𝑁) |
| 89 | 84 | adantr 480 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑞 ∈ ℙ) |
| 90 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → 𝑁 ∈ ℕ) |
| 91 | 90 | ad3antrrr 730 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑁 ∈ ℕ) |
| 92 | | pceq0 16909 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑞 pCnt 𝑁) = 0 ↔ ¬ 𝑞 ∥ 𝑁)) |
| 93 | 89, 91, 92 | syl2anc 584 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → ((𝑞 pCnt 𝑁) = 0 ↔ ¬ 𝑞 ∥ 𝑁)) |
| 94 | 88, 93 | mpbird 257 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑞 pCnt 𝑁) = 0) |
| 95 | | neqne 2948 |
. . . . . . . . . . . . 13
⊢ (¬
𝑞 = 𝑟 → 𝑞 ≠ 𝑟) |
| 96 | 95 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑞 ≠ 𝑟) |
| 97 | 3 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → 𝑃 ∥ 𝑁) |
| 98 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → 𝑃 ∈ ℙ) |
| 99 | 6, 83, 98 | rspcdva 3623 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑃 ∥ 𝑁 ↔ 𝑃 = 𝑟)) |
| 100 | 99 | biimpd 229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑃 ∥ 𝑁 → 𝑃 = 𝑟)) |
| 101 | 97, 100 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → 𝑃 = 𝑟) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑃 = 𝑟) |
| 103 | 102 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑟 = 𝑃) |
| 104 | 96, 103 | neeqtrd 3010 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑞 ≠ 𝑃) |
| 105 | 104 | neneqd 2945 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → ¬ 𝑞 = 𝑃) |
| 106 | | prmuz2 16733 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
(ℤ≥‘2)) |
| 107 | 106 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → 𝑞 ∈
(ℤ≥‘2)) |
| 108 | 107 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑞 ∈
(ℤ≥‘2)) |
| 109 | 16 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑃 ∈ ℙ) |
| 110 | | dvdsprm 16740 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑞 ∥ 𝑃 ↔ 𝑞 = 𝑃)) |
| 111 | 108, 109,
110 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑞 ∥ 𝑃 ↔ 𝑞 = 𝑃)) |
| 112 | 105, 111 | mtbird 325 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → ¬ 𝑞 ∥ 𝑃) |
| 113 | 51 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑃 ∈ ℕ) |
| 114 | 113 | nnzd 12640 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 𝑃 ∈ ℤ) |
| 115 | 41 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℙ) → (𝑃 pCnt 𝑁) ∈ ℕ) |
| 116 | 115 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → (𝑃 pCnt 𝑁) ∈ ℕ) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑃 pCnt 𝑁) ∈ ℕ) |
| 118 | 117 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑃 pCnt 𝑁) ∈ ℕ) |
| 119 | | prmdvdsexp 16752 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧ 𝑃 ∈ ℤ ∧ (𝑃 pCnt 𝑁) ∈ ℕ) → (𝑞 ∥ (𝑃↑(𝑃 pCnt 𝑁)) ↔ 𝑞 ∥ 𝑃)) |
| 120 | 89, 114, 118, 119 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑞 ∥ (𝑃↑(𝑃 pCnt 𝑁)) ↔ 𝑞 ∥ 𝑃)) |
| 121 | 112, 120 | mtbird 325 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → ¬ 𝑞 ∥ (𝑃↑(𝑃 pCnt 𝑁))) |
| 122 | 109, 91 | pccld 16888 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑃 pCnt 𝑁) ∈
ℕ0) |
| 123 | 113, 122 | nnexpcld 14284 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ) |
| 124 | | pceq0 16909 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℙ ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ) → ((𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁))) = 0 ↔ ¬ 𝑞 ∥ (𝑃↑(𝑃 pCnt 𝑁)))) |
| 125 | 89, 123, 124 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → ((𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁))) = 0 ↔ ¬ 𝑞 ∥ (𝑃↑(𝑃 pCnt 𝑁)))) |
| 126 | 121, 125 | mpbird 257 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁))) = 0) |
| 127 | 126 | eqcomd 2743 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → 0 = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 128 | 94, 127 | eqtrd 2777 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑟 ∈ ℙ) ∧
∀𝑝 ∈ ℙ
(𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 = 𝑟) → (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 129 | 79, 128 | pm2.61dan 813 |
. . . 4
⊢ ((((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 130 | 129 | ralrimiva 3146 |
. . 3
⊢ (((𝜑 ∧ 𝑟 ∈ ℙ) ∧ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 131 | | aks6d1c7.1 |
. . . . 5
⊢ ∼ =
{〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈
(Base‘(Poly1‘𝐾)) ∧ ∀𝑦 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)(𝑒(.g‘(mulGrp‘𝐾))(((eval1‘𝐾)‘𝑓)‘𝑦)) = (((eval1‘𝐾)‘𝑓)‘(𝑒(.g‘(mulGrp‘𝐾))𝑦)))} |
| 132 | | aks6d1c7.2 |
. . . . 5
⊢ 𝑃 = (chr‘𝐾) |
| 133 | | aks6d1c7.3 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Field) |
| 134 | | aks6d1c7.5 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 135 | | aks6d1c7.8 |
. . . . 5
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |
| 136 | | aks6d1c7.9 |
. . . . 5
⊢ 𝐴 =
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) |
| 137 | | aks6d1c7.10 |
. . . . 5
⊢ (𝜑 → ((2 logb 𝑁)↑2) <
((odℤ‘𝑅)‘𝑁)) |
| 138 | | aks6d1c7.11 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐾) ↦ (𝑃(.g‘(mulGrp‘𝐾))𝑥)) ∈ (𝐾 RingIso 𝐾)) |
| 139 | | aks6d1c7.12 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) |
| 140 | | aks6d1c7.13 |
. . . . 5
⊢ (𝜑 → ∀𝑏 ∈ (1...𝐴)(𝑏 gcd 𝑁) = 1) |
| 141 | | aks6d1c7.14 |
. . . . 5
⊢ (𝜑 → ∀𝑎 ∈ (1...𝐴)𝑁 ∼
((var1‘𝐾)(+g‘(Poly1‘𝐾))((algSc‘(Poly1‘𝐾))‘((ℤRHom‘𝐾)‘𝑎)))) |
| 142 | 131, 132,
133, 15, 134, 24, 2, 135, 136, 137, 138, 139, 140, 141 | aks6d1c7lem4 42184 |
. . . 4
⊢ (𝜑 → ∃!𝑝 ∈ ℙ 𝑝 ∥ 𝑁) |
| 143 | | reu6 3732 |
. . . 4
⊢
(∃!𝑝 ∈
ℙ 𝑝 ∥ 𝑁 ↔ ∃𝑟 ∈ ℙ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) |
| 144 | 142, 143 | sylib 218 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ ℙ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝑁 ↔ 𝑝 = 𝑟)) |
| 145 | 130, 144 | r19.29a 3162 |
. 2
⊢ (𝜑 → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁)))) |
| 146 | 38 | nnnn0d 12587 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 147 | 51 | nnnn0d 12587 |
. . . 4
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 148 | 15, 38 | pccld 16888 |
. . . 4
⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈
ℕ0) |
| 149 | 147, 148 | nn0expcld 14285 |
. . 3
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑁)) ∈
ℕ0) |
| 150 | | pc11 16918 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ0) → (𝑁 = (𝑃↑(𝑃 pCnt 𝑁)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁))))) |
| 151 | 146, 149,
150 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑁 = (𝑃↑(𝑃 pCnt 𝑁)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑁) = (𝑞 pCnt (𝑃↑(𝑃 pCnt 𝑁))))) |
| 152 | 145, 151 | mpbird 257 |
1
⊢ (𝜑 → 𝑁 = (𝑃↑(𝑃 pCnt 𝑁))) |