| Step | Hyp | Ref
| Expression |
| 1 | | zringring 21460 |
. . . . . 6
⊢
ℤring ∈ Ring |
| 2 | | prmirred.i |
. . . . . . 7
⊢ 𝐼 =
(Irred‘ℤring) |
| 3 | | zring1 21470 |
. . . . . . 7
⊢ 1 =
(1r‘ℤring) |
| 4 | 2, 3 | irredn1 20426 |
. . . . . 6
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ 𝐼) → 𝐴 ≠ 1) |
| 5 | 1, 4 | mpan 690 |
. . . . 5
⊢ (𝐴 ∈ 𝐼 → 𝐴 ≠ 1) |
| 6 | 5 | anim2i 617 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1)) |
| 7 | | eluz2b3 12964 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1)) |
| 8 | 6, 7 | sylibr 234 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈
(ℤ≥‘2)) |
| 9 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 10 | 9 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℤ) |
| 11 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∥ 𝐴) |
| 12 | | nnne0 12300 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
| 13 | 12 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ≠ 0) |
| 14 | | nnz 12634 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
| 15 | 14 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℤ) |
| 16 | | dvdsval2 16293 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝐴 ∈ ℤ) → (𝑦 ∥ 𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ)) |
| 17 | 10, 13, 15, 16 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∥ 𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ)) |
| 18 | 11, 17 | mpbid 232 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝐴 / 𝑦) ∈ ℤ) |
| 19 | 15 | zcnd 12723 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℂ) |
| 20 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 21 | 20 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℂ) |
| 22 | 19, 21, 13 | divcan2d 12045 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · (𝐴 / 𝑦)) = 𝐴) |
| 23 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ 𝐼) |
| 24 | 22, 23 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) |
| 25 | | zringbas 21464 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
| 26 | | eqid 2737 |
. . . . . . . 8
⊢
(Unit‘ℤring) =
(Unit‘ℤring) |
| 27 | | zringmulr 21468 |
. . . . . . . 8
⊢ ·
= (.r‘ℤring) |
| 28 | 2, 25, 26, 27 | irredmul 20429 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ (𝐴 / 𝑦) ∈ ℤ ∧ (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) → (𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring))) |
| 29 | 10, 18, 24, 28 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring))) |
| 30 | | zringunit 21477 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(Unit‘ℤring) ↔ (𝑦 ∈ ℤ ∧ (abs‘𝑦) = 1)) |
| 31 | 30 | baib 535 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → (𝑦 ∈
(Unit‘ℤring) ↔ (abs‘𝑦) = 1)) |
| 32 | 10, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑦) =
1)) |
| 33 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
| 34 | | nn0re 12535 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
| 35 | | nn0ge0 12551 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 0 ≤ 𝑦) |
| 36 | 34, 35 | absidd 15461 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (abs‘𝑦) =
𝑦) |
| 37 | 33, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(abs‘𝑦) = 𝑦) |
| 38 | 37 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (abs‘𝑦) = 𝑦) |
| 39 | 38 | eqeq1d 2739 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘𝑦) = 1 ↔ 𝑦 = 1)) |
| 40 | 32, 39 | bitrd 279 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
↔ 𝑦 =
1)) |
| 41 | | zringunit 21477 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ ((𝐴 / 𝑦) ∈ ℤ ∧
(abs‘(𝐴 / 𝑦)) = 1)) |
| 42 | 41 | baib 535 |
. . . . . . . . 9
⊢ ((𝐴 / 𝑦) ∈ ℤ → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ (abs‘(𝐴 /
𝑦)) = 1)) |
| 43 | 18, 42 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ (abs‘(𝐴 /
𝑦)) = 1)) |
| 44 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
| 45 | 44 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℝ) |
| 46 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℕ) |
| 47 | 45, 46 | nndivred 12320 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝐴 / 𝑦) ∈ ℝ) |
| 48 | | nnnn0 12533 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
| 49 | | nn0ge0 12551 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 ≤ 𝐴) |
| 52 | 46 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℝ) |
| 53 | | nngt0 12297 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
| 54 | 53 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 < 𝑦) |
| 55 | | divge0 12137 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 0 <
𝑦)) → 0 ≤ (𝐴 / 𝑦)) |
| 56 | 45, 51, 52, 54, 55 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 ≤ (𝐴 / 𝑦)) |
| 57 | 47, 56 | absidd 15461 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (abs‘(𝐴 / 𝑦)) = (𝐴 / 𝑦)) |
| 58 | 57 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ (𝐴 / 𝑦) = 1)) |
| 59 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 1 ∈ ℂ) |
| 60 | 19, 21, 59, 13 | divmuld 12065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) = 1 ↔ (𝑦 · 1) = 𝐴)) |
| 61 | 21 | mulridd 11278 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · 1) = 𝑦) |
| 62 | 61 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝑦 · 1) = 𝐴 ↔ 𝑦 = 𝐴)) |
| 63 | 58, 60, 62 | 3bitrd 305 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ 𝑦 = 𝐴)) |
| 64 | 43, 63 | bitrd 279 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ 𝑦 = 𝐴)) |
| 65 | 40, 64 | orbi12d 919 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring)) ↔ (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
| 66 | 29, 65 | mpbid 232 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 = 1 ∨ 𝑦 = 𝐴)) |
| 67 | 66 | expr 456 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ 𝑦 ∈ ℕ) → (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
| 68 | 67 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
| 69 | | isprm2 16719 |
. . 3
⊢ (𝐴 ∈ ℙ ↔ (𝐴 ∈
(ℤ≥‘2) ∧ ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))) |
| 70 | 8, 68, 69 | sylanbrc 583 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ ℙ) |
| 71 | | prmz 16712 |
. . . 4
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℤ) |
| 72 | | 1nprm 16716 |
. . . . 5
⊢ ¬ 1
∈ ℙ |
| 73 | | zringunit 21477 |
. . . . . 6
⊢ (𝐴 ∈
(Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) |
| 74 | | prmnn 16711 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℕ) |
| 75 | | nn0re 12535 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
| 76 | 75, 49 | absidd 15461 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ (abs‘𝐴) =
𝐴) |
| 77 | 74, 48, 76 | 3syl 18 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ →
(abs‘𝐴) = 𝐴) |
| 78 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℙ) |
| 79 | 77, 78 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝐴 ∈ ℙ →
(abs‘𝐴) ∈
ℙ) |
| 80 | | eleq1 2829 |
. . . . . . . 8
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)
∈ ℙ ↔ 1 ∈ ℙ)) |
| 81 | 79, 80 | syl5ibcom 245 |
. . . . . . 7
⊢ (𝐴 ∈ ℙ →
((abs‘𝐴) = 1 → 1
∈ ℙ)) |
| 82 | 81 | adantld 490 |
. . . . . 6
⊢ (𝐴 ∈ ℙ → ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) → 1
∈ ℙ)) |
| 83 | 73, 82 | biimtrid 242 |
. . . . 5
⊢ (𝐴 ∈ ℙ → (𝐴 ∈
(Unit‘ℤring) → 1 ∈ ℙ)) |
| 84 | 72, 83 | mtoi 199 |
. . . 4
⊢ (𝐴 ∈ ℙ → ¬
𝐴 ∈
(Unit‘ℤring)) |
| 85 | | dvdsmul1 16315 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∥ (𝑥 · 𝑦)) |
| 86 | 85 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ (𝑥 · 𝑦)) |
| 87 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) = 𝐴) |
| 88 | 86, 87 | breqtrd 5169 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ 𝐴) |
| 89 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℤ) |
| 90 | 71 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℤ) |
| 91 | | absdvdsb 16312 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑥 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
| 92 | 89, 90, 91 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
| 93 | 88, 92 | mpbid 232 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∥ 𝐴) |
| 94 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑥) → (𝑦 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
| 95 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑥) → (𝑦 = 1 ↔ (abs‘𝑥) = 1)) |
| 96 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑥) → (𝑦 = 𝐴 ↔ (abs‘𝑥) = 𝐴)) |
| 97 | 95, 96 | orbi12d 919 |
. . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑥) → ((𝑦 = 1 ∨ 𝑦 = 𝐴) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
| 98 | 94, 97 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑦 = (abs‘𝑥) → ((𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)) ↔ ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))) |
| 99 | 69 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℙ →
∀𝑦 ∈ ℕ
(𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
| 100 | 99 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
| 101 | 89 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℂ) |
| 102 | 74 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℕ) |
| 103 | 102 | nnne0d 12316 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ≠ 0) |
| 104 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℤ) |
| 105 | 104 | zcnd 12723 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℂ) |
| 106 | 105 | mul02d 11459 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (0 · 𝑦) = 0) |
| 107 | 103, 87, 106 | 3netr4d 3018 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) ≠ (0 · 𝑦)) |
| 108 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → (𝑥 · 𝑦) = (0 · 𝑦)) |
| 109 | 108 | necon3i 2973 |
. . . . . . . . . . . . 13
⊢ ((𝑥 · 𝑦) ≠ (0 · 𝑦) → 𝑥 ≠ 0) |
| 110 | 107, 109 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ≠ 0) |
| 111 | 101, 110 | absne0d 15486 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ≠ 0) |
| 112 | 111 | neneqd 2945 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ¬ (abs‘𝑥) = 0) |
| 113 | | nn0abscl 15351 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ →
(abs‘𝑥) ∈
ℕ0) |
| 114 | 89, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈
ℕ0) |
| 115 | | elnn0 12528 |
. . . . . . . . . . . 12
⊢
((abs‘𝑥)
∈ ℕ0 ↔ ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0)) |
| 116 | 114, 115 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0)) |
| 117 | 116 | ord 865 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (¬ (abs‘𝑥) ∈ ℕ →
(abs‘𝑥) =
0)) |
| 118 | 112, 117 | mt3d 148 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℕ) |
| 119 | 98, 100, 118 | rspcdva 3623 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
| 120 | 93, 119 | mpd 15 |
. . . . . . 7
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)) |
| 121 | | zringunit 21477 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(Unit‘ℤring) ↔ (𝑥 ∈ ℤ ∧ (abs‘𝑥) = 1)) |
| 122 | 121 | baib 535 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → (𝑥 ∈
(Unit‘ℤring) ↔ (abs‘𝑥) = 1)) |
| 123 | 89, 122 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring)
↔ (abs‘𝑥) =
1)) |
| 124 | 104, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑦) =
1)) |
| 125 | 105 | abscld 15475 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℝ) |
| 126 | 125 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℂ) |
| 127 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 1 ∈ ℂ) |
| 128 | 101 | abscld 15475 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℝ) |
| 129 | 128 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℂ) |
| 130 | 126, 127,
129, 111 | mulcand 11896 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑦) = 1)) |
| 131 | 87 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = (abs‘𝐴)) |
| 132 | 101, 105 | absmuld 15493 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = ((abs‘𝑥) · (abs‘𝑦))) |
| 133 | 77 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝐴) = 𝐴) |
| 134 | 131, 132,
133 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · (abs‘𝑦)) = 𝐴) |
| 135 | 129 | mulridd 11278 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · 1) = (abs‘𝑥)) |
| 136 | 134, 135 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ 𝐴 = (abs‘𝑥))) |
| 137 | | eqcom 2744 |
. . . . . . . . . 10
⊢ (𝐴 = (abs‘𝑥) ↔ (abs‘𝑥) = 𝐴) |
| 138 | 136, 137 | bitrdi 287 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑥) = 𝐴)) |
| 139 | 124, 130,
138 | 3bitr2d 307 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑥) =
𝐴)) |
| 140 | 123, 139 | orbi12d 919 |
. . . . . . 7
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
| 141 | 120, 140 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring))) |
| 142 | 141 | ex 412 |
. . . . 5
⊢ ((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)))) |
| 143 | 142 | ralrimivva 3202 |
. . . 4
⊢ (𝐴 ∈ ℙ →
∀𝑥 ∈ ℤ
∀𝑦 ∈ ℤ
((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)))) |
| 144 | 25, 26, 2, 27 | isirred2 20421 |
. . . 4
⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈
(Unit‘ℤring) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring))))) |
| 145 | 71, 84, 143, 144 | syl3anbrc 1344 |
. . 3
⊢ (𝐴 ∈ ℙ → 𝐴 ∈ 𝐼) |
| 146 | 145 | adantl 481 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ ℙ) → 𝐴 ∈ 𝐼) |
| 147 | 70, 146 | impbida 801 |
1
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |