Metamath Proof Explorer

Theorem amgmlem

Description: Lemma for amgm . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Hypotheses amgm.1 
|- M = ( mulGrp ` CCfld )
amgm.2 
|- ( ph -> A e. Fin )
amgm.3 
|- ( ph -> A =/= (/) )
amgm.4 
|- ( ph -> F : A --> RR+ )
Assertion amgmlem 
|- ( ph -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )

Proof

Step Hyp Ref Expression
1 amgm.1 
 |-  M = ( mulGrp ` CCfld )
2 amgm.2 
 |-  ( ph -> A e. Fin )
3 amgm.3 
 |-  ( ph -> A =/= (/) )
4 amgm.4 
 |-  ( ph -> F : A --> RR+ )
5 cnfld0 
 |-  0 = ( 0g ` CCfld )
6 cnring 
 |-  CCfld e. Ring
7 ringabl 
 |-  ( CCfld e. Ring -> CCfld e. Abel )
8 6 7 mp1i 
 |-  ( ph -> CCfld e. Abel )
9 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
10 9 simpli 
 |-  RR e. ( SubRing ` CCfld )
11 subrgsubg 
 |-  ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) )
12 10 11 mp1i 
 |-  ( ph -> RR e. ( SubGrp ` CCfld ) )
13 4 ffvelcdmda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. RR+ )
14 13 relogcld 
 |-  ( ( ph /\ k e. A ) -> ( log ` ( F ` k ) ) e. RR )
15 14 renegcld 
 |-  ( ( ph /\ k e. A ) -> -u ( log ` ( F ` k ) ) e. RR )
16 15 fmpttd 
 |-  ( ph -> ( k e. A |-> -u ( log ` ( F ` k ) ) ) : A --> RR )
17 c0ex 
 |-  0 e. _V
18 17 a1i 
 |-  ( ph -> 0 e. _V )
19 16 2 18 fdmfifsupp 
 |-  ( ph -> ( k e. A |-> -u ( log ` ( F ` k ) ) ) finSupp 0 )
20 5 8 2 12 16 19 gsumsubgcl 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) e. RR )
21 20 recnd 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) e. CC )
22 hashnncl 
 |-  ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
23 2 22 syl 
 |-  ( ph -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
24 3 23 mpbird 
 |-  ( ph -> ( # ` A ) e. NN )
25 24 nncnd 
 |-  ( ph -> ( # ` A ) e. CC )
26 24 nnne0d 
 |-  ( ph -> ( # ` A ) =/= 0 )
27 21 25 26 divnegd 
 |-  ( ph -> -u ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) = ( -u ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) )
28 14 recnd 
 |-  ( ( ph /\ k e. A ) -> ( log ` ( F ` k ) ) e. CC )
29 2 28 gsumfsum 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> ( log ` ( F ` k ) ) ) ) = sum_ k e. A ( log ` ( F ` k ) ) )
30 28 negnegd 
 |-  ( ( ph /\ k e. A ) -> -u -u ( log ` ( F ` k ) ) = ( log ` ( F ` k ) ) )
31 30 sumeq2dv 
 |-  ( ph -> sum_ k e. A -u -u ( log ` ( F ` k ) ) = sum_ k e. A ( log ` ( F ` k ) ) )
32 15 recnd 
 |-  ( ( ph /\ k e. A ) -> -u ( log ` ( F ` k ) ) e. CC )
33 2 32 fsumneg 
 |-  ( ph -> sum_ k e. A -u -u ( log ` ( F ` k ) ) = -u sum_ k e. A -u ( log ` ( F ` k ) ) )
34 29 31 33 3eqtr2rd 
 |-  ( ph -> -u sum_ k e. A -u ( log ` ( F ` k ) ) = ( CCfld gsum ( k e. A |-> ( log ` ( F ` k ) ) ) ) )
35 2 32 gsumfsum 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) = sum_ k e. A -u ( log ` ( F ` k ) ) )
36 35 negeqd 
 |-  ( ph -> -u ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) = -u sum_ k e. A -u ( log ` ( F ` k ) ) )
