# Metamath Proof Explorer

## Theorem amgmlem

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

Ref Expression
Hypotheses amgm.1 ${⊢}{M}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$
amgm.2 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
amgm.3 ${⊢}{\phi }\to {A}\ne \varnothing$
amgm.4 ${⊢}{\phi }\to {F}:{A}⟶{ℝ}^{+}$
Assertion amgmlem ${⊢}{\phi }\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}$

### Proof

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