Step | Hyp | Ref
| Expression |
1 | | 2z 9331 |
. . . . . 6
⊢ 2 ∈
ℤ |
2 | 1 | a1i 9 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ∈
ℤ) |
3 | | nnz 9322 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
4 | 3 | adantr 276 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈
ℤ) |
5 | | hash2 10857 |
. . . . . . 7
⊢
(♯‘2o) = 2 |
6 | | isidom 13736 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
7 | 6 | simprbi 275 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ Domn) |
8 | | domnnzr 13730 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Domn → 𝑌 ∈ NzRing) |
9 | 7, 8 | syl 14 |
. . . . . . . . . 10
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ NzRing) |
10 | | eqid 2189 |
. . . . . . . . . . . 12
⊢
(Base‘𝑌) =
(Base‘𝑌) |
11 | 10 | isnzr2 13644 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ NzRing ↔ (𝑌 ∈ Ring ∧ 2o
≼ (Base‘𝑌))) |
12 | 11 | simprbi 275 |
. . . . . . . . . 10
⊢ (𝑌 ∈ NzRing →
2o ≼ (Base‘𝑌)) |
13 | 9, 12 | syl 14 |
. . . . . . . . 9
⊢ (𝑌 ∈ IDomn →
2o ≼ (Base‘𝑌)) |
14 | 13 | adantl 277 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
2o ≼ (Base‘𝑌)) |
15 | | 2onn 6561 |
. . . . . . . . . 10
⊢
2o ∈ ω |
16 | | nnfi 6915 |
. . . . . . . . . 10
⊢
(2o ∈ ω → 2o ∈
Fin) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
⊢
2o ∈ Fin |
18 | | zntos.y |
. . . . . . . . . . 11
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
19 | 18, 10 | znfi 14100 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(Base‘𝑌) ∈
Fin) |
20 | 19 | adantr 276 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
(Base‘𝑌) ∈
Fin) |
21 | | fihashdom 10848 |
. . . . . . . . 9
⊢
((2o ∈ Fin ∧ (Base‘𝑌) ∈ Fin) →
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌))) |
22 | 17, 20, 21 | sylancr 414 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌))) |
23 | 14, 22 | mpbird 167 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
(♯‘2o) ≤ (♯‘(Base‘𝑌))) |
24 | 5, 23 | eqbrtrrid 4061 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ≤
(♯‘(Base‘𝑌))) |
25 | 18, 10 | znhash 14101 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(♯‘(Base‘𝑌)) = 𝑁) |
26 | 25 | adantr 276 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
(♯‘(Base‘𝑌)) = 𝑁) |
27 | 24, 26 | breqtrd 4051 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ≤
𝑁) |
28 | | eluz2 9584 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
29 | 2, 4, 27, 28 | syl3anbrc 1183 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈
(ℤ≥‘2)) |
30 | | nncn 8976 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
31 | 30 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈ ℂ) |
32 | | nncn 8976 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) |
33 | 32 | ad2antrl 490 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℂ) |
34 | | nnap0 8997 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 # 0) |
35 | 34 | ad2antrl 490 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 # 0) |
36 | 31, 33, 35 | divcanap1d 8796 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((𝑁 / 𝑥) · 𝑥) = 𝑁) |
37 | 36 | fveq2d 5546 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = ((ℤRHom‘𝑌)‘𝑁)) |
38 | 7 | ad2antlr 489 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑌 ∈ Domn) |
39 | | domnring 13731 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ Domn → 𝑌 ∈ Ring) |
40 | 38, 39 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑌 ∈ Ring) |
41 | | eqid 2189 |
. . . . . . . . . . . 12
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
42 | 41 | zrhrhm 14068 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
43 | 40, 42 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (ℤRHom‘𝑌) ∈ (ℤring
RingHom 𝑌)) |
44 | | simprr 531 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∥ 𝑁) |
45 | | nnz 9322 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
46 | 45 | ad2antrl 490 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℤ) |
47 | | nnne0 8996 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) |
48 | 47 | ad2antrl 490 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ≠ 0) |
49 | 3 | ad2antrr 488 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈ ℤ) |
50 | | dvdsval2 11907 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑥 ∥ 𝑁 ↔ (𝑁 / 𝑥) ∈ ℤ)) |
51 | 46, 48, 49, 50 | syl3anc 1249 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 ∥ 𝑁 ↔ (𝑁 / 𝑥) ∈ ℤ)) |
52 | 44, 51 | mpbid 147 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 / 𝑥) ∈ ℤ) |
53 | | zringbas 14042 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
54 | | zringmulr 14045 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
55 | | eqid 2189 |
. . . . . . . . . . 11
⊢
(.r‘𝑌) = (.r‘𝑌) |
56 | 53, 54, 55 | rhmmul 13624 |
. . . . . . . . . 10
⊢
(((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) ∧ (𝑁 / 𝑥) ∈ ℤ ∧ 𝑥 ∈ ℤ) →
((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥))) |
57 | 43, 52, 46, 56 | syl3anc 1249 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥))) |
58 | | iddvds 11921 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁) |
59 | 49, 58 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∥ 𝑁) |
60 | | nnnn0 9233 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
61 | 60 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈
ℕ0) |
62 | | eqid 2189 |
. . . . . . . . . . . 12
⊢
(0g‘𝑌) = (0g‘𝑌) |
63 | 18, 41, 62 | zndvds0 14095 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑁) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑁)) |
64 | 61, 49, 63 | syl2anc 411 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘𝑁) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑁)) |
65 | 59, 64 | mpbird 167 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘𝑁) = (0g‘𝑌)) |
66 | 37, 57, 65 | 3eqtr3d 2230 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g‘𝑌)) |
67 | 53, 10 | rhmf 13623 |
. . . . . . . . . . 11
⊢
((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) →
(ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) |
68 | 43, 67 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) |
69 | 68, 52 | ffvelcdmd 5682 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) ∈ (Base‘𝑌)) |
70 | 68, 46 | ffvelcdmd 5682 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘𝑥) ∈ (Base‘𝑌)) |
71 | 10, 55, 62 | domneq0 13732 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Domn ∧
((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) ∈ (Base‘𝑌) ∧ ((ℤRHom‘𝑌)‘𝑥) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌)))) |
72 | 38, 69, 70, 71 | syl3anc 1249 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌)))) |
73 | 66, 72 | mpbid 147 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌))) |
74 | 18, 41, 62 | zndvds0 14095 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 / 𝑥) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / 𝑥))) |
75 | 61, 52, 74 | syl2anc 411 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / 𝑥))) |
76 | | nnre 8975 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈ ℝ) |
78 | | nnre 8975 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
79 | 78 | ad2antrl 490 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℝ) |
80 | | nngt0 8993 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
81 | 80 | ad2antrr 488 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < 𝑁) |
82 | | nngt0 8993 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ → 0 <
𝑥) |
83 | 82 | ad2antrl 490 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < 𝑥) |
84 | 77, 79, 81, 83 | divgt0d 8940 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < (𝑁 / 𝑥)) |
85 | | elnnz 9313 |
. . . . . . . . . . . 12
⊢ ((𝑁 / 𝑥) ∈ ℕ ↔ ((𝑁 / 𝑥) ∈ ℤ ∧ 0 < (𝑁 / 𝑥))) |
86 | 52, 84, 85 | sylanbrc 417 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 / 𝑥) ∈ ℕ) |
87 | | dvdsle 11960 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 𝑥) ∈ ℕ) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑁 ≤ (𝑁 / 𝑥))) |
88 | 49, 86, 87 | syl2anc 411 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑁 ≤ (𝑁 / 𝑥))) |
89 | | 1red 8020 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 1 ∈ ℝ) |
90 | | 0lt1 8132 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
91 | 90 | a1i 9 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < 1) |
92 | | lediv2 8896 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 0 <
𝑥) ∧ (1 ∈ ℝ
∧ 0 < 1) ∧ (𝑁
∈ ℝ ∧ 0 < 𝑁)) → (𝑥 ≤ 1 ↔ (𝑁 / 1) ≤ (𝑁 / 𝑥))) |
93 | 79, 83, 89, 91, 77, 81, 92 | syl222anc 1265 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 ≤ 1 ↔ (𝑁 / 1) ≤ (𝑁 / 𝑥))) |
94 | | nnle1eq1 8992 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → (𝑥 ≤ 1 ↔ 𝑥 = 1)) |
95 | 94 | ad2antrl 490 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 ≤ 1 ↔ 𝑥 = 1)) |
96 | 31 | div1d 8785 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 / 1) = 𝑁) |
97 | 96 | breq1d 4035 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((𝑁 / 1) ≤ (𝑁 / 𝑥) ↔ 𝑁 ≤ (𝑁 / 𝑥))) |
98 | 93, 95, 97 | 3bitr3rd 219 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ≤ (𝑁 / 𝑥) ↔ 𝑥 = 1)) |
99 | 88, 98 | sylibd 149 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑥 = 1)) |
100 | 75, 99 | sylbid 150 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) → 𝑥 = 1)) |
101 | 18, 41, 62 | zndvds0 14095 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑥)) |
102 | 61, 46, 101 | syl2anc 411 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑥)) |
103 | | nnnn0 9233 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
104 | 103 | ad2antrl 490 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℕ0) |
105 | | dvdseq 11964 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑥 ∥ 𝑁 ∧ 𝑁 ∥ 𝑥)) → 𝑥 = 𝑁) |
106 | 105 | expr 375 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∥ 𝑁) → (𝑁 ∥ 𝑥 → 𝑥 = 𝑁)) |
107 | 104, 61, 44, 106 | syl21anc 1248 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ∥ 𝑥 → 𝑥 = 𝑁)) |
108 | 102, 107 | sylbid 150 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌) → 𝑥 = 𝑁)) |
109 | 100, 108 | orim12d 787 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌)) → (𝑥 = 1 ∨ 𝑥 = 𝑁))) |
110 | 73, 109 | mpd 13 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 = 1 ∨ 𝑥 = 𝑁)) |
111 | 110 | expr 375 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ 𝑥 ∈ ℕ) → (𝑥 ∥ 𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁))) |
112 | 111 | ralrimiva 2563 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
∀𝑥 ∈ ℕ
(𝑥 ∥ 𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁))) |
113 | | isprm2 12229 |
. . . 4
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℕ (𝑥 ∥ 𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁)))) |
114 | 29, 112, 113 | sylanbrc 417 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈
ℙ) |
115 | 114 | ex 115 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn → 𝑁 ∈
ℙ)) |
116 | 18 | znidom 14102 |
. 2
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ IDomn) |
117 | 115, 116 | impbid1 142 |
1
⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈
ℙ)) |