Step | Hyp | Ref
| Expression |
1 | | cnfld0 19770 |
. . . . . . . 8
ℂfld |
2 | | cnring 19768 |
. . . . . . . . 9
ℂfld |
3 | | ringabl 18580 |
. . . . . . . . 9
ℂfld ℂfld |
4 | 2, 3 | mp1i 13 |
. . . . . . . 8
ℂfld |
5 | | amgm.2 |
. . . . . . . 8
|
6 | | resubdrg 19954 |
. . . . . . . . . 10
SubRingℂfld
RRfld |
7 | 6 | simpli 474 |
. . . . . . . . 9
SubRingℂfld |
8 | | subrgsubg 18786 |
. . . . . . . . 9
SubRingℂfld
SubGrpℂfld |
9 | 7, 8 | mp1i 13 |
. . . . . . . 8
SubGrpℂfld |
10 | | amgm.4 |
. . . . . . . . . . . 12
|
11 | 10 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
12 | 11 | relogcld 24369 |
. . . . . . . . . 10
|
13 | 12 | renegcld 10457 |
. . . . . . . . 9
|
14 | | eqid 2622 |
. . . . . . . . 9
|
15 | 13, 14 | fmptd 6385 |
. . . . . . . 8
|
16 | | c0ex 10034 |
. . . . . . . . . 10
|
17 | 16 | a1i 11 |
. . . . . . . . 9
|
18 | 15, 5, 17 | fdmfifsupp 8285 |
. . . . . . . 8
finSupp
|
19 | 1, 4, 5, 9, 15, 18 | gsumsubgcl 18320 |
. . . . . . 7
ℂfld g |
20 | 19 | recnd 10068 |
. . . . . 6
ℂfld g |
21 | | amgm.3 |
. . . . . . . 8
|
22 | | hashnncl 13157 |
. . . . . . . . 9
|
23 | 5, 22 | syl 17 |
. . . . . . . 8
|
24 | 21, 23 | mpbird 247 |
. . . . . . 7
|
25 | 24 | nncnd 11036 |
. . . . . 6
|
26 | 24 | nnne0d 11065 |
. . . . . 6
|
27 | 20, 25, 26 | divnegd 10814 |
. . . . 5
ℂfld g ℂfld g |
28 | 12 | recnd 10068 |
. . . . . . . . . 10
|
29 | 5, 28 | gsumfsum 19813 |
. . . . . . . . 9
ℂfld g |
30 | 28 | negnegd 10383 |
. . . . . . . . . 10
|
31 | 30 | sumeq2dv 14433 |
. . . . . . . . 9
|
32 | 13 | recnd 10068 |
. . . . . . . . . 10
|
33 | 5, 32 | fsumneg 14519 |
. . . . . . . . 9
|
34 | 29, 31, 33 | 3eqtr2rd 2663 |
. . . . . . . 8
ℂfld g |
35 | 5, 32 | gsumfsum 19813 |
. . . . . . . . 9
ℂfld g |
36 | 35 | negeqd 10275 |
. . . . . . . 8
ℂfld g |
37 | 10 | feqmptd 6249 |
. . . . . . . . . 10
|
38 | | relogf1o 24313 |
. . . . . . . . . . . . 13
|
39 | | f1of 6137 |
. . . . . . . . . . . . 13
|
40 | 38, 39 | mp1i 13 |
. . . . . . . . . . . 12
|
41 | 40 | feqmptd 6249 |
. . . . . . . . . . 11
|
42 | | fvres 6207 |
. . . . . . . . . . . 12
|
43 | 42 | mpteq2ia 4740 |
. . . . . . . . . . 11
|
44 | 41, 43 | syl6eq 2672 |
. . . . . . . . . 10
|
45 | | fveq2 6191 |
. . . . . . . . . 10
|
46 | 11, 37, 44, 45 | fmptco 6396 |
. . . . . . . . 9
|
47 | 46 | oveq2d 6666 |
. . . . . . . 8
ℂfld g ℂfld g |
48 | 34, 36, 47 | 3eqtr4d 2666 |
. . . . . . 7
ℂfld g ℂfld g |
49 | | amgm.1 |
. . . . . . . . . . . . . . 15
mulGrpℂfld |
50 | 49 | oveq1i 6660 |
. . . . . . . . . . . . . 14
↾s mulGrpℂfld
↾s |
51 | 50 | rpmsubg 19810 |
. . . . . . . . . . . . 13
SubGrp ↾s |
52 | | subgsubm 17616 |
. . . . . . . . . . . . 13
SubGrp ↾s SubMnd ↾s |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . 12
SubMnd ↾s |
54 | | cnfldbas 19750 |
. . . . . . . . . . . . . . 15
ℂfld |
55 | | cndrng 19775 |
. . . . . . . . . . . . . . 15
ℂfld |
56 | 54, 1, 55 | drngui 18753 |
. . . . . . . . . . . . . 14
Unitℂfld |
57 | 56, 49 | unitsubm 18670 |
. . . . . . . . . . . . 13
ℂfld SubMnd |
58 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾s
↾s |
59 | 58 | subsubm 17357 |
. . . . . . . . . . . . 13
SubMnd SubMnd ↾s
SubMnd |
60 | 2, 57, 59 | mp2b 10 |
. . . . . . . . . . . 12
SubMnd ↾s
SubMnd
|
61 | 53, 60 | mpbi 220 |
. . . . . . . . . . 11
SubMnd
|
62 | 61 | simpli 474 |
. . . . . . . . . 10
SubMnd |
63 | | eqid 2622 |
. . . . . . . . . . 11
↾s
↾s |
64 | 63 | submbas 17355 |
. . . . . . . . . 10
SubMnd
↾s |
65 | 62, 64 | ax-mp 5 |
. . . . . . . . 9
↾s |
66 | | cnfld1 19771 |
. . . . . . . . . . . 12
ℂfld |
67 | 49, 66 | ringidval 18503 |
. . . . . . . . . . 11
|
68 | 63, 67 | subm0 17356 |
. . . . . . . . . 10
SubMnd ↾s |
69 | 62, 68 | ax-mp 5 |
. . . . . . . . 9
↾s |
70 | | cncrng 19767 |
. . . . . . . . . . 11
ℂfld |
71 | 49 | crngmgp 18555 |
. . . . . . . . . . 11
ℂfld
CMnd |
72 | 70, 71 | mp1i 13 |
. . . . . . . . . 10
CMnd |
73 | 63 | submmnd 17354 |
. . . . . . . . . . 11
SubMnd
↾s |
74 | 62, 73 | mp1i 13 |
. . . . . . . . . 10
↾s |
75 | 63 | subcmn 18242 |
. . . . . . . . . 10
CMnd ↾s
↾s CMnd |
76 | 72, 74, 75 | syl2anc 693 |
. . . . . . . . 9
↾s CMnd |
77 | | df-refld 19951 |
. . . . . . . . . . . 12
RRfld ℂfld ↾s |
78 | 77 | subrgring 18783 |
. . . . . . . . . . 11
SubRingℂfld
RRfld |
79 | 7, 78 | ax-mp 5 |
. . . . . . . . . 10
RRfld |
80 | | ringmnd 18556 |
. . . . . . . . . 10
RRfld RRfld |
81 | 79, 80 | mp1i 13 |
. . . . . . . . 9
RRfld |
82 | 49 | oveq1i 6660 |
. . . . . . . . . . . 12
↾s
mulGrpℂfld ↾s |
83 | 82 | reloggim 24345 |
. . . . . . . . . . 11
↾s GrpIso
RRfld |
84 | | gimghm 17706 |
. . . . . . . . . . 11
↾s GrpIso RRfld ↾s RRfld |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . 10
↾s RRfld |
86 | | ghmmhm 17670 |
. . . . . . . . . 10
↾s RRfld
↾s MndHom
RRfld |
87 | 85, 86 | mp1i 13 |
. . . . . . . . 9
↾s MndHom RRfld |
88 | | 1ex 10035 |
. . . . . . . . . . 11
|
89 | 88 | a1i 11 |
. . . . . . . . . 10
|
90 | 10, 5, 89 | fdmfifsupp 8285 |
. . . . . . . . 9
finSupp |
91 | 65, 69, 76, 81, 5, 87, 10, 90 | gsummhm 18338 |
. . . . . . . 8
RRfld g ↾s g |
92 | | subgsubm 17616 |
. . . . . . . . . 10
SubGrpℂfld
SubMndℂfld |
93 | 9, 92 | syl 17 |
. . . . . . . . 9
SubMndℂfld |
94 | | fco 6058 |
. . . . . . . . . 10
|
95 | 40, 10, 94 | syl2anc 693 |
. . . . . . . . 9
|
96 | 5, 93, 95, 77 | gsumsubm 17373 |
. . . . . . . 8
ℂfld g RRfld g |
97 | 62 | a1i 11 |
. . . . . . . . . 10
SubMnd |
98 | 5, 97, 10, 63 | gsumsubm 17373 |
. . . . . . . . 9
g
↾s g |
99 | 98 | fveq2d 6195 |
. . . . . . . 8
g ↾s g |
100 | 91, 96, 99 | 3eqtr4d 2666 |
. . . . . . 7
ℂfld g g |
101 | 67, 72, 5, 97, 10, 90 | gsumsubmcl 18319 |
. . . . . . . 8
g |
102 | | fvres 6207 |
. . . . . . . 8
g g g |
103 | 101, 102 | syl 17 |
. . . . . . 7
g g |
104 | 48, 100, 103 | 3eqtrd 2660 |
. . . . . 6
ℂfld g g |
105 | 104 | oveq1d 6665 |
. . . . 5
ℂfld g g |
106 | 101 | relogcld 24369 |
. . . . . . 7
g |
107 | 106 | recnd 10068 |
. . . . . 6
g |
108 | 107, 25, 26 | divrec2d 10805 |
. . . . 5
g g |
109 | 27, 105, 108 | 3eqtrd 2660 |
. . . 4
ℂfld g g |
110 | 37 | oveq2d 6666 |
. . . . . . . . 9
ℂfld g ℂfld g |
111 | 11 | rpcnd 11874 |
. . . . . . . . . 10
|
112 | 5, 111 | gsumfsum 19813 |
. . . . . . . . 9
ℂfld g |
113 | 110, 112 | eqtrd 2656 |
. . . . . . . 8
ℂfld g
|
114 | 5, 21, 11 | fsumrpcl 14468 |
. . . . . . . 8
|
115 | 113, 114 | eqeltrd 2701 |
. . . . . . 7
ℂfld g |
116 | 24 | nnrpd 11870 |
. . . . . . 7
|
117 | 115, 116 | rpdivcld 11889 |
. . . . . 6
ℂfld g |
118 | 117 | relogcld 24369 |
. . . . 5
ℂfld g |
119 | 19, 24 | nndivred 11069 |
. . . . 5
ℂfld g |
120 | | rpssre 11843 |
. . . . . . . . 9
|
121 | 120 | a1i 11 |
. . . . . . . 8
|
122 | | relogcl 24322 |
. . . . . . . . . . 11
|
123 | 122 | adantl 482 |
. . . . . . . . . 10
|
124 | 123 | renegcld 10457 |
. . . . . . . . 9
|
125 | | eqid 2622 |
. . . . . . . . 9
|
126 | 124, 125 | fmptd 6385 |
. . . . . . . 8
|
127 | | ioorp 12251 |
. . . . . . . . . . . 12
|
128 | 127 | eleq2i 2693 |
. . . . . . . . . . 11
|
129 | 127 | eleq2i 2693 |
. . . . . . . . . . 11
|
130 | | iccssioo2 12246 |
. . . . . . . . . . 11
|
131 | 128, 129,
130 | syl2anbr 497 |
. . . . . . . . . 10
|
132 | 131, 127 | syl6sseq 3651 |
. . . . . . . . 9
|
133 | 132 | adantl 482 |
. . . . . . . 8
|
134 | 24 | nnrecred 11066 |
. . . . . . . . . 10
|
135 | 116 | rpreccld 11882 |
. . . . . . . . . . 11
|
136 | 135 | rpge0d 11876 |
. . . . . . . . . 10
|
137 | | elrege0 12278 |
. . . . . . . . . 10
|
138 | 134, 136,
137 | sylanbrc 698 |
. . . . . . . . 9
|
139 | | fconst6g 6094 |
. . . . . . . . 9
|
140 | 138, 139 | syl 17 |
. . . . . . . 8
|
141 | | 0lt1 10550 |
. . . . . . . . 9
|
142 | | fconstmpt 5163 |
. . . . . . . . . . 11
|
143 | 142 | oveq2i 6661 |
. . . . . . . . . 10
ℂfld g ℂfld g |
144 | | ringmnd 18556 |
. . . . . . . . . . . . 13
ℂfld ℂfld |
145 | 2, 144 | mp1i 13 |
. . . . . . . . . . . 12
ℂfld |
146 | 134 | recnd 10068 |
. . . . . . . . . . . 12
|
147 | | eqid 2622 |
. . . . . . . . . . . . 13
.gℂfld
.gℂfld |
148 | 54, 147 | gsumconst 18334 |
. . . . . . . . . . . 12
ℂfld
ℂfld g .gℂfld |
149 | 145, 5, 146, 148 | syl3anc 1326 |
. . . . . . . . . . 11
ℂfld g .gℂfld |
150 | 24 | nnzd 11481 |
. . . . . . . . . . . 12
|
151 | | cnfldmulg 19778 |
. . . . . . . . . . . 12
.gℂfld |
152 | 150, 146,
151 | syl2anc 693 |
. . . . . . . . . . 11
.gℂfld |
153 | 25, 26 | recidd 10796 |
. . . . . . . . . . 11
|
154 | 149, 152,
153 | 3eqtrd 2660 |
. . . . . . . . . 10
ℂfld g |
155 | 143, 154 | syl5eq 2668 |
. . . . . . . . 9
ℂfld g
|
156 | 141, 155 | syl5breqr 4691 |
. . . . . . . 8
ℂfld g |
157 | | logccv 24409 |
. . . . . . . . . . . 12
|
158 | 157 | 3adant1 1079 |
. . . . . . . . . . 11
|
159 | | ioossre 12235 |
. . . . . . . . . . . . . . 15
|
160 | | simp3 1063 |
. . . . . . . . . . . . . . 15
|
161 | 159, 160 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
162 | | simp21 1094 |
. . . . . . . . . . . . . . 15
|
163 | 162 | relogcld 24369 |
. . . . . . . . . . . . . 14
|
164 | 161, 163 | remulcld 10070 |
. . . . . . . . . . . . 13
|
165 | | 1re 10039 |
. . . . . . . . . . . . . . 15
|
166 | | resubcl 10345 |
. . . . . . . . . . . . . . 15
|
167 | 165, 161,
166 | sylancr 695 |
. . . . . . . . . . . . . 14
|
168 | | simp22 1095 |
. . . . . . . . . . . . . . 15
|
169 | 168 | relogcld 24369 |
. . . . . . . . . . . . . 14
|
170 | 167, 169 | remulcld 10070 |
. . . . . . . . . . . . 13
|
171 | 164, 170 | readdcld 10069 |
. . . . . . . . . . . 12
|
172 | | simp1 1061 |
. . . . . . . . . . . . . 14
|
173 | | ioossicc 12259 |
. . . . . . . . . . . . . . 15
|
174 | 173, 160 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
175 | 121, 133 | cvxcl 24711 |
. . . . . . . . . . . . . 14
|
176 | 172, 162,
168, 174, 175 | syl13anc 1328 |
. . . . . . . . . . . . 13
|
177 | 176 | relogcld 24369 |
. . . . . . . . . . . 12
|
178 | 171, 177 | ltnegd 10605 |
. . . . . . . . . . 11
|
179 | 158, 178 | mpbid 222 |
. . . . . . . . . 10
|
180 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
181 | 180 | negeqd 10275 |
. . . . . . . . . . . 12
|
182 | | negex 10279 |
. . . . . . . . . . . 12
|
183 | 181, 125,
182 | fvmpt 6282 |
. . . . . . . . . . 11
|
184 | 176, 183 | syl 17 |
. . . . . . . . . 10
|
185 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
186 | 185 | negeqd 10275 |
. . . . . . . . . . . . . . . 16
|
187 | | negex 10279 |
. . . . . . . . . . . . . . . 16
|
188 | 186, 125,
187 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
|
189 | 162, 188 | syl 17 |
. . . . . . . . . . . . . 14
|
190 | 189 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
191 | 161 | recnd 10068 |
. . . . . . . . . . . . . 14
|
192 | 163 | recnd 10068 |
. . . . . . . . . . . . . 14
|
193 | 191, 192 | mulneg2d 10484 |
. . . . . . . . . . . . 13
|
194 | 190, 193 | eqtrd 2656 |
. . . . . . . . . . . 12
|
195 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
196 | 195 | negeqd 10275 |
. . . . . . . . . . . . . . . 16
|
197 | | negex 10279 |
. . . . . . . . . . . . . . . 16
|
198 | 196, 125,
197 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
|
199 | 168, 198 | syl 17 |
. . . . . . . . . . . . . 14
|
200 | 199 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
201 | 167 | recnd 10068 |
. . . . . . . . . . . . . 14
|
202 | 169 | recnd 10068 |
. . . . . . . . . . . . . 14
|
203 | 201, 202 | mulneg2d 10484 |
. . . . . . . . . . . . 13
|
204 | 200, 203 | eqtrd 2656 |
. . . . . . . . . . . 12
|
205 | 194, 204 | oveq12d 6668 |
. . . . . . . . . . 11
|
206 | 164 | recnd 10068 |
. . . . . . . . . . . 12
|
207 | 170 | recnd 10068 |
. . . . . . . . . . . 12
|
208 | 206, 207 | negdid 10405 |
. . . . . . . . . . 11
|
209 | 205, 208 | eqtr4d 2659 |
. . . . . . . . . 10
|
210 | 179, 184,
209 | 3brtr4d 4685 |
. . . . . . . . 9
|
211 | 121, 126,
133, 210 | scvxcvx 24712 |
. . . . . . . 8
|
212 | 121, 126,
133, 5, 140, 10, 156, 211 | jensen 24715 |
. . . . . . 7
ℂfld g ℂfld g
ℂfld g ℂfld g
ℂfld g ℂfld g |
213 | 212 | simprd 479 |
. . . . . 6
ℂfld g ℂfld g
ℂfld g ℂfld g |
214 | 134 | adantr 481 |
. . . . . . . . . . . . 13
|
215 | 142 | a1i 11 |
. . . . . . . . . . . . 13
|
216 | 5, 214, 11, 215, 37 | offval2 6914 |
. . . . . . . . . . . 12
|
217 | 216 | oveq2d 6666 |
. . . . . . . . . . 11
ℂfld g ℂfld g |
218 | | cnfldadd 19751 |
. . . . . . . . . . . 12
ℂfld |
219 | | cnfldmul 19752 |
. . . . . . . . . . . 12
ℂfld |
220 | 2 | a1i 11 |
. . . . . . . . . . . 12
ℂfld |
221 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
222 | 111, 221 | fmptd 6385 |
. . . . . . . . . . . . 13
|
223 | 222, 5, 17 | fdmfifsupp 8285 |
. . . . . . . . . . . 12
finSupp
|
224 | 54, 1, 218, 219, 220, 5, 146, 111, 223 | gsummulc2 18607 |
. . . . . . . . . . 11
ℂfld g ℂfld g |
225 | | fss 6056 |
. . . . . . . . . . . . . . . 16
|
226 | 10, 120, 225 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
227 | 10, 5, 17 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . 15
finSupp |
228 | 1, 4, 5, 9, 226, 227 | gsumsubgcl 18320 |
. . . . . . . . . . . . . 14
ℂfld g |
229 | 228 | recnd 10068 |
. . . . . . . . . . . . 13
ℂfld g |
230 | 229, 25, 26 | divrec2d 10805 |
. . . . . . . . . . . 12
ℂfld g ℂfld g |
231 | 110 | oveq2d 6666 |
. . . . . . . . . . . 12
ℂfld g ℂfld g |
232 | 230, 231 | eqtr2d 2657 |
. . . . . . . . . . 11
ℂfld g ℂfld g |
233 | 217, 224,
232 | 3eqtrd 2660 |
. . . . . . . . . 10
ℂfld g ℂfld g |
234 | 233, 155 | oveq12d 6668 |
. . . . . . . . 9
ℂfld g ℂfld g ℂfld g |
235 | 228, 24 | nndivred 11069 |
. . . . . . . . . . 11
ℂfld g |
236 | 235 | recnd 10068 |
. . . . . . . . . 10
ℂfld g |
237 | 236 | div1d 10793 |
. . . . . . . . 9
ℂfld g ℂfld g |
238 | 234, 237 | eqtrd 2656 |
. . . . . . . 8
ℂfld g ℂfld g ℂfld g |
239 | 238 | fveq2d 6195 |
. . . . . . 7
ℂfld g ℂfld g
ℂfld g |
240 | | fveq2 6191 |
. . . . . . . . . 10
ℂfld g ℂfld g |
241 | 240 | negeqd 10275 |
. . . . . . . . 9
ℂfld g ℂfld g |
242 | | negex 10279 |
. . . . . . . . 9
ℂfld g |
243 | 241, 125,
242 | fvmpt 6282 |
. . . . . . . 8
ℂfld g
ℂfld g ℂfld g |
244 | 117, 243 | syl 17 |
. . . . . . 7
ℂfld g ℂfld g |
245 | 239, 244 | eqtrd 2656 |
. . . . . 6
ℂfld g ℂfld g
ℂfld g |
246 | 54, 1, 218, 219, 220, 5, 146, 32, 18 | gsummulc2 18607 |
. . . . . . . . 9
ℂfld g ℂfld g |
247 | | negex 10279 |
. . . . . . . . . . . 12
|
248 | 247 | a1i 11 |
. . . . . . . . . . 11
|
249 | | eqidd 2623 |
. . . . . . . . . . . 12
|
250 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
251 | 250 | negeqd 10275 |
. . . . . . . . . . . 12
|
252 | 11, 37, 249, 251 | fmptco 6396 |
. . . . . . . . . . 11
|
253 | 5, 214, 248, 215, 252 | offval2 6914 |
. . . . . . . . . 10
|
254 | 253 | oveq2d 6666 |
. . . . . . . . 9
ℂfld g ℂfld g |
255 | 20, 25, 26 | divrec2d 10805 |
. . . . . . . . 9
ℂfld g ℂfld g |
256 | 246, 254,
255 | 3eqtr4d 2666 |
. . . . . . . 8
ℂfld g ℂfld g |
257 | 256, 155 | oveq12d 6668 |
. . . . . . 7
ℂfld g ℂfld g ℂfld g |
258 | 119 | recnd 10068 |
. . . . . . . 8
ℂfld g |
259 | 258 | div1d 10793 |
. . . . . . 7
ℂfld g ℂfld g |
260 | 257, 259 | eqtrd 2656 |
. . . . . 6
ℂfld g ℂfld g ℂfld g |
261 | 213, 245,
260 | 3brtr3d 4684 |
. . . . 5
ℂfld g ℂfld g |
262 | 118, 119,
261 | lenegcon1d 10609 |
. . . 4
ℂfld g
ℂfld g |
263 | 109, 262 | eqbrtrrd 4677 |
. . 3
g ℂfld g |
264 | 134, 106 | remulcld 10070 |
. . . 4
g |
265 | | efle 14848 |
. . . 4
g ℂfld g g ℂfld g g
ℂfld g |
266 | 264, 118,
265 | syl2anc 693 |
. . 3
g ℂfld g g
ℂfld g |
267 | 263, 266 | mpbid 222 |
. 2
g
ℂfld g |
268 | 101 | rpcnd 11874 |
. . 3
g |
269 | 101 | rpne0d 11877 |
. . 3
g |
270 | 268, 269,
146 | cxpefd 24458 |
. 2
g g |
271 | 117 | reeflogd 24370 |
. . 3
ℂfld g ℂfld g |
272 | 271 | eqcomd 2628 |
. 2
ℂfld g ℂfld g |
273 | 267, 270,
272 | 3brtr4d 4685 |
1
g ℂfld g |