Step | Hyp | Ref
| Expression |
1 | | zringring 19640 |
. . . . . 6
⊢
ℤring ∈ Ring |
2 | | prmirred.i |
. . . . . . 7
⊢ 𝐼 =
(Irred‘ℤring) |
3 | | zring1 19648 |
. . . . . . 7
⊢ 1 =
(1r‘ℤring) |
4 | 2, 3 | irredn1 18529 |
. . . . . 6
⊢
((ℤring ∈ Ring ∧ 𝐴 ∈ 𝐼) → 𝐴 ≠ 1) |
5 | 1, 4 | mpan 702 |
. . . . 5
⊢ (𝐴 ∈ 𝐼 → 𝐴 ≠ 1) |
6 | 5 | anim2i 591 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1)) |
7 | | eluz2b3 11638 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) ↔ (𝐴 ∈ ℕ ∧ 𝐴 ≠ 1)) |
8 | 6, 7 | sylibr 223 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈
(ℤ≥‘2)) |
9 | | nnz 11276 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
10 | 9 | ad2antrl 760 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℤ) |
11 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∥ 𝐴) |
12 | | nnne0 10930 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
13 | 12 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ≠ 0) |
14 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
15 | 14 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℤ) |
16 | | dvdsval2 14824 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝐴 ∈ ℤ) → (𝑦 ∥ 𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ)) |
17 | 10, 13, 15, 16 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∥ 𝐴 ↔ (𝐴 / 𝑦) ∈ ℤ)) |
18 | 11, 17 | mpbid 221 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝐴 / 𝑦) ∈ ℤ) |
19 | 15 | zcnd 11359 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℂ) |
20 | | nncn 10905 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
21 | 20 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℂ) |
22 | 19, 21, 13 | divcan2d 10682 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · (𝐴 / 𝑦)) = 𝐴) |
23 | | simplr 788 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ 𝐼) |
24 | 22, 23 | eqeltrd 2688 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) |
25 | | zringbas 19643 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
26 | | eqid 2610 |
. . . . . . . 8
⊢
(Unit‘ℤring) =
(Unit‘ℤring) |
27 | | zringmulr 19646 |
. . . . . . . 8
⊢ ·
= (.r‘ℤring) |
28 | 2, 25, 26, 27 | irredmul 18532 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ (𝐴 / 𝑦) ∈ ℤ ∧ (𝑦 · (𝐴 / 𝑦)) ∈ 𝐼) → (𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring))) |
29 | 10, 18, 24, 28 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring))) |
30 | | zringunit 19655 |
. . . . . . . . . 10
⊢ (𝑦 ∈
(Unit‘ℤring) ↔ (𝑦 ∈ ℤ ∧ (abs‘𝑦) = 1)) |
31 | 30 | baib 942 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℤ → (𝑦 ∈
(Unit‘ℤring) ↔ (abs‘𝑦) = 1)) |
32 | 10, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑦) =
1)) |
33 | | nnnn0 11176 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
34 | | nn0re 11178 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
35 | | nn0ge0 11195 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ 0 ≤ 𝑦) |
36 | 34, 35 | absidd 14009 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (abs‘𝑦) =
𝑦) |
37 | 33, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(abs‘𝑦) = 𝑦) |
38 | 37 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (abs‘𝑦) = 𝑦) |
39 | 38 | eqeq1d 2612 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘𝑦) = 1 ↔ 𝑦 = 1)) |
40 | 32, 39 | bitrd 267 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 ∈ (Unit‘ℤring)
↔ 𝑦 =
1)) |
41 | | zringunit 19655 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ ((𝐴 / 𝑦) ∈ ℤ ∧
(abs‘(𝐴 / 𝑦)) = 1)) |
42 | 41 | baib 942 |
. . . . . . . . 9
⊢ ((𝐴 / 𝑦) ∈ ℤ → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ (abs‘(𝐴 /
𝑦)) = 1)) |
43 | 18, 42 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ (abs‘(𝐴 /
𝑦)) = 1)) |
44 | | nnre 10904 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
45 | 44 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝐴 ∈ ℝ) |
46 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℕ) |
47 | 45, 46 | nndivred 10946 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝐴 / 𝑦) ∈ ℝ) |
48 | | nnnn0 11176 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
49 | | nn0ge0 11195 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ0
→ 0 ≤ 𝐴) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 0 ≤
𝐴) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 ≤ 𝐴) |
52 | 46 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 𝑦 ∈ ℝ) |
53 | | nngt0 10926 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 0 <
𝑦) |
54 | 53 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 < 𝑦) |
55 | | divge0 10771 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝑦 ∈ ℝ ∧ 0 <
𝑦)) → 0 ≤ (𝐴 / 𝑦)) |
56 | 45, 51, 52, 54, 55 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 0 ≤ (𝐴 / 𝑦)) |
57 | 47, 56 | absidd 14009 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (abs‘(𝐴 / 𝑦)) = (𝐴 / 𝑦)) |
58 | 57 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ (𝐴 / 𝑦) = 1)) |
59 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → 1 ∈ ℂ) |
60 | 19, 21, 59, 13 | divmuld 10702 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) = 1 ↔ (𝑦 · 1) = 𝐴)) |
61 | 21 | mulid1d 9936 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 · 1) = 𝑦) |
62 | 61 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝑦 · 1) = 𝐴 ↔ 𝑦 = 𝐴)) |
63 | 58, 60, 62 | 3bitrd 293 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((abs‘(𝐴 / 𝑦)) = 1 ↔ 𝑦 = 𝐴)) |
64 | 43, 63 | bitrd 267 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝐴 / 𝑦) ∈ (Unit‘ℤring)
↔ 𝑦 = 𝐴)) |
65 | 40, 64 | orbi12d 742 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → ((𝑦 ∈ (Unit‘ℤring)
∨ (𝐴 / 𝑦) ∈
(Unit‘ℤring)) ↔ (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
66 | 29, 65 | mpbid 221 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐴)) → (𝑦 = 1 ∨ 𝑦 = 𝐴)) |
67 | 66 | expr 641 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) ∧ 𝑦 ∈ ℕ) → (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
68 | 67 | ralrimiva 2949 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
69 | | isprm2 15233 |
. . 3
⊢ (𝐴 ∈ ℙ ↔ (𝐴 ∈
(ℤ≥‘2) ∧ ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)))) |
70 | 8, 68, 69 | sylanbrc 695 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ ℙ) |
71 | | prmz 15227 |
. . . 4
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℤ) |
72 | | 1nprm 15230 |
. . . . 5
⊢ ¬ 1
∈ ℙ |
73 | | zringunit 19655 |
. . . . . 6
⊢ (𝐴 ∈
(Unit‘ℤring) ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) = 1)) |
74 | | prmnn 15226 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℕ) |
75 | | nn0re 11178 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
76 | 75, 49 | absidd 14009 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ (abs‘𝐴) =
𝐴) |
77 | 74, 48, 76 | 3syl 18 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ →
(abs‘𝐴) = 𝐴) |
78 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ → 𝐴 ∈
ℙ) |
79 | 77, 78 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝐴 ∈ ℙ →
(abs‘𝐴) ∈
ℙ) |
80 | | eleq1 2676 |
. . . . . . . 8
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)
∈ ℙ ↔ 1 ∈ ℙ)) |
81 | 79, 80 | syl5ibcom 234 |
. . . . . . 7
⊢ (𝐴 ∈ ℙ →
((abs‘𝐴) = 1 → 1
∈ ℙ)) |
82 | 81 | adantld 482 |
. . . . . 6
⊢ (𝐴 ∈ ℙ → ((𝐴 ∈ ℤ ∧
(abs‘𝐴) = 1) → 1
∈ ℙ)) |
83 | 73, 82 | syl5bi 231 |
. . . . 5
⊢ (𝐴 ∈ ℙ → (𝐴 ∈
(Unit‘ℤring) → 1 ∈ ℙ)) |
84 | 72, 83 | mtoi 189 |
. . . 4
⊢ (𝐴 ∈ ℙ → ¬
𝐴 ∈
(Unit‘ℤring)) |
85 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℤ) |
86 | 85 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∈ ℂ) |
87 | 74 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℕ) |
88 | 87 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ≠ 0) |
89 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) = 𝐴) |
90 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℤ) |
91 | 90 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑦 ∈ ℂ) |
92 | 91 | mul02d 10113 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (0 · 𝑦) = 0) |
93 | 88, 89, 92 | 3netr4d 2859 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 · 𝑦) ≠ (0 · 𝑦)) |
94 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (𝑥 · 𝑦) = (0 · 𝑦)) |
95 | 94 | necon3i 2814 |
. . . . . . . . . . . 12
⊢ ((𝑥 · 𝑦) ≠ (0 · 𝑦) → 𝑥 ≠ 0) |
96 | 93, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ≠ 0) |
97 | 86, 96 | absne0d 14034 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ≠ 0) |
98 | 97 | neneqd 2787 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ¬ (abs‘𝑥) = 0) |
99 | | nn0abscl 13900 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ →
(abs‘𝑥) ∈
ℕ0) |
100 | 85, 99 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈
ℕ0) |
101 | | elnn0 11171 |
. . . . . . . . . . 11
⊢
((abs‘𝑥)
∈ ℕ0 ↔ ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0)) |
102 | 100, 101 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) ∈ ℕ ∨ (abs‘𝑥) = 0)) |
103 | 102 | ord 391 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (¬ (abs‘𝑥) ∈ ℕ →
(abs‘𝑥) =
0)) |
104 | 98, 103 | mt3d 139 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℕ) |
105 | 69 | simprbi 479 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℙ →
∀𝑦 ∈ ℕ
(𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
106 | 105 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴))) |
107 | | dvdsmul1 14841 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → 𝑥 ∥ (𝑥 · 𝑦)) |
108 | 107 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ (𝑥 · 𝑦)) |
109 | 108, 89 | breqtrd 4609 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝑥 ∥ 𝐴) |
110 | 71 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 𝐴 ∈ ℤ) |
111 | | absdvdsb 14838 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑥 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
112 | 85, 110, 111 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
113 | 109, 112 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∥ 𝐴) |
114 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑥) → (𝑦 ∥ 𝐴 ↔ (abs‘𝑥) ∥ 𝐴)) |
115 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑥) → (𝑦 = 1 ↔ (abs‘𝑥) = 1)) |
116 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑥) → (𝑦 = 𝐴 ↔ (abs‘𝑥) = 𝐴)) |
117 | 115, 116 | orbi12d 742 |
. . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑥) → ((𝑦 = 1 ∨ 𝑦 = 𝐴) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
118 | 114, 117 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑦 = (abs‘𝑥) → ((𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)) ↔ ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))) |
119 | 118 | rspcv 3278 |
. . . . . . . 8
⊢
((abs‘𝑥)
∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 ∥ 𝐴 → (𝑦 = 1 ∨ 𝑦 = 𝐴)) → ((abs‘𝑥) ∥ 𝐴 → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)))) |
120 | 104, 106,
113, 119 | syl3c 64 |
. . . . . . 7
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴)) |
121 | | zringunit 19655 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(Unit‘ℤring) ↔ (𝑥 ∈ ℤ ∧ (abs‘𝑥) = 1)) |
122 | 121 | baib 942 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → (𝑥 ∈
(Unit‘ℤring) ↔ (abs‘𝑥) = 1)) |
123 | 85, 122 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring)
↔ (abs‘𝑥) =
1)) |
124 | 90, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑦) =
1)) |
125 | 91 | abscld 14023 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℝ) |
126 | 125 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑦) ∈ ℂ) |
127 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → 1 ∈ ℂ) |
128 | 86 | abscld 14023 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℝ) |
129 | 128 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝑥) ∈ ℂ) |
130 | 126, 127,
129, 97 | mulcand 10539 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑦) = 1)) |
131 | 89 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = (abs‘𝐴)) |
132 | 86, 91 | absmuld 14041 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘(𝑥 · 𝑦)) = ((abs‘𝑥) · (abs‘𝑦))) |
133 | 77 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (abs‘𝐴) = 𝐴) |
134 | 131, 132,
133 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · (abs‘𝑦)) = 𝐴) |
135 | 129 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((abs‘𝑥) · 1) = (abs‘𝑥)) |
136 | 134, 135 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ 𝐴 = (abs‘𝑥))) |
137 | | eqcom 2617 |
. . . . . . . . . 10
⊢ (𝐴 = (abs‘𝑥) ↔ (abs‘𝑥) = 𝐴) |
138 | 136, 137 | syl6bb 275 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (((abs‘𝑥) · (abs‘𝑦)) = ((abs‘𝑥) · 1) ↔ (abs‘𝑥) = 𝐴)) |
139 | 124, 130,
138 | 3bitr2d 295 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑦 ∈ (Unit‘ℤring)
↔ (abs‘𝑥) =
𝐴)) |
140 | 123, 139 | orbi12d 742 |
. . . . . . 7
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → ((𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)) ↔ ((abs‘𝑥) = 1 ∨ (abs‘𝑥) = 𝐴))) |
141 | 120, 140 | mpbird 246 |
. . . . . 6
⊢ (((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) ∧ (𝑥 · 𝑦) = 𝐴) → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring))) |
142 | 141 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)))) |
143 | 142 | ralrimivva 2954 |
. . . 4
⊢ (𝐴 ∈ ℙ →
∀𝑥 ∈ ℤ
∀𝑦 ∈ ℤ
((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring)))) |
144 | 25, 26, 2, 27 | isirred2 18524 |
. . . 4
⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ ¬ 𝐴 ∈
(Unit‘ℤring) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ ((𝑥 · 𝑦) = 𝐴 → (𝑥 ∈ (Unit‘ℤring)
∨ 𝑦 ∈
(Unit‘ℤring))))) |
145 | 71, 84, 143, 144 | syl3anbrc 1239 |
. . 3
⊢ (𝐴 ∈ ℙ → 𝐴 ∈ 𝐼) |
146 | 145 | adantl 481 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ∈ ℙ) → 𝐴 ∈ 𝐼) |
147 | 70, 146 | impbida 873 |
1
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ 𝐼 ↔ 𝐴 ∈ ℙ)) |