37 4 feqmptd 
 |-  ( ph -> F = ( k e. A |-> ( F ` k ) ) )
38 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
39 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
40 38 39 mp1i 
 |-  ( ph -> ( log |` RR+ ) : RR+ --> RR )
41 40 feqmptd 
 |-  ( ph -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) )
42 fvres 
 |-  ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) )
43 42 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) )
44 41 43 eqtrdi 
 |-  ( ph -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
45 fveq2 
 |-  ( x = ( F ` k ) -> ( log ` x ) = ( log ` ( F ` k ) ) )
46 13 37 44 45 fmptco 
 |-  ( ph -> ( ( log |` RR+ ) o. F ) = ( k e. A |-> ( log ` ( F ` k ) ) ) )
47 46 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( log |` RR+ ) o. F ) ) = ( CCfld gsum ( k e. A |-> ( log ` ( F ` k ) ) ) ) )
48 34 36 47 3eqtr4d 
 |-  ( ph -> -u ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) = ( CCfld gsum ( ( log |` RR+ ) o. F ) ) )
49 1 oveq1i 
 |-  ( M |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
50 49 rpmsubg 
 |-  RR+ e. ( SubGrp ` ( M |`s ( CC \ { 0 } ) ) )
51 subgsubm 
 |-  ( RR+ e. ( SubGrp ` ( M |`s ( CC \ { 0 } ) ) ) -> RR+ e. ( SubMnd ` ( M |`s ( CC \ { 0 } ) ) ) )
52 50 51 ax-mp 
 |-  RR+ e. ( SubMnd ` ( M |`s ( CC \ { 0 } ) ) )
53 cnfldbas 
 |-  CC = ( Base ` CCfld )
54 cndrng 
 |-  CCfld e. DivRing
55 53 5 54 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
56 55 1 unitsubm 
 |-  ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` M ) )
57 eqid 
 |-  ( M |`s ( CC \ { 0 } ) ) = ( M |`s ( CC \ { 0 } ) )
58 57 subsubm 
 |-  ( ( CC \ { 0 } ) e. ( SubMnd ` M ) -> ( RR+ e. ( SubMnd ` ( M |`s ( CC \ { 0 } ) ) ) <-> ( RR+ e. ( SubMnd ` M ) /\ RR+ C_ ( CC \ { 0 } ) ) ) )
59 6 56 58 mp2b 
 |-  ( RR+ e. ( SubMnd ` ( M |`s ( CC \ { 0 } ) ) ) <-> ( RR+ e. ( SubMnd ` M ) /\ RR+ C_ ( CC \ { 0 } ) ) )
60 52 59 mpbi 
 |-  ( RR+ e. ( SubMnd ` M ) /\ RR+ C_ ( CC \ { 0 } ) )
61 60 simpli 
 |-  RR+ e. ( SubMnd ` M )
62 eqid 
 |-  ( M |`s RR+ ) = ( M |`s RR+ )
63 62 submbas 
 |-  ( RR+ e. ( SubMnd ` M ) -> RR+ = ( Base ` ( M |`s RR+ ) ) )
64 61 63 ax-mp 
 |-  RR+ = ( Base ` ( M |`s RR+ ) )
65 cnfld1 
 |-  1 = ( 1r ` CCfld )
66 1 65 ringidval 
 |-  1 = ( 0g ` M )
67 62 66 subm0 
 |-  ( RR+ e. ( SubMnd ` M ) -> 1 = ( 0g ` ( M |`s RR+ ) ) )
68 61 67 ax-mp 
 |-  1 = ( 0g ` ( M |`s RR+ ) )
69 cncrng 
 |-  CCfld e. CRing
70 1 crngmgp 
 |-  ( CCfld e. CRing -> M e. CMnd )
71 69 70 mp1i 
 |-  ( ph -> M e. CMnd )
72 62 submmnd 
 |-  ( RR+ e. ( SubMnd ` M ) -> ( M |`s RR+ ) e. Mnd )
73 61 72 mp1i 
 |-  ( ph -> ( M |`s RR+ ) e. Mnd )
74 62 subcmn 
 |-  ( ( M e. CMnd /\ ( M |`s RR+ ) e. Mnd ) -> ( M |`s RR+ ) e. CMnd )
75 71 73 74 syl2anc 
 |-  ( ph -> ( M |`s RR+ ) e. CMnd )
76 df-refld 
 |-  RRfld = ( CCfld |`s RR )
77 76 subrgring 
 |-  ( RR e. ( SubRing ` CCfld ) -> RRfld e. Ring )
78 10 77 ax-mp 
 |-  RRfld e. Ring
79 ringmnd 
 |-  ( RRfld e. Ring -> RRfld e. Mnd )
80 78 79 mp1i 
 |-  ( ph -> RRfld e. Mnd )
81 1 oveq1i 
 |-  ( M |`s RR+ ) = ( ( mulGrp ` CCfld ) |`s RR+ )
82 81 reloggim 
 |-  ( log |` RR+ ) e. ( ( M |`s RR+ ) GrpIso RRfld )
83 gimghm 
 |-  ( ( log |` RR+ ) e. ( ( M |`s RR+ ) GrpIso RRfld ) -> ( log |` RR+ ) e. ( ( M |`s RR+ ) GrpHom RRfld ) )
84 82 83 ax-mp 
 |-  ( log |` RR+ ) e. ( ( M |`s RR+ ) GrpHom RRfld )
85 ghmmhm 
 |-  ( ( log |` RR+ ) e. ( ( M |`s RR+ ) GrpHom RRfld ) -> ( log |` RR+ ) e. ( ( M |`s RR+ ) MndHom RRfld ) )
86 84 85 mp1i 
 |-  ( ph -> ( log |` RR+ ) e. ( ( M |`s RR+ ) MndHom RRfld ) )
87 1ex 
 |-  1 e. _V
88 87 a1i 
 |-  ( ph -> 1 e. _V )
89 4 2 88 fdmfifsupp 
 |-  ( ph -> F finSupp 1 )
90 64 68 75 80 2 86 4 89 gsummhm 
 |-  ( ph -> ( RRfld gsum ( ( log |` RR+ ) o. F ) ) = ( ( log |` RR+ ) ` ( ( M |`s RR+ ) gsum F ) ) )
91 subgsubm 
 |-  ( RR e. ( SubGrp ` CCfld ) -> RR e. ( SubMnd ` CCfld ) )
92 12 91 syl 
 |-  ( ph -> RR e. ( SubMnd ` CCfld ) )
93 fco 
 |-  ( ( ( log |` RR+ ) : RR+ --> RR /\ F : A --> RR+ ) -> ( ( log |` RR+ ) o. F ) : A --> RR )
94 40 4 93 syl2anc 
 |-  ( ph -> ( ( log |` RR+ ) o. F ) : A --> RR )
95 2 92 94 76 gsumsubm 
 |-  ( ph -> ( CCfld gsum ( ( log |` RR+ ) o. F ) ) = ( RRfld gsum ( ( log |` RR+ ) o. F ) ) )
96 61 a1i 
 |-  ( ph -> RR+ e. ( SubMnd ` M ) )
97 2 96 4 62 gsumsubm 
 |-  ( ph -> ( M gsum F ) = ( ( M |`s RR+ ) gsum F ) )
98 97 fveq2d 
 |-  ( ph -> ( ( log |` RR+ ) ` ( M gsum F ) ) = ( ( log |` RR+ ) ` ( ( M |`s RR+ ) gsum F ) ) )
99 90 95 98 3eqtr4d 
 |-  ( ph -> ( CCfld gsum ( ( log |` RR+ ) o. F ) ) = ( ( log |` RR+ ) ` ( M gsum F ) ) )
100 66 71 2 96 4 89 gsumsubmcl 
 |-  ( ph -> ( M gsum F ) e. RR+ )
101 100 fvresd 
 |-  ( ph -> ( ( log |` RR+ ) ` ( M gsum F ) ) = ( log ` ( M gsum F ) ) )
102 48 99 101 3eqtrd 
 |-  ( ph -> -u ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) = ( log ` ( M gsum F ) ) )
103 102 oveq1d 
 |-  ( ph -> ( -u ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) = ( ( log ` ( M gsum F ) ) / ( # ` A ) ) )
104 100 relogcld 
 |-  ( ph -> ( log ` ( M gsum F ) ) e. RR )
105 104 recnd 
 |-  ( ph -> ( log ` ( M gsum F ) ) e. CC )
106 105 25 26 divrec2d 
 |-  ( ph -> ( ( log ` ( M gsum F ) ) / ( # ` A ) ) = ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) )
107 27 103 106 3eqtrd 
 |-  ( ph -> -u ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) = ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) )
108 37 oveq2d 
 |-  ( ph -> ( CCfld gsum F ) = ( CCfld gsum ( k e. A |-> ( F ` k ) ) ) )
109 13 rpcnd 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. CC )
110 2 109 gsumfsum 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> ( F ` k ) ) ) = sum_ k e. A ( F ` k ) )
111 108 110 eqtrd 
 |-  ( ph -> ( CCfld gsum F ) = sum_ k e. A ( F ` k ) )
112 2 3 13 fsumrpcl 
 |-  ( ph -> sum_ k e. A ( F ` k ) e. RR+ )
113 111 112 eqeltrd 
 |-  ( ph -> ( CCfld gsum F ) e. RR+ )
114 24 nnrpd 
 |-  ( ph -> ( # ` A ) e. RR+ )
115 113 114 rpdivcld 
 |-  ( ph -> ( ( CCfld gsum F ) / ( # ` A ) ) e. RR+ )
116 115 relogcld 
 |-  ( ph -> ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) e. RR )
117 20 24 nndivred 
 |-  ( ph -> ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) e. RR )
118 rpssre 
 |-  RR+ C_ RR
119 118 a1i 
 |-  ( ph -> RR+ C_ RR )
120 relogcl 
 |-  ( w e. RR+ -> ( log ` w ) e. RR )
121 120 adantl 
 |-  ( ( ph /\ w e. RR+ ) -> ( log ` w ) e. RR )
122 121 renegcld 
 |-  ( ( ph /\ w e. RR+ ) -> -u ( log ` w ) e. RR )
123 122 fmpttd 
 |-  ( ph -> ( w e. RR+ |-> -u ( log ` w ) ) : RR+ --> RR )
124 ioorp 
 |-  ( 0 (,) +oo ) = RR+
125 124 eleq2i 
 |-  ( a e. ( 0 (,) +oo ) <-> a e. RR+ )
126 124 eleq2i 
 |-  ( b e. ( 0 (,) +oo ) <-> b e. RR+ )
127 iccssioo2 
 |-  ( ( a e. ( 0 (,) +oo ) /\ b e. ( 0 (,) +oo ) ) -> ( a [,] b ) C_ ( 0 (,) +oo ) )
128 125 126 127 syl2anbr 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> ( a [,] b ) C_ ( 0 (,) +oo ) )
129 128 124 sseqtrdi 
 |-  ( ( a e. RR+ /\ b e. RR+ ) -> ( a [,] b ) C_ RR+ )
130 129 adantl 
 |-  ( ( ph /\ ( a e. RR+ /\ b e. RR+ ) ) -> ( a [,] b ) C_ RR+ )
131 24 nnrecred 
 |-  ( ph -> ( 1 / ( # ` A ) ) e. RR )
132 114 rpreccld 
 |-  ( ph -> ( 1 / ( # ` A ) ) e. RR+ )
133 132 rpge0d 
 |-  ( ph -> 0 <_ ( 1 / ( # ` A ) ) )
134 elrege0 
 |-  ( ( 1 / ( # ` A ) ) e. ( 0 [,) +oo ) <-> ( ( 1 / ( # ` A ) ) e. RR /\ 0 <_ ( 1 / ( # ` A ) ) ) )
135 131 133 134 sylanbrc 
 |-  ( ph -> ( 1 / ( # ` A ) ) e. ( 0 [,) +oo ) )
136 fconst6g 
 |-  ( ( 1 / ( # ` A ) ) e. ( 0 [,) +oo ) -> ( A X. { ( 1 / ( # ` A ) ) } ) : A --> ( 0 [,) +oo ) )
137 135 136 syl 
 |-  ( ph -> ( A X. { ( 1 / ( # ` A ) ) } ) : A --> ( 0 [,) +oo ) )
138 0lt1 
 |-  0 < 1
139 fconstmpt 
 |-  ( A X. { ( 1 / ( # ` A ) ) } ) = ( k e. A |-> ( 1 / ( # ` A ) ) )
140 139 oveq2i 
 |-  ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) = ( CCfld gsum ( k e. A |-> ( 1 / ( # ` A ) ) ) )
141 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
142 6 141 mp1i 
 |-  ( ph -> CCfld e. Mnd )
143 131 recnd 
 |-  ( ph -> ( 1 / ( # ` A ) ) e. CC )
144 eqid 
 |-  ( .g ` CCfld ) = ( .g ` CCfld )
145 53 144 gsumconst 
 |-  ( ( CCfld e. Mnd /\ A e. Fin /\ ( 1 / ( # ` A ) ) e. CC ) -> ( CCfld gsum ( k e. A |-> ( 1 / ( # ` A ) ) ) ) = ( ( # ` A ) ( .g ` CCfld ) ( 1 / ( # ` A ) ) ) )
146 142 2 143 145 syl3anc 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> ( 1 / ( # ` A ) ) ) ) = ( ( # ` A ) ( .g ` CCfld ) ( 1 / ( # ` A ) ) ) )
147 24 nnzd 
 |-  ( ph -> ( # ` A ) e. ZZ )
148 cnfldmulg 
 |-  ( ( ( # ` A ) e. ZZ /\ ( 1 / ( # ` A ) ) e. CC ) -> ( ( # ` A ) ( .g ` CCfld ) ( 1 / ( # ` A ) ) ) = ( ( # ` A ) x. ( 1 / ( # ` A ) ) ) )
149 147 143 148 syl2anc 
 |-  ( ph -> ( ( # ` A ) ( .g ` CCfld ) ( 1 / ( # ` A ) ) ) = ( ( # ` A ) x. ( 1 / ( # ` A ) ) ) )
150 25 26 recidd 
 |-  ( ph -> ( ( # ` A ) x. ( 1 / ( # ` A ) ) ) = 1 )
151 146 149 150 3eqtrd 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> ( 1 / ( # ` A ) ) ) ) = 1 )
152 140 151 eqtrid 
 |-  ( ph -> ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) = 1 )
153 138 152 breqtrrid 
 |-  ( ph -> 0 < ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) )
154 logccv 
 |-  ( ( ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) < ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) )
155 154 3adant1 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) < ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) )
156 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
157 simp3 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> t e. ( 0 (,) 1 ) )
158 156 157 sselid 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> t e. RR )
159 simp21 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> x e. RR+ )
160 159 relogcld 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( log ` x ) e. RR )
161 158 160 remulcld 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( t x. ( log ` x ) ) e. RR )
162 1re 
 |-  1 e. RR
163 resubcl 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 - t ) e. RR )
164 162 158 163 sylancr 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( 1 - t ) e. RR )
165 simp22 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> y e. RR+ )
166 165 relogcld 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( log ` y ) e. RR )
167 164 166 remulcld 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 - t ) x. ( log ` y ) ) e. RR )
168 161 167 readdcld 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) e. RR )
169 simp1 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ph )
170 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
171 170 157 sselid 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> t e. ( 0 [,] 1 ) )
172 119 130 cvxcl 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. RR+ )
173 169 159 165 171 172 syl13anc 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. RR+ )
174 173 relogcld 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. RR )
175 168 174 ltnegd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) < ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <-> -u ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) < -u ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) ) )
176 155 175 mpbid 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> -u ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) < -u ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) )
177 fveq2 
 |-  ( w = ( ( t x. x ) + ( ( 1 - t ) x. y ) ) -> ( log ` w ) = ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) )
178 177 negeqd 
 |-  ( w = ( ( t x. x ) + ( ( 1 - t ) x. y ) ) -> -u ( log ` w ) = -u ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) )
179 eqid 
 |-  ( w e. RR+ |-> -u ( log ` w ) ) = ( w e. RR+ |-> -u ( log ` w ) )
180 negex 
 |-  -u ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. _V
181 178 179 180 fvmpt 
 |-  ( ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. RR+ -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = -u ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) )
182 173 181 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = -u ( log ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) )
183 fveq2 
 |-  ( w = x -> ( log ` w ) = ( log ` x ) )
184 183 negeqd 
 |-  ( w = x -> -u ( log ` w ) = -u ( log ` x ) )
185 negex 
 |-  -u ( log ` x ) e. _V
186 184 179 185 fvmpt 
 |-  ( x e. RR+ -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) = -u ( log ` x ) )
187 159 186 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) = -u ( log ` x ) )
188 187 oveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( t x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) ) = ( t x. -u ( log ` x ) ) )
189 158 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> t e. CC )
190 160 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( log ` x ) e. CC )
191 189 190 mulneg2d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( t x. -u ( log ` x ) ) = -u ( t x. ( log ` x ) ) )
192 188 191 eqtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( t x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) ) = -u ( t x. ( log ` x ) ) )
193 fveq2 
 |-  ( w = y -> ( log ` w ) = ( log ` y ) )
194 193 negeqd 
 |-  ( w = y -> -u ( log ` w ) = -u ( log ` y ) )
195 negex 
 |-  -u ( log ` y ) e. _V
196 194 179 195 fvmpt 
 |-  ( y e. RR+ -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) = -u ( log ` y ) )
197 165 196 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) = -u ( log ` y ) )
198 197 oveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 - t ) x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) ) = ( ( 1 - t ) x. -u ( log ` y ) ) )
199 164 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( 1 - t ) e. CC )
200 166 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( log ` y ) e. CC )
201 199 200 mulneg2d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 - t ) x. -u ( log ` y ) ) = -u ( ( 1 - t ) x. ( log ` y ) ) )
202 198 201 eqtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 - t ) x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) ) = -u ( ( 1 - t ) x. ( log ` y ) ) )
203 192 202 oveq12d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( t x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) ) + ( ( 1 - t ) x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) ) ) = ( -u ( t x. ( log ` x ) ) + -u ( ( 1 - t ) x. ( log ` y ) ) ) )
204 161 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( t x. ( log ` x ) ) e. CC )
205 167 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 - t ) x. ( log ` y ) ) e. CC )
206 204 205 negdid 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> -u ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) = ( -u ( t x. ( log ` x ) ) + -u ( ( 1 - t ) x. ( log ` y ) ) ) )
207 203 206 eqtr4d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( t x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) ) + ( ( 1 - t ) x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) ) ) = -u ( ( t x. ( log ` x ) ) + ( ( 1 - t ) x. ( log ` y ) ) ) )
208 176 182 207 3brtr4d 
 |-  ( ( ph /\ ( x e. RR+ /\ y e. RR+ /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) < ( ( t x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` x ) ) + ( ( 1 - t ) x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` y ) ) ) )
