Step | Hyp | Ref
| Expression |
1 | | nnnn0 11299 |
. . . . . . 7
|
2 | | znchr.y |
. . . . . . . 8
ℤ/nℤ |
3 | | eqid 2622 |
. . . . . . . 8
|
4 | | eqid 2622 |
. . . . . . . 8
RHom RHom |
5 | 2, 3, 4 | znzrhfo 19896 |
. . . . . . 7
RHom |
6 | 1, 5 | syl 17 |
. . . . . 6
RHom |
7 | | znrrg.e |
. . . . . . . 8
RLReg |
8 | 7, 3 | rrgss 19292 |
. . . . . . 7
|
9 | 8 | sseli 3599 |
. . . . . 6
|
10 | | foelrn 6378 |
. . . . . 6
RHom
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
|
19 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
RHom |
20 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
21 | 20 | necon3ai 2819 |
. . . . . . . . . . . . . . . . . 18
|
22 | 19, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
RHom
|
23 | | gcdn0cl 15224 |
. . . . . . . . . . . . . . . . 17
|
24 | 15, 17, 22, 23 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
RHom |
25 | 24 | nncnd 11036 |
. . . . . . . . . . . . . . 15
RHom |
26 | 24 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
RHom |
27 | 14, 25, 26 | divcan2d 10803 |
. . . . . . . . . . . . . 14
RHom
|
28 | | gcddvds 15225 |
. . . . . . . . . . . . . . . . 17
|
29 | 15, 17, 28 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
RHom |
30 | 29 | simpld 475 |
. . . . . . . . . . . . . . 15
RHom |
31 | 24 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
RHom |
32 | 29 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
RHom |
33 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
RHom |
34 | | nndivdvds 14989 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 33, 24, 34 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
RHom
|
36 | 32, 35 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
RHom |
37 | 36 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
RHom |
38 | | dvdsmulc 15009 |
. . . . . . . . . . . . . . . 16
|
39 | 31, 15, 37, 38 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
RHom
|
40 | 30, 39 | mpd 15 |
. . . . . . . . . . . . . 14
RHom
|
41 | 27, 40 | eqbrtrrd 4677 |
. . . . . . . . . . . . 13
RHom |
42 | | simpr 477 |
. . . . . . . . . . . . . . 15
RHom RHom |
43 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
RHom |
44 | 43, 5 | syl 17 |
. . . . . . . . . . . . . . . . 17
RHom RHom |
45 | | fof 6115 |
. . . . . . . . . . . . . . . . 17
RHom
RHom |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . 16
RHom RHom |
47 | 46, 37 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
RHom RHom |
48 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
49 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
50 | 7, 3, 48, 49 | rrgeq0i 19289 |
. . . . . . . . . . . . . . 15
RHom RHom RHomRHom
RHom
|
51 | 42, 47, 50 | syl2anc 693 |
. . . . . . . . . . . . . 14
RHom RHomRHom RHom |
52 | 2 | zncrng 19893 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 1, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | | crngring 18558 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
RHom |
57 | 4 | zrhrhm 19860 |
. . . . . . . . . . . . . . . . . 18
RHom ℤring RingHom |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
RHom RHom ℤring RingHom |
59 | | zringbas 19824 |
. . . . . . . . . . . . . . . . . 18
ℤring |
60 | | zringmulr 19827 |
. . . . . . . . . . . . . . . . . 18
ℤring |
61 | 59, 60, 48 | rhmmul 18727 |
. . . . . . . . . . . . . . . . 17
RHom ℤring
RingHom
RHom RHomRHom |
62 | 58, 15, 37, 61 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
RHom RHom RHomRHom |
63 | 62 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
RHom RHom
RHomRHom |
64 | 15, 37 | zmulcld 11488 |
. . . . . . . . . . . . . . . 16
RHom
|
65 | 2, 4, 49 | zndvds0 19899 |
. . . . . . . . . . . . . . . 16
RHom
|
66 | 43, 64, 65 | syl2anc 693 |
. . . . . . . . . . . . . . 15
RHom RHom
|
67 | 63, 66 | bitr3d 270 |
. . . . . . . . . . . . . 14
RHom RHomRHom
|
68 | 2, 4, 49 | zndvds0 19899 |
. . . . . . . . . . . . . . 15
RHom
|
69 | 43, 37, 68 | syl2anc 693 |
. . . . . . . . . . . . . 14
RHom RHom
|
70 | 51, 67, 69 | 3imtr3d 282 |
. . . . . . . . . . . . 13
RHom
|
71 | 41, 70 | mpd 15 |
. . . . . . . . . . . 12
RHom |
72 | 14, 25, 26 | divcan1d 10802 |
. . . . . . . . . . . 12
RHom
|
73 | 36 | nncnd 11036 |
. . . . . . . . . . . . 13
RHom |
74 | 73 | mulid1d 10057 |
. . . . . . . . . . . 12
RHom |
75 | 71, 72, 74 | 3brtr4d 4685 |
. . . . . . . . . . 11
RHom
|
76 | | 1zzd 11408 |
. . . . . . . . . . . 12
RHom |
77 | 36 | nnne0d 11065 |
. . . . . . . . . . . 12
RHom |
78 | | dvdscmulr 15010 |
. . . . . . . . . . . 12
|
79 | 31, 76, 37, 77, 78 | syl112anc 1330 |
. . . . . . . . . . 11
RHom
|
80 | 75, 79 | mpbid 222 |
. . . . . . . . . 10
RHom |
81 | 15, 17 | gcdcld 15230 |
. . . . . . . . . . 11
RHom |
82 | | dvds1 15041 |
. . . . . . . . . . 11
|
83 | 81, 82 | syl 17 |
. . . . . . . . . 10
RHom |
84 | 80, 83 | mpbid 222 |
. . . . . . . . 9
RHom |
85 | | znunit.u |
. . . . . . . . . . 11
Unit |
86 | 2, 85, 4 | znunit 19912 |
. . . . . . . . . 10
RHom
|
87 | 43, 15, 86 | syl2anc 693 |
. . . . . . . . 9
RHom RHom |
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
|
99 | 55, 98 | syl 17 |
. 2
|
100 | 97, 99 | eqssd 3620 |
1
|