| Step | Hyp | Ref
| Expression |
| 1 | | 2z 12649 |
. . . . . 6
⊢ 2 ∈
ℤ |
| 2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ∈
ℤ) |
| 3 | | nnz 12634 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈
ℤ) |
| 5 | | hash2 14444 |
. . . . . . 7
⊢
(♯‘2o) = 2 |
| 6 | | isidom 20725 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
| 7 | 6 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ Domn) |
| 8 | | domnnzr 20706 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Domn → 𝑌 ∈ NzRing) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . 10
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ NzRing) |
| 10 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 11 | 10 | isnzr2 20518 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ NzRing ↔ (𝑌 ∈ Ring ∧ 2o
≼ (Base‘𝑌))) |
| 12 | 11 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑌 ∈ NzRing →
2o ≼ (Base‘𝑌)) |
| 13 | 9, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝑌 ∈ IDomn →
2o ≼ (Base‘𝑌)) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
2o ≼ (Base‘𝑌)) |
| 15 | | df2o2 8515 |
. . . . . . . . . 10
⊢
2o = {∅, {∅}} |
| 16 | | prfi 9363 |
. . . . . . . . . 10
⊢ {∅,
{∅}} ∈ Fin |
| 17 | 15, 16 | eqeltri 2837 |
. . . . . . . . 9
⊢
2o ∈ Fin |
| 18 | | fvex 6919 |
. . . . . . . . 9
⊢
(Base‘𝑌)
∈ V |
| 19 | | hashdom 14418 |
. . . . . . . . 9
⊢
((2o ∈ Fin ∧ (Base‘𝑌) ∈ V) →
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌))) |
| 20 | 17, 18, 19 | mp2an 692 |
. . . . . . . 8
⊢
((♯‘2o) ≤ (♯‘(Base‘𝑌)) ↔ 2o ≼
(Base‘𝑌)) |
| 21 | 14, 20 | sylibr 234 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
(♯‘2o) ≤ (♯‘(Base‘𝑌))) |
| 22 | 5, 21 | eqbrtrrid 5179 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ≤
(♯‘(Base‘𝑌))) |
| 23 | | zntos.y |
. . . . . . . 8
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
| 24 | 23, 10 | znhash 21577 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(♯‘(Base‘𝑌)) = 𝑁) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
(♯‘(Base‘𝑌)) = 𝑁) |
| 26 | 22, 25 | breqtrd 5169 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 2 ≤
𝑁) |
| 27 | | eluz2 12884 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
| 28 | 2, 4, 26, 27 | syl3anbrc 1344 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈
(ℤ≥‘2)) |
| 29 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈ ℂ) |
| 31 | | nncn 12274 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℂ) |
| 32 | 31 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℂ) |
| 33 | | nnne0 12300 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → 𝑥 ≠ 0) |
| 34 | 33 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ≠ 0) |
| 35 | 30, 32, 34 | divcan1d 12044 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((𝑁 / 𝑥) · 𝑥) = 𝑁) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = ((ℤRHom‘𝑌)‘𝑁)) |
| 37 | 7 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑌 ∈ Domn) |
| 38 | | domnring 20707 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ Domn → 𝑌 ∈ Ring) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑌 ∈ Ring) |
| 40 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
| 41 | 40 | zrhrhm 21522 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
| 42 | 39, 41 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (ℤRHom‘𝑌) ∈ (ℤring
RingHom 𝑌)) |
| 43 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∥ 𝑁) |
| 44 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
| 45 | 44 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℤ) |
| 46 | 3 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈ ℤ) |
| 47 | | dvdsval2 16293 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑥 ∥ 𝑁 ↔ (𝑁 / 𝑥) ∈ ℤ)) |
| 48 | 45, 34, 46, 47 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 ∥ 𝑁 ↔ (𝑁 / 𝑥) ∈ ℤ)) |
| 49 | 43, 48 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 / 𝑥) ∈ ℤ) |
| 50 | | zringbas 21464 |
. . . . . . . . . . 11
⊢ ℤ =
(Base‘ℤring) |
| 51 | | zringmulr 21468 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℤring) |
| 52 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑌) = (.r‘𝑌) |
| 53 | 50, 51, 52 | rhmmul 20486 |
. . . . . . . . . 10
⊢
(((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) ∧ (𝑁 / 𝑥) ∈ ℤ ∧ 𝑥 ∈ ℤ) →
((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥))) |
| 54 | 42, 49, 45, 53 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘((𝑁 / 𝑥) · 𝑥)) = (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥))) |
| 55 | | iddvds 16307 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁) |
| 56 | 46, 55 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∥ 𝑁) |
| 57 | | nnnn0 12533 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 58 | 57 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈
ℕ0) |
| 59 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑌) = (0g‘𝑌) |
| 60 | 23, 40, 59 | zndvds0 21569 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑁 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑁) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑁)) |
| 61 | 58, 46, 60 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘𝑁) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑁)) |
| 62 | 56, 61 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘𝑁) = (0g‘𝑌)) |
| 63 | 36, 54, 62 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g‘𝑌)) |
| 64 | 50, 10 | rhmf 20485 |
. . . . . . . . . . 11
⊢
((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) →
(ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) |
| 65 | 42, 64 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) |
| 66 | 65, 49 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) ∈ (Base‘𝑌)) |
| 67 | 65, 45 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((ℤRHom‘𝑌)‘𝑥) ∈ (Base‘𝑌)) |
| 68 | 10, 52, 59 | domneq0 20708 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Domn ∧
((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) ∈ (Base‘𝑌) ∧ ((ℤRHom‘𝑌)‘𝑥) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌)))) |
| 69 | 37, 66, 67, 68 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥))(.r‘𝑌)((ℤRHom‘𝑌)‘𝑥)) = (0g‘𝑌) ↔ (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌)))) |
| 70 | 63, 69 | mpbid 232 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌))) |
| 71 | 23, 40, 59 | zndvds0 21569 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 / 𝑥) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / 𝑥))) |
| 72 | 58, 49, 71 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / 𝑥))) |
| 73 | | nnre 12273 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 74 | 73 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑁 ∈ ℝ) |
| 75 | | nnre 12273 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℝ) |
| 76 | 75 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℝ) |
| 77 | | nngt0 12297 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
| 78 | 77 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < 𝑁) |
| 79 | | nngt0 12297 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ → 0 <
𝑥) |
| 80 | 79 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < 𝑥) |
| 81 | 74, 76, 78, 80 | divgt0d 12203 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < (𝑁 / 𝑥)) |
| 82 | | elnnz 12623 |
. . . . . . . . . . . 12
⊢ ((𝑁 / 𝑥) ∈ ℕ ↔ ((𝑁 / 𝑥) ∈ ℤ ∧ 0 < (𝑁 / 𝑥))) |
| 83 | 49, 81, 82 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 / 𝑥) ∈ ℕ) |
| 84 | | dvdsle 16347 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 𝑥) ∈ ℕ) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑁 ≤ (𝑁 / 𝑥))) |
| 85 | 46, 83, 84 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑁 ≤ (𝑁 / 𝑥))) |
| 86 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 1 ∈ ℝ) |
| 87 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 88 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 0 < 1) |
| 89 | | lediv2 12158 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 0 <
𝑥) ∧ (1 ∈ ℝ
∧ 0 < 1) ∧ (𝑁
∈ ℝ ∧ 0 < 𝑁)) → (𝑥 ≤ 1 ↔ (𝑁 / 1) ≤ (𝑁 / 𝑥))) |
| 90 | 76, 80, 86, 88, 74, 78, 89 | syl222anc 1388 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 ≤ 1 ↔ (𝑁 / 1) ≤ (𝑁 / 𝑥))) |
| 91 | | nnle1eq1 12296 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℕ → (𝑥 ≤ 1 ↔ 𝑥 = 1)) |
| 92 | 91 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 ≤ 1 ↔ 𝑥 = 1)) |
| 93 | 30 | div1d 12035 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 / 1) = 𝑁) |
| 94 | 93 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((𝑁 / 1) ≤ (𝑁 / 𝑥) ↔ 𝑁 ≤ (𝑁 / 𝑥))) |
| 95 | 90, 92, 94 | 3bitr3rd 310 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ≤ (𝑁 / 𝑥) ↔ 𝑥 = 1)) |
| 96 | 85, 95 | sylibd 239 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ∥ (𝑁 / 𝑥) → 𝑥 = 1)) |
| 97 | 72, 96 | sylbid 240 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) → 𝑥 = 1)) |
| 98 | 23, 40, 59 | zndvds0 21569 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑥)) |
| 99 | 58, 45, 98 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌) ↔ 𝑁 ∥ 𝑥)) |
| 100 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
| 101 | 100 | ad2antrl 728 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → 𝑥 ∈ ℕ0) |
| 102 | | dvdseq 16351 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑥 ∥ 𝑁 ∧ 𝑁 ∥ 𝑥)) → 𝑥 = 𝑁) |
| 103 | 102 | expr 456 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∥ 𝑁) → (𝑁 ∥ 𝑥 → 𝑥 = 𝑁)) |
| 104 | 101, 58, 43, 103 | syl21anc 838 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑁 ∥ 𝑥 → 𝑥 = 𝑁)) |
| 105 | 99, 104 | sylbid 240 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌) → 𝑥 = 𝑁)) |
| 106 | 97, 105 | orim12d 967 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → ((((ℤRHom‘𝑌)‘(𝑁 / 𝑥)) = (0g‘𝑌) ∨ ((ℤRHom‘𝑌)‘𝑥) = (0g‘𝑌)) → (𝑥 = 1 ∨ 𝑥 = 𝑁))) |
| 107 | 70, 106 | mpd 15 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ (𝑥 ∈ ℕ ∧ 𝑥 ∥ 𝑁)) → (𝑥 = 1 ∨ 𝑥 = 𝑁)) |
| 108 | 107 | expr 456 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) ∧ 𝑥 ∈ ℕ) → (𝑥 ∥ 𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁))) |
| 109 | 108 | ralrimiva 3146 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) →
∀𝑥 ∈ ℕ
(𝑥 ∥ 𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁))) |
| 110 | | isprm2 16719 |
. . . 4
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈
(ℤ≥‘2) ∧ ∀𝑥 ∈ ℕ (𝑥 ∥ 𝑁 → (𝑥 = 1 ∨ 𝑥 = 𝑁)))) |
| 111 | 28, 109, 110 | sylanbrc 583 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑌 ∈ IDomn) → 𝑁 ∈
ℙ) |
| 112 | 111 | ex 412 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn → 𝑁 ∈
ℙ)) |
| 113 | 23 | znfld 21579 |
. . 3
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field) |
| 114 | | fldidom 20771 |
. . 3
⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn) |
| 115 | 113, 114 | syl 17 |
. 2
⊢ (𝑁 ∈ ℙ → 𝑌 ∈ IDomn) |
| 116 | 112, 115 | impbid1 225 |
1
⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈
ℙ)) |