Step | Hyp | Ref
| Expression |
1 | | 1red 9676 |
. . . . 5
                       |
2 | | 0red 9662 |
. . . . 5
                       |
3 | 1, 2 | ifclda 3904 |
. . . 4
 
        
               |
4 | | 1red 9676 |
. . . 4
 
        
  |
5 | | fzfid 12224 |
. . . . . 6
       |
6 | | dchrisum0flb.r |
. . . . . . . 8
           |
7 | | rpvmasum.a |
. . . . . . . . . . 11
   |
8 | 7 | nnnn0d 10949 |
. . . . . . . . . 10
   |
9 | | rpvmasum.z |
. . . . . . . . . . 11
ℤ/nℤ   |
10 | | eqid 2471 |
. . . . . . . . . . 11
         |
11 | | rpvmasum.l |
. . . . . . . . . . 11
 RHom   |
12 | 9, 10, 11 | znzrhfo 19195 |
. . . . . . . . . 10

          |
13 | | fof 5806 |
. . . . . . . . . 10
                   |
14 | 8, 12, 13 | 3syl 18 |
. . . . . . . . 9
           |
15 | | dchrisum0flblem1.1 |
. . . . . . . . . 10
   |
16 | | prmz 14705 |
. . . . . . . . . 10

  |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
   |
18 | 14, 17 | ffvelrnd 6038 |
. . . . . . . 8
           |
19 | 6, 18 | ffvelrnd 6038 |
. . . . . . 7
           |
20 | | elfznn0 11913 |
. . . . . . 7
       |
21 | | reexpcl 12327 |
. . . . . . 7
         
               |
22 | 19, 20, 21 | syl2an 485 |
. . . . . 6
 
                   |
23 | 5, 22 | fsumrecl 13877 |
. . . . 5
                     |
24 | 23 | adantr 472 |
. . . 4
 
        
                    |
25 | | breq1 4398 |
. . . . . 6
                               |
26 | | breq1 4398 |
. . . . . 6
                               |
27 | | 1le1 10262 |
. . . . . 6
 |
28 | | 0le1 10158 |
. . . . . 6
 |
29 | 25, 26, 27, 28 | keephyp 3936 |
. . . . 5
              |
30 | 29 | a1i 11 |
. . . 4
 
        
               |
31 | | dchrisum0flblem1.2 |
. . . . . . . . . 10
   |
32 | | nn0uz 11217 |
. . . . . . . . . 10
     |
33 | 31, 32 | syl6eleq 2559 |
. . . . . . . . 9
       |
34 | | fzn0 11839 |
. . . . . . . . 9
    
      |
35 | 33, 34 | sylibr 217 |
. . . . . . . 8
       |
36 | | hashnncl 12585 |
. . . . . . . . 9
             
       |
37 | 5, 36 | syl 17 |
. . . . . . . 8
         
       |
38 | 35, 37 | mpbird 240 |
. . . . . . 7
           |
39 | 38 | adantr 472 |
. . . . . 6
 
        
          |
40 | 39 | nnge1d 10674 |
. . . . 5
 
        
          |
41 | | simpr 468 |
. . . . . . . . 9
 
        
          |
42 | 41 | oveq1d 6323 |
. . . . . . . 8
 
        
                  |
43 | | elfzelz 11826 |
. . . . . . . . 9
       |
44 | | 1exp 12339 |
. . . . . . . . 9
       |
45 | 43, 44 | syl 17 |
. . . . . . . 8
           |
46 | 42, 45 | sylan9eq 2525 |
. . . . . . 7
                               |
47 | 46 | sumeq2dv 13846 |
. . . . . 6
 
        
                  
       |
48 | | fzfid 12224 |
. . . . . . 7
 
        
      |
49 | | ax-1cn 9615 |
. . . . . . 7
 |
50 | | fsumconst 13928 |
. . . . . . 7
     
                   |
51 | 48, 49, 50 | sylancl 675 |
. . . . . 6
 
        
                  |
52 | 39 | nncnd 10647 |
. . . . . . 7
 
        
          |
53 | 52 | mulid1d 9678 |
. . . . . 6
 
        
                    |
