Step | Hyp | Ref
| Expression |
1 | | zringring 20673 |
. . . . . 6
⊢
ℤring ∈ Ring |
2 | | prmirred.i |
. . . . . . 7
⊢ 𝐼 =
(Irred‘ℤring) |
3 | | zring1 20681 |
. . . . . . 7
⊢ 1 =
(1r‘ℤring) |
4 | 2, 3 | irredn1 19948 |
. . . . . 6
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ 𝐼) → 𝐴 ≠ 1) |
5 | 1, 4 | mpan 687 |
. . . . 5
⊢ (𝐴 ∈ 𝐼 → 𝐴 ≠ 1) |
6 | 5 | anim2i 617 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1)) |
7 | | eluz2b3 12662 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1)) |
8 | 6, 7 | sylibr 233 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈
(ℤ≥‘2)) |
9 | | nnz 12342 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
10 | 9 | ad2antrl 725 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℤ) |
11 | | simprr 770 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∥ 𝐴) |
12 | | nnne0 12007 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
13 | 12 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ≠ 0) |
14 | | nnz 12342 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
15 | 14 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℤ) |
16 | | dvdsval2 15966 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝐴 ∈ ℤ) → (𝑦 ∥ 𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ)) |
17 | 10, 13, 15, 16 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∥ 𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ)) |
18 | 11, 17 | mpbid 231 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝐴 / 𝑦) ∈ ℤ) |
19 | 15 | zcnd 12427 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℂ) |
20 | | nncn 11981 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
21 | 20 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℂ) |
22 | 19, 21, 13 | divcan2d 11753 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · (𝐴 / 𝑦)) = 𝐴) |
23 | | simplr 766 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ 𝐼) |
24 | 22, 23 | eqeltrd 2839 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) |
25 | | zringbas 20676 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
26 | | eqid 2738 |
. . . . . . . 8
⊢
(Unit‘ℤring) =
(Unit‘ℤring) |
27 | | zringmulr 20679 |
. . . . . . . 8
⊢ ·
= (.r‘ℤring) |
28 | 2, 25, 26, 27 | irredmul 19951 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ (𝐴 / 𝑦) ∈ ℤ ∧ (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) → (𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring))) |
29 | 10, 18, 24, 28 | syl3anc 1370 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring))) |
30 | | zringunit 20688 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(Unit‘ℤring) ↔ (𝑦 ∈ ℤ ∧ (abs‘𝑦) = 1)) |
31 | 30 | baib 536 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → (𝑦 ∈
(Unit‘ℤring) ↔ (abs‘𝑦) = 1)) |
32 | 10, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑦) =
1)) |
33 | | nnnn0 12240 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
34 | | nn0re 12242 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
35 | | nn0ge0 12258 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 0 ≤ 𝑦) |
36 | 34, 35 | absidd 15134 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (abs‘𝑦) =
𝑦) |
37 | 33, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(abs‘𝑦) = 𝑦) |
38 | 37 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (abs‘𝑦) = 𝑦) |
39 | 38 | eqeq1d 2740 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘𝑦) = 1 ↔ 𝑦 = 1)) |
40 | 32, 39 | bitrd 278 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
↔ 𝑦 =
1)) |
41 | | zringunit 20688 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ ((𝐴 / 𝑦) ∈ ℤ ∧
(abs‘(𝐴 / 𝑦)) = 1)) |
42 | 41 | baib 536 |
. . . . . . . . 9
⊢ ((𝐴 / 𝑦) ∈ ℤ → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ (abs‘(𝐴 /
𝑦)) = 1)) |
43 | 18, 42 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ (abs‘(𝐴 /
𝑦)) = 1)) |
44 | | nnre 11980 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
45 | 44 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℝ) |
46 | | simprl 768 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℕ) |
47 | 45, 46 | nndivred 12027 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝐴 / 𝑦) ∈ ℝ) |
48 | | nnnn0 12240 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
49 | | nn0ge0 12258 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
51 | 50 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 ≤ 𝐴) |
52 | 46 | nnred 11988 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℝ) |
53 | | nngt0 12004 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
54 | 53 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 < 𝑦) |
55 | | divge0 11844 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 0 <
𝑦)) → 0 ≤ (𝐴 / 𝑦)) |
56 | 45, 51, 52, 54, 55 | syl22anc 836 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 ≤ (𝐴 / 𝑦)) |
57 | 47, 56 | absidd 15134 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (abs‘(𝐴 / 𝑦)) = (𝐴 / 𝑦)) |
58 | 57 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ (𝐴 / 𝑦) = 1)) |
59 | | 1cnd 10970 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 1 ∈ ℂ) |
60 | 19, 21, 59, 13 | divmuld 11773 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) = 1 ↔ (𝑦 · 1) = 𝐴)) |
61 | 21 | mulid1d 10992 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · 1) = 𝑦) |
62 | 61 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝑦 · 1) = 𝐴 ↔ 𝑦 = 𝐴)) |
63 | 58, 60, 62 | 3bitrd 305 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ 𝑦 = 𝐴)) |
64 | 43, 63 | bitrd 278 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ 𝑦 = 𝐴)) |
65 | 40, 64 | orbi12d 916 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring)) ↔ (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
66 | 29, 65 | mpbid 231 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 = 1 ∨ 𝑦 = 𝐴)) |
67 | 66 | expr 457 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ 𝑦 ∈ ℕ) → (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
68 | 67 | ralrimiva 3103 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
69 | | isprm2 16387 |
. . 3
⊢ (𝐴 ∈ ℙ ↔ (𝐴 ∈
(ℤ≥‘2) ∧ ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))) |
70 | 8, 68, 69 | sylanbrc 583 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ ℙ) |
71 | | prmz 16380 |
. . . 4
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℤ) |
72 | | 1nprm 16384 |
. . . . 5
⊢ ¬ 1
∈ ℙ |
73 | | zringunit 20688 |
. . . . . 6
⊢ (𝐴 ∈
(Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) |
74 | | prmnn 16379 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℕ) |
75 | | nn0re 12242 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
76 | 75, 49 | absidd 15134 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ (abs‘𝐴) =
𝐴) |
77 | 74, 48, 76 | 3syl 18 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ →
(abs‘𝐴) = 𝐴) |
78 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℙ) |
79 | 77, 78 | eqeltrd 2839 |
. . . . . . . 8
⊢ (𝐴 ∈ ℙ →
(abs‘𝐴) ∈
ℙ) |
80 | | eleq1 2826 |
. . . . . . . 8
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)
∈ ℙ ↔ 1 ∈ ℙ)) |
81 | 79, 80 | syl5ibcom 244 |
. . . . . . 7
⊢ (𝐴 ∈ ℙ →
((abs‘𝐴) = 1 → 1
∈ ℙ)) |
82 | 81 | adantld 491 |
. . . . . 6
⊢ (𝐴 ∈ ℙ → ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) → 1
∈ ℙ)) |
83 | 73, 82 | syl5bi 241 |
. . . . 5
⊢ (𝐴 ∈ ℙ → (𝐴 ∈
(Unit‘ℤring) → 1 ∈ ℙ)) |
84 | 72, 83 | mtoi 198 |
. . . 4
⊢ (𝐴 ∈ ℙ → ¬
𝐴 ∈
(Unit‘ℤring)) |
85 | | dvdsmul1 15987 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∥ (𝑥 · 𝑦)) |
86 | 85 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ (𝑥 · 𝑦)) |
87 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) = 𝐴) |
88 | 86, 87 | breqtrd 5100 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ 𝐴) |
89 | | simplrl 774 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℤ) |
90 | 71 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℤ) |
91 | | absdvdsb 15984 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑥 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
92 | 89, 90, 91 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
93 | 88, 92 | mpbid 231 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∥ 𝐴) |
94 | | breq1 5077 |
. . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑥) → (𝑦 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
95 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑥) → (𝑦 = 1 ↔ (abs‘𝑥) = 1)) |
96 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑥) → (𝑦 = 𝐴 ↔ (abs‘𝑥) = 𝐴)) |
97 | 95, 96 | orbi12d 916 |
. . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑥) → ((𝑦 = 1 ∨ 𝑦 = 𝐴) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
98 | 94, 97 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑦 = (abs‘𝑥) → ((𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)) ↔ ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))) |
99 | 69 | simprbi 497 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℙ →
∀𝑦 ∈ ℕ
(𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
100 | 99 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
101 | 89 | zcnd 12427 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℂ) |
102 | 74 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℕ) |
103 | 102 | nnne0d 12023 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ≠ 0) |
104 | | simplrr 775 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℤ) |
105 | 104 | zcnd 12427 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℂ) |
106 | 105 | mul02d 11173 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (0 · 𝑦) = 0) |
107 | 103, 87, 106 | 3netr4d 3021 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) ≠ (0 · 𝑦)) |
108 | | oveq1 7282 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0 → (𝑥 · 𝑦) = (0 · 𝑦)) |
109 | 108 | necon3i 2976 |
. . . . . . . . . . . . 13
⊢ ((𝑥 · 𝑦) ≠ (0 · 𝑦) → 𝑥 ≠ 0) |
110 | 107, 109 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ≠ 0) |
111 | 101, 110 | absne0d 15159 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ≠ 0) |
112 | 111 | neneqd 2948 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ¬ (abs‘𝑥) = 0) |
113 | | nn0abscl 15024 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ →
(abs‘𝑥) ∈
ℕ0) |
114 | 89, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈
ℕ0) |
115 | | elnn0 12235 |
. . . . . . . . . . . 12
⊢
((abs‘𝑥)
∈ ℕ0 ↔ ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0)) |
116 | 114, 115 | sylib 217 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0)) |
117 | 116 | ord 861 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (¬ (abs‘𝑥) ∈ ℕ →
(abs‘𝑥) =
0)) |
118 | 112, 117 | mt3d 148 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℕ) |
119 | 98, 100, 118 | rspcdva 3562 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
120 | 93, 119 | mpd 15 |
. . . . . . 7
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)) |
121 | | zringunit 20688 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(Unit‘ℤring) ↔ (𝑥 ∈ ℤ ∧ (abs‘𝑥) = 1)) |
122 | 121 | baib 536 |
. . . . . . . . 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 15148 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℝ) |
126 | 125 | recnd 11003 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℂ) |
127 | | 1cnd 10970 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 1 ∈ ℂ) |
128 | 101 | abscld 15148 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℝ) |
129 | 128 | recnd 11003 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℂ) |
130 | 126, 127,
129, 111 | mulcand 11608 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑦) = 1)) |
131 | 87 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = (abs‘𝐴)) |
132 | 101, 105 | absmuld 15166 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = ((abs‘𝑥) · (abs‘𝑦))) |
133 | 77 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝐴) = 𝐴) |
134 | 131, 132,
133 | 3eqtr3d 2786 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · (abs‘𝑦)) = 𝐴) |
135 | 129 | mulid1d 10992 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · 1) = (abs‘𝑥)) |
136 | 134, 135 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ 𝐴 = (abs‘𝑥))) |
137 | | eqcom 2745 |
. . . . . . . . . 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 916 |
. . . . . . 7
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
141 | 120, 140 | mpbird 256 |
. . . . . 6
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring))) |
142 | 141 | ex 413 |
. . . . 5
⊢ ((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)))) |
143 | 142 | ralrimivva 3123 |
. . . 4
⊢ (𝐴 ∈ ℙ →
∀𝑥 ∈ ℤ
∀𝑦 ∈ ℤ
((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)))) |
144 | 25, 26, 2, 27 | isirred2 19943 |
. . . 4
⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈
(Unit‘ℤring) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring))))) |
145 | 71, 84, 143, 144 | syl3anbrc 1342 |
. . 3
⊢ (𝐴 ∈ ℙ → 𝐴 ∈ 𝐼) |
146 | 145 | adantl 482 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ ℙ) → 𝐴 ∈ 𝐼) |
147 | 70, 146 | impbida 798 |
1
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |