Proof of Theorem jensenlem2
Step | Hyp | Ref
| Expression |
1 | | cnfld0 19069 |
. . . . . . 7
  ℂfld |
2 | | cnring 19067 |
. . . . . . . 8
ℂfld  |
3 | | ringabl 17888 |
. . . . . . . 8
ℂfld ℂfld   |
4 | 2, 3 | mp1i 13 |
. . . . . . 7
 ℂfld   |
5 | | jensen.4 |
. . . . . . . 8
   |
6 | | jensenlem.2 |
. . . . . . . . 9
       |
7 | 6 | unssad 3602 |
. . . . . . . 8

  |
8 | | ssfi 7810 |
. . . . . . . 8
  
  |
9 | 5, 7, 8 | syl2anc 673 |
. . . . . . 7
   |
10 | | resubdrg 19253 |
. . . . . . . . 9
 SubRing ℂfld
RRfld   |
11 | 10 | simpli 465 |
. . . . . . . 8
SubRing ℂfld |
12 | | subrgsubg 18092 |
. . . . . . . 8
 SubRing ℂfld
SubGrp ℂfld  |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
 SubGrp ℂfld  |
14 | | remulcl 9642 |
. . . . . . . . . 10
 
     |
15 | 14 | adantl 473 |
. . . . . . . . 9
 
       |
16 | | jensen.5 |
. . . . . . . . . 10
          |
17 | | rge0ssre 11766 |
. . . . . . . . . 10
    |
18 | | fss 5749 |
. . . . . . . . . 10
                   |
19 | 16, 17, 18 | sylancl 675 |
. . . . . . . . 9
       |
20 | | jensen.6 |
. . . . . . . . . 10
       |
21 | | jensen.1 |
. . . . . . . . . 10

  |
22 | 20, 21 | fssd 5750 |
. . . . . . . . 9
       |
23 | | inidm 3632 |
. . . . . . . . 9
   |
24 | 15, 19, 22, 5, 5, 23 | off 6565 |
. . . . . . . 8
          |
25 | 24, 7 | fssresd 5762 |
. . . . . . 7
   
        |
26 | | c0ex 9655 |
. . . . . . . . 9
 |
27 | 26 | a1i 11 |
. . . . . . . 8
   |
28 | 25, 9, 27 | fdmfifsupp 7911 |
. . . . . . 7
   
  finSupp   |
29 | 1, 4, 9, 13, 25, 28 | gsumsubgcl 17631 |
. . . . . 6
 ℂfld g   
     |
30 | 29 | recnd 9687 |
. . . . 5
 ℂfld g   
     |
31 | | ax-resscn 9614 |
. . . . . . . 8
 |
32 | 17, 31 | sstri 3427 |
. . . . . . 7
    |
33 | 6 | unssbd 3603 |
. . . . . . . . 9
     |
34 | | vex 3034 |
. . . . . . . . . 10
 |
35 | 34 | snss 4087 |
. . . . . . . . 9

    |
36 | 33, 35 | sylibr 217 |
. . . . . . . 8
   |
37 | 16, 36 | ffvelrnd 6038 |
. . . . . . 7
          |
38 | 32, 37 | sseldi 3416 |
. . . . . 6
       |
39 | 20, 36 | ffvelrnd 6038 |
. . . . . . . 8
       |
40 | 21, 39 | sseldd 3419 |
. . . . . . 7
       |
41 | 40 | recnd 9687 |
. . . . . 6
       |
42 | 38, 41 | mulcld 9681 |
. . . . 5
             |
43 | | jensen.2 |
. . . . . . . 8
       |
44 | | jensen.3 |
. . . . . . . 8
 

    ![[,] [,]](_icc.gif) 
  |
45 | | jensen.7 |
. . . . . . . 8
 ℂfld g    |
46 | | jensen.8 |
. . . . . . . 8
 

  ![[,] [,]](_icc.gif)               
                  |
47 | | jensenlem.1 |
. . . . . . . 8
   |
48 | | jensenlem.s |
. . . . . . . 8
ℂfld g 
   |
49 | | jensenlem.l |
. . . . . . . 8
ℂfld g 
       |
50 | 21, 43, 44, 5, 16, 20, 45, 46, 47, 6, 48, 49 | jensenlem1 23991 |
. . . . . . 7
         |
51 | | jensenlem.3 |
. . . . . . . . 9
   |
52 | 51 | rpred 11364 |
. . . . . . . 8
   |
53 | | elrege0 11764 |
. . . . . . . . . 10
       
            |
54 | 53 | simplbi 467 |
. . . . . . . . 9
       
      |
55 | 37, 54 | syl 17 |
. . . . . . . 8
       |
56 | 52, 55 | readdcld 9688 |
. . . . . . 7
         |
57 | 50, 56 | eqeltrd 2549 |
. . . . . 6
   |
58 | 57 | recnd 9687 |
. . . . 5
   |
59 | | 0red 9662 |
. . . . . . 7
   |
60 | 51 | rpgt0d 11367 |
. . . . . . 7
   |
61 | 53 | simprbi 471 |
. . . . . . . . . 10
       
      |
62 | 37, 61 | syl 17 |
. . . . . . . . 9

      |
63 | 52, 55 | addge01d 10222 |
. . . . . . . . 9
               |
64 | 62, 63 | mpbid 215 |
. . . . . . . 8

        |
65 | 64, 50 | breqtrrd 4422 |
. . . . . . 7

  |
66 | 59, 52, 57, 60, 65 | ltletrd 9812 |
. . . . . 6
   |
67 | 66 | gt0ne0d 10199 |
. . . . 5
   |
68 | 30, 42, 58, 67 | divdird 10443 |
. . . 4
   ℂfld g   
                 ℂfld g   
                   |
69 | | cnfldbas 19051 |
. . . . . . 7
  ℂfld |
70 | | cnfldadd 19052 |
. . . . . . 7
 ℂfld |
71 | | ringcmn 17889 |
. . . . . . . 8
ℂfld ℂfld CMnd |
72 | 2, 71 | mp1i 13 |
. . . . . . 7
 ℂfld CMnd |
73 | 7 | sselda 3418 |
. . . . . . . . . 10
 
   |
74 | 16 | ffvelrnda 6037 |
. . . . . . . . . 10
 
          |
75 | 73, 74 | syldan 478 |
. . . . . . . . 9
 
          |
76 | 32, 75 | sseldi 3416 |
. . . . . . . 8
 
       |
77 | 21 | adantr 472 |
. . . . . . . . . 10
 
   |
78 | 20 | ffvelrnda 6037 |
. . . . . . . . . . 11
 
       |
79 | 73, 78 | syldan 478 |
. . . . . . . . . 10
 
       |
80 | 77, 79 | sseldd 3419 |
. . . . . . . . 9
 
       |
81 | 80 | recnd 9687 |
. . . . . . . 8
 
       |
82 | 76, 81 | mulcld 9681 |
. . . . . . 7
 
             |
83 | | fveq2 5879 |
. . . . . . . 8
           |
84 | | fveq2 5879 |
. . . . . . . 8
           |
85 | 83, 84 | oveq12d 6326 |
. . . . . . 7
                       |
86 | 69, 70, 72, 9, 82, 36, 47, 42, 85 | gsumunsn 17670 |
. . . . . 6
 ℂfld g 

                ℂfld g                           |
87 | 16 | feqmptd 5932 |
. . . . . . . . . 10
         |
88 | 20 | feqmptd 5932 |
. . . . . . . . . 10
         |
89 | 5, 74, 78, 87, 88 | offval2 6567 |
. . . . . . . . 9
                  |
90 | 89 | reseq1d 5110 |
. . . . . . . 8
   
                          |
91 | 6 | resmptd 5162 |
. . . . . . . 8
              
                      |
92 | 90, 91 | eqtrd 2505 |
. . . . . . 7
   
                        |
93 | 92 | oveq2d 6324 |
. . . . . 6
 ℂfld g   
       ℂfld g                    |
94 | 89 | reseq1d 5110 |
. . . . . . . . 9
   
                  |
95 | 7 | resmptd 5162 |
. . . . . . . . 9
                             |
96 | 94, 95 | eqtrd 2505 |
. . . . . . . 8
   
                |
97 | 96 | oveq2d 6324 |
. . . . . . 7
 ℂfld g   
   ℂfld g 
              |
98 | 97 | oveq1d 6323 |
. . . . . 6
  ℂfld g   
               ℂfld g 
                         |
99 | 86, 93, 98 | 3eqtr4d 2515 |
. . . . 5
 ℂfld g   
        ℂfld g                    |
100 | 99 | oveq1d 6323 |
. . . 4
  ℂfld g   
          ℂfld g                     |
101 | 52 | recnd 9687 |
. . . . . 6
   |
102 | 51 | rpne0d 11369 |
. . . . . 6
   |
103 | 30, 101, 58, 102, 67 | dmdcand 10434 |
. . . . 5
     ℂfld g          ℂfld g   
      |
104 | 58, 101, 58, 67 | divsubdird 10444 |
. . . . . . . 8
             |
105 | 50 | oveq1d 6323 |
. . . . . . . . . 10
             |
106 | 101, 38 | pncan2d 10007 |
. . . . . . . . . 10
               |
107 | 105, 106 | eqtrd 2505 |
. . . . . . . . 9
         |
108 | 107 | oveq1d 6323 |
. . . . . . . 8
             |
109 | 58, 67 | dividd 10403 |
. . . . . . . . 9
     |
110 | 109 | oveq1d 6323 |
. . . . . . . 8
             |
111 | 104, 108,
110 | 3eqtr3rd 2514 |
. . . . . . 7
             |
112 | 111 | oveq1d 6323 |
. . . . . 6
                         |
113 | 38, 41, 58, 67 | div23d 10442 |
. . . . . 6
                           |
114 | 112, 113 | eqtr4d 2508 |
. . . . 5
                         |
115 | 103, 114 | oveq12d 6326 |
. . . 4
      ℂfld g   
                  ℂfld g   
                   |
116 | 68, 100, 115 | 3eqtr4d 2515 |
. . 3
  ℂfld g   
             ℂfld g   
                  |
117 | | jensenlem.4 |
. . . . 5
  ℂfld g   
      |
118 | 52, 57, 67 | redivcld 10457 |
. . . . . 6
     |
119 | 51 | rpge0d 11368 |
. . . . . . 7

  |
120 | | divge0 10496 |
. . . . . . 7
  
   
    |
121 | 52, 119, 57, 66, 120 | syl22anc 1293 |
. . . . . 6

    |
122 | 58 | mulid1d 9678 |
. . . . . . . 8
     |
123 | 65, 122 | breqtrrd 4422 |
. . . . . . 7

    |
124 | | 1red 9676 |
. . . . . . . 8
   |
125 | | ledivmul 10503 |
. . . . . . . 8
 

          |
126 | 52, 124, 57, 66, 125 | syl112anc 1296 |
. . . . . . 7
         |
127 | 123, 126 | mpbird 240 |
. . . . . 6
  
  |
128 | | 0re 9661 |
. . . . . . 7
 |
129 | | 1re 9660 |
. . . . . . 7
 |
130 | 128, 129 | elicc2i 11725 |
. . . . . 6
     ![[,] [,]](_icc.gif) 
    
     |
131 | 118, 121,
127, 130 | syl3anbrc 1214 |
. . . . 5
     ![[,] [,]](_icc.gif)    |
132 | 117, 39, 131 | 3jca 1210 |
. . . 4
   ℂfld g   
        
   ![[,] [,]](_icc.gif)     |
133 | 21, 44 | cvxcl 23989 |
. . . 4
 
  ℂfld g            
   ![[,] [,]](_icc.gif)   
     ℂfld g                      |
134 | 132, 133 | mpdan 681 |
. . 3
      ℂfld g   
                  |
135 | 116, 134 | eqeltrd 2549 |
. 2
  ℂfld g   
          |
136 | 43, 134 | ffvelrnd 6038 |
. . . 4
         ℂfld g                       |
137 | 43, 117 | ffvelrnd 6038 |
. . . . . 6
     ℂfld g           |
138 | 118, 137 | remulcld 9689 |
. . . . 5
        ℂfld g   
        |
139 | 43, 39 | ffvelrnd 6038 |
. . . . . . 7
           |
140 | 55, 139 | remulcld 9689 |
. . . . . 6
                 |
141 | 140, 57, 67 | redivcld 10457 |
. . . . 5
                   |
142 | 138, 141 | readdcld 9688 |
. . . 4
         ℂfld g                             |
143 | | fco 5751 |
. . . . . . . . . . 11
                   |
144 | 43, 20, 143 | syl2anc 673 |
. . . . . . . . . 10
         |
145 | 15, 19, 144, 5, 5, 23 | off 6565 |
. . . . . . . . 9
            |
146 | 145, 7 | fssresd 5762 |
. . . . . . . 8
   
          |
147 | 146, 9, 27 | fdmfifsupp 7911 |
. . . . . . . 8
   
   
finSupp   |
148 | 1, 4, 9, 13, 146, 147 | gsumsubgcl 17631 |
. . . . . . 7
 ℂfld g   
       |
149 | 148, 52, 102 | redivcld 10457 |
. . . . . 6
  ℂfld g   
        |
150 | 118, 149 | remulcld 9689 |
. . . . 5
     ℂfld g             |
151 | | resubcl 9958 |
. . . . . . 7
  
        |
152 | 129, 118,
151 | sylancr 676 |
. . . . . 6
       |
153 | 152, 139 | remulcld 9689 |
. . . . 5
                 |
154 | 150, 153 | readdcld 9688 |
. . . 4
      ℂfld g   
                        |
155 | | oveq2 6316 |
. . . . . . . . . . . 12
  ℂfld g   
        ℂfld g   
       |
156 | 155 | oveq1d 6323 |
. . . . . . . . . . 11
  ℂfld g   
               ℂfld g   
            |
157 | 156 | fveq2d 5883 |
. . . . . . . . . 10
  ℂfld g   
                      ℂfld g   
             |
158 | | fveq2 5879 |
. . . . . . . . . . . 12
  ℂfld g   
            ℂfld g   
       |
159 | 158 | oveq2d 6324 |
. . . . . . . . . . 11
  ℂfld g   
               ℂfld g            |
160 | 159 | oveq1d 6323 |
. . . . . . . . . 10
  ℂfld g   
                          ℂfld g   
                 |
161 | 157, 160 | breq12d 4408 |
. . . . . . . . 9
  ℂfld g   
                
               
      ℂfld g   
                 ℂfld g                      |
162 | 161 | imbi2d 323 |
. . . . . . . 8
  ℂfld g   
     
                            
       ℂfld g                     ℂfld g                       |
163 | | oveq2 6316 |
. . . . . . . . . . . 12
                   |
164 | 163 | oveq2d 6324 |
. . . . . . . . . . 11
        ℂfld g                 ℂfld g                    |
165 | 164 | fveq2d 5883 |
. . . . . . . . . 10
           ℂfld g                     ℂfld g   
                 |
166 | | fveq2 5879 |
. . . . . . . . . . . 12
                   |
167 | 166 | oveq2d 6324 |
. . . . . . . . . . 11
                           |
168 | 167 | oveq2d 6324 |
. . . . . . . . . 10
           ℂfld g   
                     ℂfld g                         |
169 | 165, 168 | breq12d 4408 |
. . . . . . . . 9
            ℂfld g                     ℂfld g                  
      ℂfld g   
                     ℂfld g                          |
170 | 169 | imbi2d 323 |
. . . . . . . 8
      
      ℂfld g   
                 ℂfld g                    
      ℂfld g   
                     ℂfld g                           |
171 | | oveq1 6315 |
. . . . . . . . . . . 12
     ℂfld g             ℂfld g   
       |
172 | | oveq2 6316 |
. . . . . . . . . . . . 13
           |
173 | 172 | oveq1d 6323 |
. . . . . . . . . . . 12
                       |
174 | 171, 173 | oveq12d 6326 |
. . . . . . . . . . 11
      ℂfld g                       ℂfld g                      |
175 | 174 | fveq2d 5883 |
. . . . . . . . . 10
         ℂfld g                           ℂfld g   
                   |
176 | | oveq1 6315 |
. . . . . . . . . . 11
        ℂfld g   
             ℂfld g            |
177 | 172 | oveq1d 6323 |
. . . . . . . . . . 11
                               |
178 | 176, 177 | oveq12d 6326 |
. . . . . . . . . 10
         ℂfld g   
                           ℂfld g                           |
179 | 175, 178 | breq12d 4408 |
. . . . . . . . 9
          ℂfld g                         ℂfld g                      
        ℂfld g   
                         ℂfld g                            |
180 | 179 | imbi2d 323 |
. . . . . . . 8
    
      ℂfld g   
                     ℂfld g                        
        ℂfld g   
                         ℂfld g                             |
181 | 46 | expcom 442 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)                                   |
182 | 162, 170,
180, 181 | vtocl3ga 3103 |
. . . . . . 7
   ℂfld g   
        
   ![[,] [,]](_icc.gif)            ℂfld g                    
        ℂfld g   
                        |
183 | 117, 39, 131, 182 | syl3anc 1292 |
. . . . . 6
          ℂfld g                    
        ℂfld g   
                        |
184 | 183 | pm2.43i 48 |
. . . . 5
         ℂfld g                             ℂfld g                           |
185 | 111 | oveq1d 6323 |
. . . . . . 7
                                 |
186 | 139 | recnd 9687 |
. . . . . . . 8
           |
187 | 38, 186, 58, 67 | div23d 10442 |
. . . . . . 7
                                   |
188 | 185, 187 | eqtr4d 2508 |
. . . . . 6
                                 |
189 | 188 | oveq2d 6324 |
. . . . 5
         ℂfld g                                 ℂfld g                             |
190 | 184, 189 | breqtrd 4420 |
. . . 4
         ℂfld g                             ℂfld g                             |
191 | 187, 185 | eqtr4d 2508 |
. . . . . 6
                                 |
192 | 191 | oveq2d 6324 |
. . . . 5
         ℂfld g                                   ℂfld g   
                       |
193 | | jensenlem.5 |
. . . . . . 7
     ℂfld g          ℂfld g   
        |
194 | 52, 57, 60, 66 | divgt0d 10564 |
. . . . . . . 8
     |
195 | | lemul2 10480 |
. . . . . . . 8
      ℂfld g          ℂfld g                      ℂfld g   
      ℂfld g   
     
       ℂfld g              ℂfld g   
          |
196 | 137, 149,
118, 194, 195 | syl112anc 1296 |
. . . . . . 7
      ℂfld g   
      ℂfld g   
     
       ℂfld g              ℂfld g   
          |
197 | 193, 196 | mpbid 215 |
. . . . . 6
        ℂfld g   
          ℂfld g   
         |
198 | 138, 150,
153, 197 | leadd1dd 10248 |
. . . . 5
         ℂfld g                              ℂfld g   
                        |
199 | 192, 198 | eqbrtrd 4416 |
. . . 4
         ℂfld g                                ℂfld g                            |
200 | 136, 142,
154, 190, 199 | letrd 9809 |
. . 3
         ℂfld g                          ℂfld g   
                        |
201 | 116 | fveq2d 5883 |
. . 3
     ℂfld g     
               ℂfld g   
                   |
202 | 148 | recnd 9687 |
. . . . 5
 ℂfld g   
       |
203 | 140 | recnd 9687 |
. . . . 5
                 |
204 | 202, 203,
58, 67 | divdird 10443 |
. . . 4
   ℂfld g   
                       ℂfld g                             |
205 | 17, 74 | sseldi 3416 |
. . . . . . . . . 10
 
       |
206 | 43 | ffvelrnda 6037 |
. . . . . . . . . . 11
 
    
          |
207 | 78, 206 | syldan 478 |
. . . . . . . . . 10
 
           |
208 | 205, 207 | remulcld 9689 |
. . . . . . . . 9
 
                 |
209 | 208 | recnd 9687 |
. . . . . . . 8
 
                 |
210 | 73, 209 | syldan 478 |
. . . . . . 7
 
                 |
211 | 84 | fveq2d 5883 |
. . . . . . . 8
                   |
212 | 83, 211 | oveq12d 6326 |
. . . . . . 7
                               |
213 | 69, 70, 72, 9, 210, 36, 47, 203, 212 | gsumunsn 17670 |
. . . . . 6
 ℂfld g 

                    ℂfld g                                   |
214 | 43 | feqmptd 5932 |
. . . . . . . . . . 11
         |
215 | | fveq2 5879 |
. . . . . . . . . . 11
                   |
216 | 78, 88, 214, 215 | fmptco 6072 |
. . . . . . . . . 10
               |
217 | 5, 74, 207, 87, 216 | offval2 6567 |
. . . . . . . . 9
                        |
218 | 217 | reseq1d 5110 |
. . . . . . . 8
   
   
                     
      |
219 | 6 | resmptd 5162 |
. . . . . . . 8
                  
                          |
220 | 218, 219 | eqtrd 2505 |
. . . . . . 7
   
   
                          |
221 | 220 | oveq2d 6324 |
. . . . . 6
 ℂfld g   
   
     ℂfld g 

                     |
222 | 217 | reseq1d 5110 |
. . . . . . . . 9
   
                    
   |
223 | 7 | resmptd 5162 |
. . . . . . . . 9
                                     |
224 | 222, 223 | eqtrd 2505 |
. . . . . . . 8
   
                      |
225 | 224 | oveq2d 6324 |
. . . . . . 7
 ℂfld g   
     ℂfld g 
                  |
226 | 225 | oveq1d 6323 |
. . . . . 6
  ℂfld g   
                     ℂfld g                                   |
227 | 213, 221,
226 | 3eqtr4d 2515 |
. . . . 5
 ℂfld g   
   
      ℂfld g   
                      |
228 | 227 | oveq1d 6323 |
. . . 4
  ℂfld g   
   
        ℂfld g   
                       |
229 | 202, 101,
58, 102, 67 | dmdcand 10434 |
. . . . 5
     ℂfld g            ℂfld g   
        |
230 | 229, 188 | oveq12d 6326 |
. . . 4
      ℂfld g   
                        ℂfld g   
                         |
231 | 204, 228,
230 | 3eqtr4d 2515 |
. . 3
  ℂfld g   
   
           ℂfld g   
                        |
232 | 200, 201,
231 | 3brtr4d 4426 |
. 2
     ℂfld g     
        ℂfld g   
   
        |
233 | 135, 232 | jca 541 |
1
   ℂfld g   
            ℂfld g   
        
 ℂfld g   
   
         |