54 | 47, 51, 53 | 3eqtrd 2509 |
. . . . 5
 
        
                            |
55 | 40, 54 | breqtrrd 4422 |
. . . 4
 
        
                    |
56 | 3, 4, 24, 30, 55 | letrd 9809 |
. . 3
 
        
                                 |
57 | | oveq1 6315 |
. . . . . . 7
                                                     |
58 | 57 | breq1d 4405 |
. . . . . 6
                          
               
                        
                   |
59 | | oveq1 6315 |
. . . . . . 7
                                                     |
60 | 59 | breq1d 4405 |
. . . . . 6
                          
               
                        
                   |
61 | | 1re 9660 |
. . . . . . . . . 10
 |
62 | 19 | adantr 472 |
. . . . . . . . . 10
 
        
          |
63 | | resubcl 9958 |
. . . . . . . . . 10
                       |
64 | 61, 62, 63 | sylancr 676 |
. . . . . . . . 9
 
        
            |
65 | 64 | adantr 472 |
. . . . . . . 8
                                 |
66 | 65 | leidd 10201 |
. . . . . . 7
                                           |
67 | 64 | recnd 9687 |
. . . . . . . . 9
 
        
            |
68 | 67 | adantr 472 |
. . . . . . . 8
                                 |
69 | 68 | mulid2d 9679 |
. . . . . . 7
                                             |
70 | | nn0p1nn 10933 |
. . . . . . . . . . . . 13

    |
71 | 31, 70 | syl 17 |
. . . . . . . . . . . 12
     |
72 | 71 | ad3antrrr 744 |
. . . . . . . . . . 11
                                   |
73 | 72 | 0expd 12470 |
. . . . . . . . . 10
                                  
    |
74 | | simpr 468 |
. . . . . . . . . . 11
                                         |
75 | 74 | oveq1d 6323 |
. . . . . . . . . 10
                                                     |
76 | 73, 75, 74 | 3eqtr4d 2515 |
. . . . . . . . 9
                                                       |
77 | | neg1cn 10735 |
. . . . . . . . . . . . 13
  |
78 | 31 | ad2antrr 740 |
. . . . . . . . . . . . 13
                       |
79 | | expp1 12317 |
. . . . . . . . . . . . 13
                     |
80 | 77, 78, 79 | sylancr 676 |
. . . . . . . . . . . 12
                                      |
81 | | prmnn 14704 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
82 | 15, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
83 | 82, 31 | nnexpcld 12475 |
. . . . . . . . . . . . . . . . . . . . 21
       |
84 | 83 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . . 20
       |
85 | 84 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . 19
                           |
86 | 85 | sqsqrtd 13578 |
. . . . . . . . . . . . . . . . . 18
                                       |
87 | 86 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                                   
       |
88 | 15 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
                       |
89 | | nnq 11300 |
. . . . . . . . . . . . . . . . . . 19
                   |
90 | 89 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
                               |
91 | | nnne0 10664 |
. . . . . . . . . . . . . . . . . . 19
                   |
92 | 91 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
                               |
93 | | 2z 10993 |
. . . . . . . . . . . . . . . . . . 19
 |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                       |
95 | | pcexp 14888 |
. . . . . . . . . . . . . . . . . 18
                                                 |
96 | 88, 90, 92, 94, 95 | syl121anc 1297 |
. . . . . . . . . . . . . . . . 17
                                                 |
97 | 78 | nn0zd 11061 |
. . . . . . . . . . . . . . . . . 18
                       |
98 | | pcid 14901 |
. . . . . . . . . . . . . . . . . 18
           |
99 | 88, 97, 98 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
                             |
100 | 87, 96, 99 | 3eqtr3rd 2514 |
. . . . . . . . . . . . . . . 16
                                   |
101 | 100 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                                             |
102 | 77 | a1i 11 |
. . . . . . . . . . . . . . . 16
                        |
103 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
                               |
104 | 88, 103 | pccld 14879 |
. . . . . . . . . . . . . . . 16
                                 |
105 | | 2nn0 10910 |
. . . . . . . . . . . . . . . . 17
 |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . 16
                       |