209 119 123 130 208 scvxcvx 
 |-  ( ( ph /\ ( u e. RR+ /\ v e. RR+ /\ s e. ( 0 [,] 1 ) ) ) -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( s x. u ) + ( ( 1 - s ) x. v ) ) ) <_ ( ( s x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` u ) ) + ( ( 1 - s ) x. ( ( w e. RR+ |-> -u ( log ` w ) ) ` v ) ) ) )
210 119 123 130 2 137 4 153 209 jensen 
 |-  ( ph -> ( ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) e. RR+ /\ ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) ) <_ ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) ) )
211 210 simprd 
 |-  ( ph -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) ) <_ ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) )
212 131 adantr 
 |-  ( ( ph /\ k e. A ) -> ( 1 / ( # ` A ) ) e. RR )
213 139 a1i 
 |-  ( ph -> ( A X. { ( 1 / ( # ` A ) ) } ) = ( k e. A |-> ( 1 / ( # ` A ) ) ) )
214 2 212 13 213 37 offval2 
 |-  ( ph -> ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) = ( k e. A |-> ( ( 1 / ( # ` A ) ) x. ( F ` k ) ) ) )
215 214 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) = ( CCfld gsum ( k e. A |-> ( ( 1 / ( # ` A ) ) x. ( F ` k ) ) ) ) )
216 cnfldmul 
 |-  x. = ( .r ` CCfld )
217 6 a1i 
 |-  ( ph -> CCfld e. Ring )
218 109 fmpttd 
 |-  ( ph -> ( k e. A |-> ( F ` k ) ) : A --> CC )
219 218 2 18 fdmfifsupp 
 |-  ( ph -> ( k e. A |-> ( F ` k ) ) finSupp 0 )
220 53 5 216 217 2 143 109 219 gsummulc2 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> ( ( 1 / ( # ` A ) ) x. ( F ` k ) ) ) ) = ( ( 1 / ( # ` A ) ) x. ( CCfld gsum ( k e. A |-> ( F ` k ) ) ) ) )
221 fss 
 |-  ( ( F : A --> RR+ /\ RR+ C_ RR ) -> F : A --> RR )
222 4 118 221 sylancl 
 |-  ( ph -> F : A --> RR )
223 4 2 18 fdmfifsupp 
 |-  ( ph -> F finSupp 0 )
224 5 8 2 12 222 223 gsumsubgcl 
 |-  ( ph -> ( CCfld gsum F ) e. RR )
225 224 recnd 
 |-  ( ph -> ( CCfld gsum F ) e. CC )
226 225 25 26 divrec2d 
 |-  ( ph -> ( ( CCfld gsum F ) / ( # ` A ) ) = ( ( 1 / ( # ` A ) ) x. ( CCfld gsum F ) ) )
227 108 oveq2d 
 |-  ( ph -> ( ( 1 / ( # ` A ) ) x. ( CCfld gsum F ) ) = ( ( 1 / ( # ` A ) ) x. ( CCfld gsum ( k e. A |-> ( F ` k ) ) ) ) )
228 226 227 eqtr2d 
 |-  ( ph -> ( ( 1 / ( # ` A ) ) x. ( CCfld gsum ( k e. A |-> ( F ` k ) ) ) ) = ( ( CCfld gsum F ) / ( # ` A ) ) )
229 215 220 228 3eqtrd 
 |-  ( ph -> ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) = ( ( CCfld gsum F ) / ( # ` A ) ) )
230 229 152 oveq12d 
 |-  ( ph -> ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) = ( ( ( CCfld gsum F ) / ( # ` A ) ) / 1 ) )
231 224 24 nndivred 
 |-  ( ph -> ( ( CCfld gsum F ) / ( # ` A ) ) e. RR )
232 231 recnd 
 |-  ( ph -> ( ( CCfld gsum F ) / ( # ` A ) ) e. CC )
233 232 div1d 
 |-  ( ph -> ( ( ( CCfld gsum F ) / ( # ` A ) ) / 1 ) = ( ( CCfld gsum F ) / ( # ` A ) ) )
234 230 233 eqtrd 
 |-  ( ph -> ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) = ( ( CCfld gsum F ) / ( # ` A ) ) )
235 234 fveq2d 
 |-  ( ph -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) ) = ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
236 fveq2 
 |-  ( w = ( ( CCfld gsum F ) / ( # ` A ) ) -> ( log ` w ) = ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
237 236 negeqd 
 |-  ( w = ( ( CCfld gsum F ) / ( # ` A ) ) -> -u ( log ` w ) = -u ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
238 negex 
 |-  -u ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) e. _V
239 237 179 238 fvmpt 
 |-  ( ( ( CCfld gsum F ) / ( # ` A ) ) e. RR+ -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum F ) / ( # ` A ) ) ) = -u ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
240 115 239 syl 
 |-  ( ph -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum F ) / ( # ` A ) ) ) = -u ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
241 235 240 eqtrd 
 |-  ( ph -> ( ( w e. RR+ |-> -u ( log ` w ) ) ` ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. F ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) ) = -u ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
242 53 5 216 217 2 143 32 19 gsummulc2 
 |-  ( ph -> ( CCfld gsum ( k e. A |-> ( ( 1 / ( # ` A ) ) x. -u ( log ` ( F ` k ) ) ) ) ) = ( ( 1 / ( # ` A ) ) x. ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) ) )
243 negex 
 |-  -u ( log ` ( F ` k ) ) e. _V
244 243 a1i 
 |-  ( ( ph /\ k e. A ) -> -u ( log ` ( F ` k ) ) e. _V )
245 eqidd 
 |-  ( ph -> ( w e. RR+ |-> -u ( log ` w ) ) = ( w e. RR+ |-> -u ( log ` w ) ) )
246 fveq2 
 |-  ( w = ( F ` k ) -> ( log ` w ) = ( log ` ( F ` k ) ) )
247 246 negeqd 
 |-  ( w = ( F ` k ) -> -u ( log ` w ) = -u ( log ` ( F ` k ) ) )
248 13 37 245 247 fmptco 
 |-  ( ph -> ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) = ( k e. A |-> -u ( log ` ( F ` k ) ) ) )
249 2 212 244 213 248 offval2 
 |-  ( ph -> ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) = ( k e. A |-> ( ( 1 / ( # ` A ) ) x. -u ( log ` ( F ` k ) ) ) ) )
250 249 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) ) = ( CCfld gsum ( k e. A |-> ( ( 1 / ( # ` A ) ) x. -u ( log ` ( F ` k ) ) ) ) ) )
251 21 25 26 divrec2d 
 |-  ( ph -> ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) = ( ( 1 / ( # ` A ) ) x. ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) ) )
252 242 250 251 3eqtr4d 
 |-  ( ph -> ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) ) = ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) )
253 252 152 oveq12d 
 |-  ( ph -> ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) = ( ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) / 1 ) )
254 117 recnd 
 |-  ( ph -> ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) e. CC )
255 254 div1d 
 |-  ( ph -> ( ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) / 1 ) = ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) )
256 253 255 eqtrd 
 |-  ( ph -> ( ( CCfld gsum ( ( A X. { ( 1 / ( # ` A ) ) } ) oF x. ( ( w e. RR+ |-> -u ( log ` w ) ) o. F ) ) ) / ( CCfld gsum ( A X. { ( 1 / ( # ` A ) ) } ) ) ) = ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) )
257 211 241 256 3brtr3d 
 |-  ( ph -> -u ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) <_ ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) )
258 116 117 257 lenegcon1d 
 |-  ( ph -> -u ( ( CCfld gsum ( k e. A |-> -u ( log ` ( F ` k ) ) ) ) / ( # ` A ) ) <_ ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
259 107 258 eqbrtrrd 
 |-  ( ph -> ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) <_ ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) )
260 131 104 remulcld 
 |-  ( ph -> ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) e. RR )
261 efle 
 |-  ( ( ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) e. RR /\ ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) e. RR ) -> ( ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) <_ ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) <-> ( exp ` ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) ) <_ ( exp ` ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) ) ) )
262 260 116 261 syl2anc 
 |-  ( ph -> ( ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) <_ ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) <-> ( exp ` ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) ) <_ ( exp ` ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) ) ) )
263 259 262 mpbid 
 |-  ( ph -> ( exp ` ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) ) <_ ( exp ` ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) ) )
264 100 rpcnd 
 |-  ( ph -> ( M gsum F ) e. CC )
265 100 rpne0d 
 |-  ( ph -> ( M gsum F ) =/= 0 )
266 264 265 143 cxpefd 
 |-  ( ph -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) = ( exp ` ( ( 1 / ( # ` A ) ) x. ( log ` ( M gsum F ) ) ) ) )
267 115 reeflogd 
 |-  ( ph -> ( exp ` ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) ) = ( ( CCfld gsum F ) / ( # ` A ) ) )
268 267 eqcomd 
 |-  ( ph -> ( ( CCfld gsum F ) / ( # ` A ) ) = ( exp ` ( log ` ( ( CCfld gsum F ) / ( # ` A ) ) ) ) )
269 263 266 268 3brtr4d 
 |-  ( ph -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )