Step | Hyp | Ref
| Expression |
1 | | nnnn0 11299 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | | znchr.y |
. . . . . . . 8
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
3 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
4 | | eqid 2622 |
. . . . . . . 8
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
5 | 2, 3, 4 | znzrhfo 19896 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) |
6 | 1, 5 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) |
7 | | znrrg.e |
. . . . . . . 8
⊢ 𝐸 = (RLReg‘𝑌) |
8 | 7, 3 | rrgss 19292 |
. . . . . . 7
⊢ 𝐸 ⊆ (Base‘𝑌) |
9 | 8 | sseli 3599 |
. . . . . 6
⊢ (𝑥 ∈ 𝐸 → 𝑥 ∈ (Base‘𝑌)) |
10 | | foelrn 6378 |
. . . . . 6
⊢
(((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ 𝑥 ∈ (Base‘𝑌)) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛)) |
11 | 6, 9, 10 | syl2an 494 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐸) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛)) |
12 | 11 | ex 450 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝐸 → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛))) |
13 | | nncn 11028 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
14 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℂ) |
15 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑛 ∈ ℤ) |
16 | | nnz 11399 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
17 | 16 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℤ) |
18 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
19 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ≠ 0) |
20 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
21 | 20 | necon3ai 2819 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ≠ 0 → ¬ (𝑛 = 0 ∧ 𝑁 = 0)) |
22 | 19, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ¬ (𝑛 = 0 ∧ 𝑁 = 0)) |
23 | | gcdn0cl 15224 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑛 = 0 ∧ 𝑁 = 0)) → (𝑛 gcd 𝑁) ∈ ℕ) |
24 | 15, 17, 22, 23 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℕ) |
25 | 24 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℂ) |
26 | 24 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ≠ 0) |
27 | 14, 25, 26 | divcan2d 10803 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) = 𝑁) |
28 | | gcddvds 15225 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁)) |
29 | 15, 17, 28 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁)) |
30 | 29 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑛) |
31 | 24 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℤ) |
32 | 29 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑁) |
33 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℕ) |
34 | | nndivdvds 14989 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 gcd 𝑁) ∈ ℕ) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ)) |
35 | 33, 24, 34 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ)) |
36 | 32, 35 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ) |
37 | 36 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) |
38 | | dvdsmulc 15009 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 gcd 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) |
39 | 31, 15, 37, 38 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) |
40 | 30, 39 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) |
41 | 27, 40 | eqbrtrrd 4677 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) |
42 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) |
43 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈
ℕ0) |
44 | 43, 5 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) |
45 | | fof 6115 |
. . . . . . . . . . . . . . . . 17
⊢
((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) |
47 | 46, 37 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌)) |
48 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑌) = (.r‘𝑌) |
49 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑌) = (0g‘𝑌) |
50 | 7, 3, 48, 49 | rrgeq0i 19289 |
. . . . . . . . . . . . . . 15
⊢
((((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 ∧ ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) →
((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌))) |
51 | 42, 47, 50 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) →
((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌))) |
52 | 2 | zncrng 19893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) |
53 | 1, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ CRing) |
54 | | crngring 18558 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ Ring) |
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑌 ∈ Ring) |
57 | 4 | zrhrhm 19860 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌) ∈ (ℤring
RingHom 𝑌)) |
59 | | zringbas 19824 |
. . . . . . . . . . . . . . . . . 18
⊢ ℤ =
(Base‘ℤring) |
60 | | zringmulr 19827 |
. . . . . . . . . . . . . . . . . 18
⊢ ·
= (.r‘ℤring) |
61 | 59, 60, 48 | rhmmul 18727 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) →
((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))))) |
62 | 58, 15, 37, 61 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))))) |
63 | 62 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔
(((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌))) |
64 | 15, 37 | zmulcld 11488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ) |
65 | 2, 4, 49 | zndvds0 19899 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) |
66 | 43, 64, 65 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) |
67 | 63, 66 | bitr3d 270 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) |
68 | 2, 4, 49 | zndvds0 19899 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))) |
69 | 43, 37, 68 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))) |
70 | 51, 67, 69 | 3imtr3d 282 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))) |
71 | 41, 70 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))) |
72 | 14, 25, 26 | divcan1d 10802 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) = 𝑁) |
73 | 36 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℂ) |
74 | 73 | mulid1d 10057 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · 1) = (𝑁 / (𝑛 gcd 𝑁))) |
75 | 71, 72, 74 | 3brtr4d 4685 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1)) |
76 | | 1zzd 11408 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 1 ∈ ℤ) |
77 | 36 | nnne0d 11065 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ≠ 0) |
78 | | dvdscmulr 15010 |
. . . . . . . . . . . 12
⊢ (((𝑛 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ
∧ ((𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ≠ 0)) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1)) |
79 | 31, 76, 37, 77, 78 | syl112anc 1330 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1)) |
80 | 75, 79 | mpbid 222 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 1) |
81 | 15, 17 | gcdcld 15230 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈
ℕ0) |
82 | | dvds1 15041 |
. . . . . . . . . . 11
⊢ ((𝑛 gcd 𝑁) ∈ ℕ0 → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1)) |
83 | 81, 82 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1)) |
84 | 80, 83 | mpbid 222 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) = 1) |
85 | | znunit.u |
. . . . . . . . . . 11
⊢ 𝑈 = (Unit‘𝑌) |
86 | 2, 85, 4 | znunit 19912 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1)) |
87 | 43, 15, 86 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1)) |
88 | 84, 87 | mpbird 247 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈) |
89 | 88 | ex 450 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) →
(((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)) |
90 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝐸 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸)) |
91 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝑈 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)) |
92 | 90, 91 | imbi12d 334 |
. . . . . . 7
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → ((𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈) ↔ (((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈))) |
93 | 89, 92 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) → (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈))) |
94 | 93 | rexlimdva 3031 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(∃𝑛 ∈ ℤ
𝑥 =
((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈))) |
95 | 94 | com23 86 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝐸 → (∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛) → 𝑥 ∈ 𝑈))) |
96 | 12, 95 | mpdd 43 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈)) |
97 | 96 | ssrdv 3609 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐸 ⊆ 𝑈) |
98 | 7, 85 | unitrrg 19293 |
. . 3
⊢ (𝑌 ∈ Ring → 𝑈 ⊆ 𝐸) |
99 | 55, 98 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ → 𝑈 ⊆ 𝐸) |
100 | 97, 99 | eqssd 3620 |
1
⊢ (𝑁 ∈ ℕ → 𝐸 = 𝑈) |