107 | 102, 104,
106 | expmuld 12457 |
. . . . . . . . . . . . . . 15
                                                           |
108 | | neg1sqe1 12408 |
. . . . . . . . . . . . . . . . 17
      |
109 | 108 | oveq1i 6318 |
. . . . . . . . . . . . . . . 16
                                  |
110 | 104 | nn0zd 11061 |
. . . . . . . . . . . . . . . . 17
                                 |
111 | | 1exp 12339 |
. . . . . . . . . . . . . . . . 17
 
        
                |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
                                     |
113 | 109, 112 | syl5eq 2517 |
. . . . . . . . . . . . . . 15
                                          |
114 | 101, 107,
113 | 3eqtrd 2509 |
. . . . . . . . . . . . . 14
                            |
115 | 114 | oveq1d 6323 |
. . . . . . . . . . . . 13
                                  |
116 | 77 | mulid2i 9664 |
. . . . . . . . . . . . 13
     |
117 | 115, 116 | syl6eq 2521 |
. . . . . . . . . . . 12
                                |
118 | 80, 117 | eqtrd 2505 |
. . . . . . . . . . 11
                               |
119 | 118 | adantr 472 |
. . . . . . . . . 10
                                   
     |
120 | 19 | recnd 9687 |
. . . . . . . . . . . . . . 15
           |
121 | 120 | adantr 472 |
. . . . . . . . . . . . . 14
 
        
          |
122 | 121 | ad2antrr 740 |
. . . . . . . . . . . . 13
                                         |
123 | 122 | negnegd 9996 |
. . . . . . . . . . . 12
                                                   |
124 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
 
        
          |
125 | 124 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
                                         |
126 | | rpvmasum2.g |
. . . . . . . . . . . . . . . . . . 19
DChr   |
127 | | rpvmasum2.d |
. . . . . . . . . . . . . . . . . . 19
     |
128 | | dchrisum0f.x |
. . . . . . . . . . . . . . . . . . . 20
   |
129 | 128 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . 19
                              
  |
130 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
Unit  Unit   |
131 | 126, 9, 127, 10, 130, 128, 18 | dchrn0 24257 |
. . . . . . . . . . . . . . . . . . . . 21
              Unit     |
132 | 131 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
                                  Unit     |
133 | 132 | biimpa 492 |
. . . . . . . . . . . . . . . . . . 19
                                   Unit    |
134 | 126, 127,
129, 9, 130, 133 | dchrabs 24267 |
. . . . . . . . . . . . . . . . . 18
                                             |
135 | | eqeq1 2475 |
. . . . . . . . . . . . . . . . . 18
                    
                        |
136 | 134, 135 | syl5ibcom 228 |
. . . . . . . . . . . . . . . . 17
                                                   
           |
137 | 136 | necon3ad 2656 |
. . . . . . . . . . . . . . . 16
                                                               |
138 | 125, 137 | mpd 15 |
. . . . . . . . . . . . . . 15
                                                     |
139 | 62 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
                                         |
140 | 139 | absord 13554 |
. . . . . . . . . . . . . . . 16
                                                                            |
141 | 140 | ord 384 |
. . . . . . . . . . . . . . 15
                                                                            |
142 | 138, 141 | mpd 15 |
. . . . . . . . . . . . . 14
                                                      |
143 | 142, 134 | eqtr3d 2507 |
. . . . . . . . . . . . 13
                                          |
144 | 143 | negeqd 9889 |
. . . . . . . . . . . 12
                                            |
145 | 123, 144 | eqtr3d 2507 |
. . . . . . . . . . 11
                                          |
146 | 145 | oveq1d 6323 |
. . . . . . . . . 10
                                                      |
147 | 119, 146,
145 | 3eqtr4d 2515 |
. . . . . . . . 9
                                                       |
148 | 76, 147 | pm2.61dane 2730 |
. . . . . . . 8
                                             |
149 | 148 | oveq2d 6324 |
. . . . . . 7
                                                 |
150 | 66, 69, 149 | 3brtr4d 4426 |
. . . . . 6
                                                   |
