Step | Hyp | Ref
| Expression |
1 | | df-ne 2782 |
. . 3
⊢
((chr‘𝑅) ≠
0 ↔ ¬ (chr‘𝑅) = 0) |
2 | | domnring 19117 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) |
3 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(chr‘𝑅) =
(chr‘𝑅) |
4 | 3 | chrcl 19693 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(chr‘𝑅) ∈
ℕ0) |
5 | 2, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Domn →
(chr‘𝑅) ∈
ℕ0) |
6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ∈
ℕ0) |
7 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ≠
0) |
8 | | eldifsn 4260 |
. . . . . . . 8
⊢
((chr‘𝑅)
∈ (ℕ0 ∖ {0}) ↔ ((chr‘𝑅) ∈ ℕ0 ∧
(chr‘𝑅) ≠
0)) |
9 | 6, 7, 8 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ∈
(ℕ0 ∖ {0})) |
10 | | dfn2 11182 |
. . . . . . 7
⊢ ℕ =
(ℕ0 ∖ {0}) |
11 | 9, 10 | syl6eleqr 2699 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ∈
ℕ) |
12 | | domnnzr 19116 |
. . . . . . . 8
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
13 | | nzrring 19082 |
. . . . . . . . . 10
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
14 | | chrnzr 19697 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔
(chr‘𝑅) ≠
1)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ NzRing → (𝑅 ∈ NzRing ↔
(chr‘𝑅) ≠
1)) |
16 | 15 | ibi 255 |
. . . . . . . 8
⊢ (𝑅 ∈ NzRing →
(chr‘𝑅) ≠
1) |
17 | 12, 16 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ Domn →
(chr‘𝑅) ≠
1) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ≠
1) |
19 | | eluz2b3 11638 |
. . . . . 6
⊢
((chr‘𝑅)
∈ (ℤ≥‘2) ↔ ((chr‘𝑅) ∈ ℕ ∧ (chr‘𝑅) ≠ 1)) |
20 | 11, 18, 19 | sylanbrc 695 |
. . . . 5
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ∈
(ℤ≥‘2)) |
21 | 2 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
𝑅 ∈
Ring) |
22 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
23 | 22 | zrhrhm 19679 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(ℤRHom‘𝑅)
∈ (ℤring RingHom 𝑅)) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(ℤRHom‘𝑅)
∈ (ℤring RingHom 𝑅)) |
25 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
𝑥 ∈
ℤ) |
26 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
𝑦 ∈
ℤ) |
27 | | zringbas 19643 |
. . . . . . . . . . . 12
⊢ ℤ =
(Base‘ℤring) |
28 | | zringmulr 19646 |
. . . . . . . . . . . 12
⊢ ·
= (.r‘ℤring) |
29 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
30 | 27, 28, 29 | rhmmul 18550 |
. . . . . . . . . . 11
⊢
(((ℤRHom‘𝑅) ∈ (ℤring RingHom
𝑅) ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) →
((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (((ℤRHom‘𝑅)‘𝑥)(.r‘𝑅)((ℤRHom‘𝑅)‘𝑦))) |
31 | 24, 25, 26, 30 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (((ℤRHom‘𝑅)‘𝑥)(.r‘𝑅)((ℤRHom‘𝑅)‘𝑦))) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (0g‘𝑅) ↔ (((ℤRHom‘𝑅)‘𝑥)(.r‘𝑅)((ℤRHom‘𝑅)‘𝑦)) = (0g‘𝑅))) |
33 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
𝑅 ∈
Domn) |
34 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘𝑅) |
35 | 27, 34 | rhmf 18549 |
. . . . . . . . . . . 12
⊢
((ℤRHom‘𝑅) ∈ (ℤring RingHom
𝑅) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) |
36 | 24, 35 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) |
37 | 36, 25 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((ℤRHom‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
38 | 36, 26 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((ℤRHom‘𝑅)‘𝑦) ∈ (Base‘𝑅)) |
39 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
40 | 34, 29, 39 | domneq0 19118 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Domn ∧
((ℤRHom‘𝑅)‘𝑥) ∈ (Base‘𝑅) ∧ ((ℤRHom‘𝑅)‘𝑦) ∈ (Base‘𝑅)) → ((((ℤRHom‘𝑅)‘𝑥)(.r‘𝑅)((ℤRHom‘𝑅)‘𝑦)) = (0g‘𝑅) ↔ (((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅) ∨ ((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅)))) |
41 | 33, 37, 38, 40 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((((ℤRHom‘𝑅)‘𝑥)(.r‘𝑅)((ℤRHom‘𝑅)‘𝑦)) = (0g‘𝑅) ↔ (((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅) ∨ ((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅)))) |
42 | 32, 41 | bitrd 267 |
. . . . . . . 8
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (0g‘𝑅) ↔ (((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅) ∨ ((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅)))) |
43 | 42 | biimpd 218 |
. . . . . . 7
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (0g‘𝑅) → (((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅) ∨ ((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅)))) |
44 | | zmulcl 11303 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
45 | 44 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(𝑥 · 𝑦) ∈
ℤ) |
46 | 3, 22, 39 | chrdvds 19695 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 · 𝑦) ∈ ℤ) → ((chr‘𝑅) ∥ (𝑥 · 𝑦) ↔ ((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (0g‘𝑅))) |
47 | 21, 45, 46 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((chr‘𝑅) ∥
(𝑥 · 𝑦) ↔
((ℤRHom‘𝑅)‘(𝑥 · 𝑦)) = (0g‘𝑅))) |
48 | 3, 22, 39 | chrdvds 19695 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ ℤ) →
((chr‘𝑅) ∥
𝑥 ↔
((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅))) |
49 | 21, 25, 48 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((chr‘𝑅) ∥
𝑥 ↔
((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅))) |
50 | 3, 22, 39 | chrdvds 19695 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ ℤ) →
((chr‘𝑅) ∥
𝑦 ↔
((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅))) |
51 | 21, 26, 50 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((chr‘𝑅) ∥
𝑦 ↔
((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅))) |
52 | 49, 51 | orbi12d 742 |
. . . . . . 7
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
(((chr‘𝑅) ∥
𝑥 ∨ (chr‘𝑅) ∥ 𝑦) ↔ (((ℤRHom‘𝑅)‘𝑥) = (0g‘𝑅) ∨ ((ℤRHom‘𝑅)‘𝑦) = (0g‘𝑅)))) |
53 | 43, 47, 52 | 3imtr4d 282 |
. . . . . 6
⊢ (((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ)) →
((chr‘𝑅) ∥
(𝑥 · 𝑦) → ((chr‘𝑅) ∥ 𝑥 ∨ (chr‘𝑅) ∥ 𝑦))) |
54 | 53 | ralrimivva 2954 |
. . . . 5
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ ∀𝑥 ∈
ℤ ∀𝑦 ∈
ℤ ((chr‘𝑅)
∥ (𝑥 · 𝑦) → ((chr‘𝑅) ∥ 𝑥 ∨ (chr‘𝑅) ∥ 𝑦))) |
55 | | isprm6 15264 |
. . . . 5
⊢
((chr‘𝑅)
∈ ℙ ↔ ((chr‘𝑅) ∈ (ℤ≥‘2)
∧ ∀𝑥 ∈
ℤ ∀𝑦 ∈
ℤ ((chr‘𝑅)
∥ (𝑥 · 𝑦) → ((chr‘𝑅) ∥ 𝑥 ∨ (chr‘𝑅) ∥ 𝑦)))) |
56 | 20, 54, 55 | sylanbrc 695 |
. . . 4
⊢ ((𝑅 ∈ Domn ∧
(chr‘𝑅) ≠ 0)
→ (chr‘𝑅) ∈
ℙ) |
57 | 56 | ex 449 |
. . 3
⊢ (𝑅 ∈ Domn →
((chr‘𝑅) ≠ 0
→ (chr‘𝑅) ∈
ℙ)) |
58 | 1, 57 | syl5bir 232 |
. 2
⊢ (𝑅 ∈ Domn → (¬
(chr‘𝑅) = 0 →
(chr‘𝑅) ∈
ℙ)) |
59 | 58 | orrd 392 |
1
⊢ (𝑅 ∈ Domn →
((chr‘𝑅) = 0 ∨
(chr‘𝑅) ∈
ℙ)) |