Step | Hyp | Ref
| Expression |
1 | | 1red 10055 |
. . . . 5
|
2 | | 0red 10041 |
. . . . 5
|
3 | 1, 2 | ifclda 4120 |
. . . 4
|
4 | | 1red 10055 |
. . . 4
|
5 | | fzfid 12772 |
. . . . . 6
|
6 | | dchrisum0flb.r |
. . . . . . . 8
|
7 | | rpvmasum.a |
. . . . . . . . . . 11
|
8 | 7 | nnnn0d 11351 |
. . . . . . . . . 10
|
9 | | rpvmasum.z |
. . . . . . . . . . 11
ℤ/nℤ |
10 | | eqid 2622 |
. . . . . . . . . . 11
|
11 | | rpvmasum.l |
. . . . . . . . . . 11
RHom |
12 | 9, 10, 11 | znzrhfo 19896 |
. . . . . . . . . 10
|
13 | | fof 6115 |
. . . . . . . . . 10
|
14 | 8, 12, 13 | 3syl 18 |
. . . . . . . . 9
|
15 | | dchrisum0flblem1.1 |
. . . . . . . . . 10
|
16 | | prmz 15389 |
. . . . . . . . . 10
|
17 | 15, 16 | syl 17 |
. . . . . . . . 9
|
18 | 14, 17 | ffvelrnd 6360 |
. . . . . . . 8
|
19 | 6, 18 | ffvelrnd 6360 |
. . . . . . 7
|
20 | | elfznn0 12433 |
. . . . . . 7
|
21 | | reexpcl 12877 |
. . . . . . 7
|
22 | 19, 20, 21 | syl2an 494 |
. . . . . 6
|
23 | 5, 22 | fsumrecl 14465 |
. . . . 5
|
24 | 23 | adantr 481 |
. . . 4
|
25 | | breq1 4656 |
. . . . . 6
|
26 | | breq1 4656 |
. . . . . 6
|
27 | | 1le1 10655 |
. . . . . 6
|
28 | | 0le1 10551 |
. . . . . 6
|
29 | 25, 26, 27, 28 | keephyp 4152 |
. . . . 5
|
30 | 29 | a1i 11 |
. . . 4
|
31 | | dchrisum0flblem1.2 |
. . . . . . . . . 10
|
32 | | nn0uz 11722 |
. . . . . . . . . 10
|
33 | 31, 32 | syl6eleq 2711 |
. . . . . . . . 9
|
34 | | fzn0 12355 |
. . . . . . . . 9
|
35 | 33, 34 | sylibr 224 |
. . . . . . . 8
|
36 | | hashnncl 13157 |
. . . . . . . . 9
|
37 | 5, 36 | syl 17 |
. . . . . . . 8
|
38 | 35, 37 | mpbird 247 |
. . . . . . 7
|
39 | 38 | adantr 481 |
. . . . . 6
|
40 | 39 | nnge1d 11063 |
. . . . 5
|
41 | | simpr 477 |
. . . . . . . . 9
|
42 | 41 | oveq1d 6665 |
. . . . . . . 8
|
43 | | elfzelz 12342 |
. . . . . . . . 9
|
44 | | 1exp 12889 |
. . . . . . . . 9
|
45 | 43, 44 | syl 17 |
. . . . . . . 8
|
46 | 42, 45 | sylan9eq 2676 |
. . . . . . 7
|
47 | 46 | sumeq2dv 14433 |
. . . . . 6
|
48 | | fzfid 12772 |
. . . . . . 7
|
49 | | ax-1cn 9994 |
. . . . . . 7
|
50 | | fsumconst 14522 |
. . . . . . 7
|
51 | 48, 49, 50 | sylancl 694 |
. . . . . 6
|
52 | 39 | nncnd 11036 |
. . . . . . 7
|
53 | 52 | mulid1d 10057 |
. . . . . 6
|
54 | 47, 51, 53 | 3eqtrd 2660 |
. . . . 5
|
55 | 40, 54 | breqtrrd 4681 |
. . . 4
|
56 | 3, 4, 24, 30, 55 | letrd 10194 |
. . 3
|
57 | | oveq1 6657 |
. . . . . . 7
|
58 | 57 | breq1d 4663 |
. . . . . 6
|
59 | | oveq1 6657 |
. . . . . . 7
|
60 | 59 | breq1d 4663 |
. . . . . 6
|
61 | | 1re 10039 |
. . . . . . . . . 10
|
62 | 19 | adantr 481 |
. . . . . . . . . 10
|
63 | | resubcl 10345 |
. . . . . . . . . 10
|
64 | 61, 62, 63 | sylancr 695 |
. . . . . . . . 9
|
65 | 64 | adantr 481 |
. . . . . . . 8
|
66 | 65 | leidd 10594 |
. . . . . . 7
|
67 | 64 | recnd 10068 |
. . . . . . . . 9
|
68 | 67 | adantr 481 |
. . . . . . . 8
|
69 | 68 | mulid2d 10058 |
. . . . . . 7
|
70 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
|
71 | 31, 70 | syl 17 |
. . . . . . . . . . . 12
|
72 | 71 | ad3antrrr 766 |
. . . . . . . . . . 11
|
73 | 72 | 0expd 13024 |
. . . . . . . . . 10
|
74 | | simpr 477 |
. . . . . . . . . . 11
|
75 | 74 | oveq1d 6665 |
. . . . . . . . . 10
|
76 | 73, 75, 74 | 3eqtr4d 2666 |
. . . . . . . . 9
|
77 | | neg1cn 11124 |
. . . . . . . . . . . . 13
|
78 | 31 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
79 | | expp1 12867 |
. . . . . . . . . . . . 13
|
80 | 77, 78, 79 | sylancr 695 |
. . . . . . . . . . . 12
|
81 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
82 | 15, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
83 | 82, 31 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . . . . 21
|
84 | 83 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | 84 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
86 | 85 | sqsqrtd 14178 |
. . . . . . . . . . . . . . . . . 18
|
87 | 86 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
88 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
89 | | nnq 11801 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
91 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . 19
|
92 | 91 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
93 | | 2z 11409 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
95 | | pcexp 15564 |
. . . . . . . . . . . . . . . . . 18
|
96 | 88, 90, 92, 94, 95 | syl121anc 1331 |
. . . . . . . . . . . . . . . . 17
|
97 | 78 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . 18
|
98 | | pcid 15577 |
. . . . . . . . . . . . . . . . . 18
|
99 | 88, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
100 | 87, 96, 99 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . 16
|
101 | 100 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
102 | 77 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
103 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
104 | 88, 103 | pccld 15555 |
. . . . . . . . . . . . . . . 16
|
105 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
107 | 102, 104,
106 | expmuld 13011 |
. . . . . . . . . . . . . . 15
|
108 | | neg1sqe1 12959 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
110 | 104 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
|
111 | | 1exp 12889 |
. . . . . . . . . . . . . . . . 17
|
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
|
113 | 109, 112 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
|
114 | 101, 107,
113 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
116 | 77 | mulid2i 10043 |
. . . . . . . . . . . . 13
|
117 | 115, 116 | syl6eq 2672 |
. . . . . . . . . . . 12
|
118 | 80, 117 | eqtrd 2656 |
. . . . . . . . . . 11
|
119 | 118 | adantr 481 |
. . . . . . . . . 10
|
120 | 19 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
121 | 120 | adantr 481 |
. . . . . . . . . . . . . 14
|
122 | 121 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
123 | 122 | negnegd 10383 |
. . . . . . . . . . . 12
|
124 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
125 | 124 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
126 | | rpvmasum2.g |
. . . . . . . . . . . . . . . . . . 19
DChr |
127 | | rpvmasum2.d |
. . . . . . . . . . . . . . . . . . 19
|
128 | | dchrisum0f.x |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 128 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
|
130 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
Unit Unit |
131 | 126, 9, 127, 10, 130, 128, 18 | dchrn0 24975 |
. . . . . . . . . . . . . . . . . . . . 21
Unit |
132 | 131 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
Unit |
133 | 132 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
Unit |
134 | 126, 127,
129, 9, 130, 133 | dchrabs 24985 |
. . . . . . . . . . . . . . . . . 18
|
135 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
|
136 | 134, 135 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . 17
|
137 | 136 | necon3ad 2807 |
. . . . . . . . . . . . . . . 16
|
138 | 125, 137 | mpd 15 |
. . . . . . . . . . . . . . 15
|
139 | 62 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
140 | 139 | absord 14154 |
. . . . . . . . . . . . . . . 16
|
141 | 140 | ord 392 |
. . . . . . . . . . . . . . 15
|
142 | 138, 141 | mpd 15 |
. . . . . . . . . . . . . 14
|
143 | 142, 134 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
144 | 143 | negeqd 10275 |
. . . . . . . . . . . 12
|
145 | 123, 144 | eqtr3d 2658 |
. . . . . . . . . . 11
|
146 | 145 | oveq1d 6665 |
. . . . . . . . . 10
|
147 | 119, 146,
145 | 3eqtr4d 2666 |
. . . . . . . . 9
|
148 | 76, 147 | pm2.61dane 2881 |
. . . . . . . 8
|
149 | 148 | oveq2d 6666 |
. . . . . . 7
|
150 | 66, 69, 149 | 3brtr4d 4685 |
. . . . . 6
|
151 | 67 | mul02d 10234 |
. . . . . . . 8
|
152 | | peano2nn0 11333 |
. . . . . . . . . . . . 13
|
153 | 31, 152 | syl 17 |
. . . . . . . . . . . 12
|
154 | 19, 153 | reexpcld 13025 |
. . . . . . . . . . 11
|
155 | 154 | adantr 481 |
. . . . . . . . . 10
|
156 | 155 | recnd 10068 |
. . . . . . . . . . 11
|
157 | 156 | abscld 14175 |
. . . . . . . . . 10
|
158 | | 1red 10055 |
. . . . . . . . . 10
|
159 | 155 | leabsd 14153 |
. . . . . . . . . 10
|
160 | 153 | adantr 481 |
. . . . . . . . . . . 12
|
161 | 121, 160 | absexpd 14191 |
. . . . . . . . . . 11
|
162 | 121 | abscld 14175 |
. . . . . . . . . . . 12
|
163 | 121 | absge0d 14183 |
. . . . . . . . . . . 12
|
164 | 126, 127,
9, 10, 128, 18 | dchrabs2 24987 |
. . . . . . . . . . . . 13
|
165 | 164 | adantr 481 |
. . . . . . . . . . . 12
|
166 | | exple1 12920 |
. . . . . . . . . . . 12
|
167 | 162, 163,
165, 160, 166 | syl31anc 1329 |
. . . . . . . . . . 11
|
168 | 161, 167 | eqbrtrd 4675 |
. . . . . . . . . 10
|
169 | 155, 157,
158, 159, 168 | letrd 10194 |
. . . . . . . . 9
|
170 | | subge0 10541 |
. . . . . . . . . 10
|
171 | 61, 155, 170 | sylancr 695 |
. . . . . . . . 9
|
172 | 169, 171 | mpbird 247 |
. . . . . . . 8
|
173 | 151, 172 | eqbrtrd 4675 |
. . . . . . 7
|
174 | 173 | adantr 481 |
. . . . . 6
|
175 | 58, 60, 150, 174 | ifbothda 4123 |
. . . . 5
|
176 | | 0re 10040 |
. . . . . . . 8
|
177 | 61, 176 | keepel 4155 |
. . . . . . 7
|
178 | 177 | a1i 11 |
. . . . . 6
|
179 | | resubcl 10345 |
. . . . . . 7
|
180 | 61, 155, 179 | sylancr 695 |
. . . . . 6
|
181 | 124 | necomd 2849 |
. . . . . . . 8
|
182 | 62 | leabsd 14153 |
. . . . . . . . . 10
|
183 | 62, 162, 158, 182, 165 | letrd 10194 |
. . . . . . . . 9
|
184 | 62, 158, 183 | leltned 10190 |
. . . . . . . 8
|
185 | 181, 184 | mpbird 247 |
. . . . . . 7
|
186 | | posdif 10521 |
. . . . . . . 8
|
187 | 62, 61, 186 | sylancl 694 |
. . . . . . 7
|
188 | 185, 187 | mpbid 222 |
. . . . . 6
|
189 | | lemuldiv 10903 |
. . . . . 6
|
190 | 178, 180,
64, 188, 189 | syl112anc 1330 |
. . . . 5
|
191 | 175, 190 | mpbid 222 |
. . . 4
|
192 | 31 | nn0zd 11480 |
. . . . . . . 8
|
193 | | fzval3 12536 |
. . . . . . . 8
..^ |
194 | 192, 193 | syl 17 |
. . . . . . 7
..^ |
195 | 194 | adantr 481 |
. . . . . 6
..^ |
196 | 195 | sumeq1d 14431 |
. . . . 5
..^ |
197 | | 0nn0 11307 |
. . . . . . 7
|
198 | 197 | a1i 11 |
. . . . . 6
|
199 | 153, 32 | syl6eleq 2711 |
. . . . . . 7
|
200 | 199 | adantr 481 |
. . . . . 6
|
201 | 121, 124,
198, 200 | geoserg 14598 |
. . . . 5
..^ |
202 | 121 | exp0d 13002 |
. . . . . . 7
|
203 | 202 | oveq1d 6665 |
. . . . . 6
|
204 | 203 | oveq1d 6665 |
. . . . 5
|
205 | 196, 201,
204 | 3eqtrd 2660 |
. . . 4
|
206 | 191, 205 | breqtrrd 4681 |
. . 3
|
207 | 56, 206 | pm2.61dane 2881 |
. 2
|
208 | | rpvmasum2.1 |
. . . . 5
|
209 | | dchrisum0f.f |
. . . . 5
|
210 | 9, 11, 7, 126, 127, 208, 209 | dchrisum0fval 25194 |
. . . 4
|
211 | 83, 210 | syl 17 |
. . 3
|
212 | | fveq2 6191 |
. . . . 5
|
213 | 212 | fveq2d 6195 |
. . . 4
|
214 | | eqid 2622 |
. . . . . 6
|
215 | 214 | dvdsppwf1o 24912 |
. . . . 5
|
216 | 15, 31, 215 | syl2anc 693 |
. . . 4
|
217 | | oveq2 6658 |
. . . . . 6
|
218 | | ovex 6678 |
. . . . . 6
|
219 | 217, 214,
218 | fvmpt3i 6287 |
. . . . 5
|
220 | 219 | adantl 482 |
. . . 4
|
221 | 6 | adantr 481 |
. . . . . 6
|
222 | | elrabi 3359 |
. . . . . . . 8
|
223 | 222 | nnzd 11481 |
. . . . . . 7
|
224 | | ffvelrn 6357 |
. . . . . . 7
|
225 | 14, 223, 224 | syl2an 494 |
. . . . . 6
|
226 | 221, 225 | ffvelrnd 6360 |
. . . . 5
|
227 | 226 | recnd 10068 |
. . . 4
|
228 | 213, 5, 216, 220, 227 | fsumf1o 14454 |
. . 3
|
229 | | zsubrg 19799 |
. . . . . . . . . . 11
SubRingℂfld |
230 | | eqid 2622 |
. . . . . . . . . . . 12
mulGrpℂfld mulGrpℂfld |
231 | 230 | subrgsubm 18793 |
. . . . . . . . . . 11
SubRingℂfld
SubMndmulGrpℂfld |
232 | 229, 231 | mp1i 13 |
. . . . . . . . . 10
SubMndmulGrpℂfld |
233 | 20 | adantl 482 |
. . . . . . . . . 10
|
234 | 17 | adantr 481 |
. . . . . . . . . 10
|
235 | | eqid 2622 |
. . . . . . . . . . 11
.gmulGrpℂfld .gmulGrpℂfld |
236 | | zringmpg 19840 |
. . . . . . . . . . . 12
mulGrpℂfld ↾s
mulGrpℤring |
237 | 236 | eqcomi 2631 |
. . . . . . . . . . 11
mulGrpℤring mulGrpℂfld ↾s |
238 | | eqid 2622 |
. . . . . . . . . . 11
.gmulGrpℤring .gmulGrpℤring |
239 | 235, 237,
238 | submmulg 17586 |
. . . . . . . . . 10
SubMndmulGrpℂfld .gmulGrpℂfld .gmulGrpℤring |
240 | 232, 233,
234, 239 | syl3anc 1326 |
. . . . . . . . 9
.gmulGrpℂfld .gmulGrpℤring |
241 | 82 | nncnd 11036 |
. . . . . . . . . 10
|
242 | | cnfldexp 19779 |
. . . . . . . . . 10
.gmulGrpℂfld |
243 | 241, 20, 242 | syl2an 494 |
. . . . . . . . 9
.gmulGrpℂfld |
244 | 240, 243 | eqtr3d 2658 |
. . . . . . . 8
.gmulGrpℤring |
245 | 244 | fveq2d 6195 |
. . . . . . 7
.gmulGrpℤring |
246 | 9 | zncrng 19893 |
. . . . . . . . . . 11
|
247 | | crngring 18558 |
. . . . . . . . . . 11
|
248 | 8, 246, 247 | 3syl 18 |
. . . . . . . . . 10
|
249 | 11 | zrhrhm 19860 |
. . . . . . . . . 10
ℤring RingHom |
250 | | eqid 2622 |
. . . . . . . . . . 11
mulGrpℤring mulGrpℤring |
251 | | eqid 2622 |
. . . . . . . . . . 11
mulGrp mulGrp |
252 | 250, 251 | rhmmhm 18722 |
. . . . . . . . . 10
ℤring RingHom mulGrpℤring
MndHom mulGrp |
253 | 248, 249,
252 | 3syl 18 |
. . . . . . . . 9
mulGrpℤring MndHom mulGrp |
254 | 253 | adantr 481 |
. . . . . . . 8
mulGrpℤring
MndHom mulGrp |
255 | | zringbas 19824 |
. . . . . . . . . 10
ℤring |
256 | 250, 255 | mgpbas 18495 |
. . . . . . . . 9
mulGrpℤring |
257 | | eqid 2622 |
. . . . . . . . 9
.gmulGrp .gmulGrp |
258 | 256, 238,
257 | mhmmulg 17583 |
. . . . . . . 8
mulGrpℤring MndHom mulGrp
.gmulGrpℤring .gmulGrp |
259 | 254, 233,
234, 258 | syl3anc 1326 |
. . . . . . 7
.gmulGrpℤring .gmulGrp |
260 | 245, 259 | eqtr3d 2658 |
. . . . . 6
.gmulGrp |
261 | 260 | fveq2d 6195 |
. . . . 5
.gmulGrp |
262 | 126, 9, 127 | dchrmhm 24966 |
. . . . . . . 8
mulGrp MndHom mulGrpℂfld |
263 | 262, 128 | sseldi 3601 |
. . . . . . 7
mulGrp MndHom mulGrpℂfld |
264 | 263 | adantr 481 |
. . . . . 6
mulGrp MndHom mulGrpℂfld |
265 | 18 | adantr 481 |
. . . . . 6
|
266 | 251, 10 | mgpbas 18495 |
. . . . . . 7
mulGrp |
267 | 266, 257,
235 | mhmmulg 17583 |
. . . . . 6
mulGrp MndHom mulGrpℂfld
.gmulGrp .gmulGrpℂfld |
268 | 264, 233,
265, 267 | syl3anc 1326 |
. . . . 5
.gmulGrp .gmulGrpℂfld |
269 | | cnfldexp 19779 |
. . . . . 6
.gmulGrpℂfld |
270 | 120, 20, 269 | syl2an 494 |
. . . . 5
.gmulGrpℂfld |
271 | 261, 268,
270 | 3eqtrd 2660 |
. . . 4
|
272 | 271 | sumeq2dv 14433 |
. . 3
|
273 | 211, 228,
272 | 3eqtrd 2660 |
. 2
|
274 | 207, 273 | breqtrrd 4681 |
1
|