151 | 67 | mul02d 9849 |
. . . . . . . 8
 
        
              |
152 | | peano2nn0 10934 |
. . . . . . . . . . . . 13

    |
153 | 31, 152 | syl 17 |
. . . . . . . . . . . 12
     |
154 | 19, 153 | reexpcld 12471 |
. . . . . . . . . . 11
                 |
155 | 154 | adantr 472 |
. . . . . . . . . 10
 
        
                |
156 | 155 | recnd 9687 |
. . . . . . . . . . 11
 
        
                |
157 | 156 | abscld 13575 |
. . . . . . . . . 10
 
        
                    |
158 | | 1red 9676 |
. . . . . . . . . 10
 
        
  |
159 | 155 | leabsd 13553 |
. . . . . . . . . 10
 
        
                                  |
160 | 153 | adantr 472 |
. . . . . . . . . . . 12
 
        
    |
161 | 121, 160 | absexpd 13591 |
. . . . . . . . . . 11
 
        
                                      |
162 | 121 | abscld 13575 |
. . . . . . . . . . . 12
 
        
              |
163 | 121 | absge0d 13583 |
. . . . . . . . . . . 12
 
        
              |
164 | 126, 127,
9, 10, 128, 18 | dchrabs2 24269 |
. . . . . . . . . . . . 13
               |
165 | 164 | adantr 472 |
. . . . . . . . . . . 12
 
        
              |
166 | | exple1 12370 |
. . . . . . . . . . . 12
                                        
                      |
167 | 162, 163,
165, 160, 166 | syl31anc 1295 |
. . . . . . . . . . 11
 
        
               
 
  |
168 | 161, 167 | eqbrtrd 4416 |
. . . . . . . . . 10
 
        
                 
  |
169 | 155, 157,
158, 159, 168 | letrd 9809 |
. . . . . . . . 9
 
        
                |
170 | | subge0 10148 |
. . . . . . . . . 10
                                                   |
171 | 61, 155, 170 | sylancr 676 |
. . . . . . . . 9
 
        
                                  |
172 | 169, 171 | mpbird 240 |
. . . . . . . 8
 
        
                  |
173 | 151, 172 | eqbrtrd 4416 |
. . . . . . 7
 
        
                              |
174 | 173 | adantr 472 |
. . . . . 6
                                
                  |
175 | 58, 60, 150, 174 | ifbothda 3907 |
. . . . 5
 
        
                        
                  |
176 | | 0re 9661 |
. . . . . . . 8
 |
177 | 61, 176 | keepel 3939 |
. . . . . . 7
              |
178 | 177 | a1i 11 |
. . . . . 6
 
        
               |
179 | | resubcl 9958 |
. . . . . . 7
                                   |
180 | 61, 155, 179 | sylancr 676 |
. . . . . 6
 
        
                  |
181 | 124 | necomd 2698 |
. . . . . . . 8
 
        
          |
182 | 62 | leabsd 13553 |
. . . . . . . . . 10
 
        
                      |
183 | 62, 162, 158, 182, 165 | letrd 9809 |
. . . . . . . . 9
 
        
          |
184 | 62, 158, 183 | leltned 9805 |
. . . . . . . 8
 
        
                    |
185 | 181, 184 | mpbird 240 |
. . . . . . 7
 
        
          |
186 | | posdif 10128 |
. . . . . . . 8
         
                       |
187 | 62, 61, 186 | sylancl 675 |
. . . . . . 7
 
        
                      |
188 | 185, 187 | mpbid 215 |
. . . . . 6
 
        
            |
189 | | lemuldiv 10508 |
. . . . . 6
                                                                               
               
                                            |
190 | 178, 180,
64, 188, 189 | syl112anc 1296 |
. . . . 5
 
        
                         
               
                                            |
191 | 175, 190 | mpbid 215 |
. . . 4
 
        
                                           |
192 | 31 | nn0zd 11061 |
. . . . . . . 8
   |
193 | | fzval3 12012 |
. . . . . . . 8
      ..^     |
194 | 192, 193 | syl 17 |
. . . . . . 7
      ..^     |
195 | 194 | adantr 472 |
. . . . . 6
 
        
     ..^     |
196 | 195 | sumeq1d 13844 |
. . . . 5
 
        
                  
 ..^                  |
197 | | 0nn0 10908 |
. . . . . . 7
 |
198 | 197 | a1i 11 |
. . . . . 6
 
        
  |
199 | 153, 32 | syl6eleq 2559 |
. . . . . . 7
         |
200 | 199 | adantr 472 |
. . . . . 6
 
        
        |
201 | 121, 124,
198, 200 | geoserg 14001 |
. . . . 5
 
        
  ..^                                                          |
202 | 121 | exp0d 12448 |
. . . . . . 7
 
        
              |
203 | 202 | oveq1d 6323 |
. . . . . 6
 
        
                                              |
204 | 203 | oveq1d 6323 |
. . . . 5
 
        
                                                                      |
205 | 196, 201,
204 | 3eqtrd 2509 |
. . . 4
 
        
                                                |
206 | 191, 205 | breqtrrd 4422 |
. . 3
 
        
                                 |
207 | 56, 206 | pm2.61dane 2730 |
. 2
             
                    |
208 | | rpvmasum2.1 |
. . . . 5
     |
209 | | dchrisum0f.f |
. . . . 5
              |
210 | 9, 11, 7, 126, 127, 208, 209 | dchrisum0fval 24422 |
. . . 4
              
               |
211 | 83, 210 | syl 17 |
. . 3
          
               |
212 | | fveq2 5879 |
. . . . 5
                   |
213 | 212 | fveq2d 5883 |
. . . 4
                           |
214 | | eqid 2471 |
. . . . . 6
                     |
215 | 214 | dvdsppwf1o 24194 |
. . . . 5
                             |
216 | 15, 31, 215 | syl2anc 673 |
. . . 4
                   
       |
217 | | oveq2 6316 |
. . . . . 6
           |
218 | | ovex 6336 |
. . . . . 6
     |
219 | 217, 214,
218 | fvmpt3i 5968 |
. . . . 5
                         |
220 | 219 | adantl 473 |
. . . 4
 
                         |
221 | 6 | adantr 472 |
. . . . . 6
 

                |
222 | | elrabi 3181 |
. . . . . . . 8
      
  |
223 | 222 | nnzd 11062 |
. . . . . . 7
      
  |
224 | | ffvelrn 6035 |
. . . . . . 7
                     |
225 | 14, 223, 224 | syl2an 485 |
. . . . . 6
 

                |
226 | 221, 225 | ffvelrnd 6038 |
. . . . 5
 

                |
227 | 226 | recnd 9687 |
. . . 4
 

                |
228 | 213, 5, 216, 220, 227 | fsumf1o 13866 |
. . 3
  
                                 |
229 | | zsubrg 19098 |
. . . . . . . . . . 11
SubRing ℂfld |
230 | | eqid 2471 |
. . . . . . . . . . . 12
mulGrp ℂfld mulGrp ℂfld |
231 | 230 | subrgsubm 18099 |
. . . . . . . . . . 11
 SubRing ℂfld
SubMnd mulGrp ℂfld   |
232 | 229, 231 | mp1i 13 |
. . . . . . . . . 10
 
     SubMnd mulGrp ℂfld   |
233 | 20 | adantl 473 |
. . . . . . . . . 10
 
       |
234 | 17 | adantr 472 |
. . . . . . . . . 10
 
       |
235 | | eqid 2471 |
. . . . . . . . . . 11
.g mulGrp ℂfld .g mulGrp ℂfld  |
236 | | zringmpg 19140 |
. . . . . . . . . . . 12
 mulGrp ℂfld ↾s 
mulGrp ℤring |
237 | 236 | eqcomi 2480 |
. . . . . . . . . . 11
mulGrp ℤring  mulGrp ℂfld ↾s   |
238 | | eqid 2471 |
. . . . . . . . . . 11
.g mulGrp ℤring .g mulGrp ℤring  |
239 | 235, 237,
238 | submmulg 16871 |
. . . . . . . . . 10
  SubMnd mulGrp ℂfld    .g mulGrp ℂfld     .g mulGrp ℤring     |
240 | 232, 233,
234, 239 | syl3anc 1292 |
. . . . . . . . 9
 
       .g mulGrp ℂfld     .g mulGrp ℤring     |
241 | 82 | nncnd 10647 |
. . . . . . . . . 10
   |
242 | | cnfldexp 19078 |
. . . . . . . . . 10
 
   .g mulGrp ℂfld         |
243 | 241, 20, 242 | syl2an 485 |
. . . . . . . . 9
 
       .g mulGrp ℂfld         |
244 | 240, 243 | eqtr3d 2507 |
. . . . . . . 8
 
       .g mulGrp ℤring         |
245 | 244 | fveq2d 5883 |
. . . . . . 7
 
          .g mulGrp ℤring              |
246 | 9 | zncrng 19192 |
. . . . . . . . . . 11

  |
247 | | crngring 17869 |
. . . . . . . . . . 11

  |
248 | 8, 246, 247 | 3syl 18 |
. . . . . . . . . 10
   |
249 | 11 | zrhrhm 19160 |
. . . . . . . . . 10

ℤring RingHom    |
250 | | eqid 2471 |
. . . . . . . . . . 11
mulGrp ℤring mulGrp ℤring |
251 | | eqid 2471 |
. . . . . . . . . . 11
mulGrp  mulGrp   |
252 | 250, 251 | rhmmhm 18028 |
. . . . . . . . . 10
 ℤring RingHom   mulGrp ℤring
MndHom mulGrp     |
253 | 248, 249,
252 | 3syl 18 |
. . . . . . . . 9
  mulGrp ℤring MndHom mulGrp     |
254 | 253 | adantr 472 |
. . . . . . . 8
 
      mulGrp ℤring
MndHom mulGrp     |
255 | | zringbas 19122 |
. . . . . . . . . 10
  ℤring |
256 | 250, 255 | mgpbas 17807 |
. . . . . . . . 9
   mulGrp ℤring  |
257 | | eqid 2471 |
. . . . . . . . 9
.g mulGrp   .g mulGrp    |
258 | 256, 238,
257 | mhmmulg 16868 |
. . . . . . . 8
   mulGrp ℤring MndHom mulGrp  
      .g mulGrp ℤring      .g mulGrp           |
259 | 254, 233,
234, 258 | syl3anc 1292 |
. . . . . . 7
 
          .g mulGrp ℤring      .g mulGrp           |
260 | 245, 259 | eqtr3d 2507 |
. . . . . 6
 
               .g mulGrp           |
261 | 260 | fveq2d 5883 |
. . . . 5
 
                      .g mulGrp            |
262 | 126, 9, 127 | dchrmhm 24248 |
. . . . . . . 8
 mulGrp  MndHom mulGrp ℂfld  |
263 | 262, 128 | sseldi 3416 |
. . . . . . 7
  mulGrp  MndHom mulGrp ℂfld   |
264 | 263 | adantr 472 |
. . . . . 6
 
      mulGrp  MndHom mulGrp ℂfld   |
265 | 18 | adantr 472 |
. . . . . 6
 
               |
266 | 251, 10 | mgpbas 17807 |
. . . . . . 7
       mulGrp    |
267 | 266, 257,
235 | mhmmulg 16868 |
. . . . . 6
   mulGrp  MndHom mulGrp ℂfld
        
     .g mulGrp            .g mulGrp ℂfld             |
268 | 264, 233,
265, 267 | syl3anc 1292 |
. . . . 5
 
          .g mulGrp            .g mulGrp ℂfld             |
269 | | cnfldexp 19078 |
. . . . . 6
         
   .g mulGrp ℂfld                         |
270 | 120, 20, 269 | syl2an 485 |
. . . . 5
 
       .g mulGrp ℂfld                         |
271 | 261, 268,
270 | 3eqtrd 2509 |
. . . 4
 
                               |
272 | 271 | sumeq2dv 13846 |
. . 3
                                       |
273 | 211, 228,
272 | 3eqtrd 2509 |
. 2
                             |
274 | 207, 273 | breqtrrd 4422 |
1
             
          |