# Metamath Proof Explorer

## Theorem amgm

Description: Inequality of arithmetic and geometric means. Here ( M gsum F ) calculates the group sum within the multiplicative monoid of the complex numbers (or in other words, it multiplies the elements F ( x ) , x e. A together), and ( CCfld gsum F ) calculates the group sum in the additive group (i.e. the sum of the elements). This is Metamath 100 proof #38. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypothesis amgm.1 ${⊢}{M}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$
Assertion amgm ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\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 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
3 1 2 mgpbas ${⊢}ℂ={\mathrm{Base}}_{{M}}$
4 cnfld1 ${⊢}1={1}_{{ℂ}_{\mathrm{fld}}}$
5 1 4 ringidval ${⊢}1={0}_{{M}}$
6 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
7 1 6 mgpplusg ${⊢}×={+}_{{M}}$
8 cncrng ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$
9 1 crngmgp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\to {M}\in \mathrm{CMnd}$
10 8 9 mp1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {M}\in \mathrm{CMnd}$
11 simpl1 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {A}\in \mathrm{Fin}$
12 simpl3 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {F}:{A}⟶\left[0,\mathrm{+\infty }\right)$
13 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
14 ax-resscn ${⊢}ℝ\subseteq ℂ$
15 13 14 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
16 fss ${⊢}\left({F}:{A}⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq ℂ\right)\to {F}:{A}⟶ℂ$
17 12 15 16 sylancl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {F}:{A}⟶ℂ$
18 1ex ${⊢}1\in \mathrm{V}$
19 18 a1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to 1\in \mathrm{V}$
20 17 11 19 fdmfifsupp ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {finSupp}_{1}\left({F}\right)$
21 disjdif ${⊢}\left\{{x}\right\}\cap \left({A}\setminus \left\{{x}\right\}\right)=\varnothing$
22 21 a1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left\{{x}\right\}\cap \left({A}\setminus \left\{{x}\right\}\right)=\varnothing$
23 undif2 ${⊢}\left\{{x}\right\}\cup \left({A}\setminus \left\{{x}\right\}\right)=\left\{{x}\right\}\cup {A}$
24 simprl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {x}\in {A}$
25 24 snssd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left\{{x}\right\}\subseteq {A}$
26 ssequn1 ${⊢}\left\{{x}\right\}\subseteq {A}↔\left\{{x}\right\}\cup {A}={A}$
27 25 26 sylib ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left\{{x}\right\}\cup {A}={A}$
28 23 27 syl5req ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {A}=\left\{{x}\right\}\cup \left({A}\setminus \left\{{x}\right\}\right)$
29 3 5 7 10 11 17 20 22 28 gsumsplit ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\sum }_{{M}}{F}=\left({\sum }_{{M}},\left({{F}↾}_{\left\{{x}\right\}}\right)\right)\left({\sum }_{{M}},\left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right)\right)$
30 12 25 feqresmpt ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {{F}↾}_{\left\{{x}\right\}}=\left({y}\in \left\{{x}\right\}⟼{F}\left({y}\right)\right)$
31 30 oveq2d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\sum }_{{M}}\left({{F}↾}_{\left\{{x}\right\}}\right)=\underset{{y}\in \left\{{x}\right\}}{{\sum }_{{M}}}{F}\left({y}\right)$
32 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
33 1 ringmgp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {M}\in \mathrm{Mnd}$
34 32 33 mp1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {M}\in \mathrm{Mnd}$
35 17 24 ffvelrnd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {F}\left({x}\right)\in ℂ$
36 fveq2 ${⊢}{y}={x}\to {F}\left({y}\right)={F}\left({x}\right)$
37 3 36 gsumsn ${⊢}\left({M}\in \mathrm{Mnd}\wedge {x}\in {A}\wedge {F}\left({x}\right)\in ℂ\right)\to \underset{{y}\in \left\{{x}\right\}}{{\sum }_{{M}}}{F}\left({y}\right)={F}\left({x}\right)$
38 34 24 35 37 syl3anc ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \underset{{y}\in \left\{{x}\right\}}{{\sum }_{{M}}}{F}\left({y}\right)={F}\left({x}\right)$
39 simprr ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {F}\left({x}\right)=0$
40 31 38 39 3eqtrd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\sum }_{{M}}\left({{F}↾}_{\left\{{x}\right\}}\right)=0$
41 40 oveq1d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left({\sum }_{{M}},\left({{F}↾}_{\left\{{x}\right\}}\right)\right)\left({\sum }_{{M}},\left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right)\right)=0\cdot \left({\sum }_{{M}},\left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right)\right)$
42 diffi ${⊢}{A}\in \mathrm{Fin}\to {A}\setminus \left\{{x}\right\}\in \mathrm{Fin}$
43 11 42 syl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {A}\setminus \left\{{x}\right\}\in \mathrm{Fin}$
44 difss ${⊢}{A}\setminus \left\{{x}\right\}\subseteq {A}$
45 fssres ${⊢}\left({F}:{A}⟶ℂ\wedge {A}\setminus \left\{{x}\right\}\subseteq {A}\right)\to \left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right):{A}\setminus \left\{{x}\right\}⟶ℂ$
46 17 44 45 sylancl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right):{A}\setminus \left\{{x}\right\}⟶ℂ$
47 46 43 19 fdmfifsupp ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {finSupp}_{1}\left(\left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right)\right)$
48 3 5 10 43 46 47 gsumcl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\sum }_{{M}}\left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right)\in ℂ$
49 48 mul02d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to 0\cdot \left({\sum }_{{M}},\left({{F}↾}_{\left({A}\setminus \left\{{x}\right\}\right)}\right)\right)=0$
50 29 41 49 3eqtrd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\sum }_{{M}}{F}=0$
51 50 oveq1d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}={0}^{\frac{1}{\left|{A}\right|}}$
52 simpl2 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {A}\ne \varnothing$
53 hashnncl ${⊢}{A}\in \mathrm{Fin}\to \left(\left|{A}\right|\in ℕ↔{A}\ne \varnothing \right)$
54 11 53 syl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left(\left|{A}\right|\in ℕ↔{A}\ne \varnothing \right)$
55 52 54 mpbird ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left|{A}\right|\in ℕ$
56 55 nncnd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left|{A}\right|\in ℂ$
57 55 nnne0d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left|{A}\right|\ne 0$
58 56 57 reccld ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \frac{1}{\left|{A}\right|}\in ℂ$
59 56 57 recne0d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \frac{1}{\left|{A}\right|}\ne 0$
60 58 59 0cxpd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {0}^{\frac{1}{\left|{A}\right|}}=0$
61 51 60 eqtrd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}=0$
62 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
63 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
64 32 63 mp1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
65 rege0subm ${⊢}\left[0,\mathrm{+\infty }\right)\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$
66 65 a1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left[0,\mathrm{+\infty }\right)\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$
67 c0ex ${⊢}0\in \mathrm{V}$
68 67 a1i ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to 0\in \mathrm{V}$
69 12 11 68 fdmfifsupp ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {finSupp}_{0}\left({F}\right)$
70 62 64 11 66 12 69 gsumsubmcl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}{F}\in \left[0,\mathrm{+\infty }\right)$
71 elrege0 ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}{F}\in \left[0,\mathrm{+\infty }\right)↔\left({\sum }_{{ℂ}_{\mathrm{fld}}}{F}\in ℝ\wedge 0\le {\sum }_{{ℂ}_{\mathrm{fld}}}{F}\right)$
72 70 71 sylib ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left({\sum }_{{ℂ}_{\mathrm{fld}}}{F}\in ℝ\wedge 0\le {\sum }_{{ℂ}_{\mathrm{fld}}}{F}\right)$
73 55 nnred ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to \left|{A}\right|\in ℝ$
74 55 nngt0d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to 0<\left|{A}\right|$
75 divge0 ${⊢}\left(\left({\sum }_{{ℂ}_{\mathrm{fld}}}{F}\in ℝ\wedge 0\le {\sum }_{{ℂ}_{\mathrm{fld}}}{F}\right)\wedge \left(\left|{A}\right|\in ℝ\wedge 0<\left|{A}\right|\right)\right)\to 0\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}$
76 72 73 74 75 syl12anc ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to 0\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}$
77 61 76 eqbrtrd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \left({x}\in {A}\wedge {F}\left({x}\right)=0\right)\right)\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}$
78 77 rexlimdvaa ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)=0\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}\right)$
79 ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)=0$
80 simpl1 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to {A}\in \mathrm{Fin}$
81 simpl2 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to {A}\ne \varnothing$
82 simpl3 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to {F}:{A}⟶\left[0,\mathrm{+\infty }\right)$
83 82 ffnd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to {F}Fn{A}$
84 ffvelrn ${⊢}\left({F}:{A}⟶\left[0,\mathrm{+\infty }\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
85 84 3ad2antl3 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
86 elrege0 ${⊢}{F}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({F}\left({x}\right)\in ℝ\wedge 0\le {F}\left({x}\right)\right)$
87 85 86 sylib ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)\in ℝ\wedge 0\le {F}\left({x}\right)\right)$
88 87 simprd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to 0\le {F}\left({x}\right)$
89 0re ${⊢}0\in ℝ$
90 87 simpld ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in ℝ$
91 leloe ${⊢}\left(0\in ℝ\wedge {F}\left({x}\right)\in ℝ\right)\to \left(0\le {F}\left({x}\right)↔\left(0<{F}\left({x}\right)\vee 0={F}\left({x}\right)\right)\right)$
92 89 90 91 sylancr ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left(0\le {F}\left({x}\right)↔\left(0<{F}\left({x}\right)\vee 0={F}\left({x}\right)\right)\right)$
93 88 92 mpbid ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left(0<{F}\left({x}\right)\vee 0={F}\left({x}\right)\right)$
94 93 ord ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left(¬0<{F}\left({x}\right)\to 0={F}\left({x}\right)\right)$
95 eqcom ${⊢}0={F}\left({x}\right)↔{F}\left({x}\right)=0$
96 94 95 syl6ib ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left(¬0<{F}\left({x}\right)\to {F}\left({x}\right)=0\right)$
97 96 con1d ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left(¬{F}\left({x}\right)=0\to 0<{F}\left({x}\right)\right)$
98 elrp ${⊢}{F}\left({x}\right)\in {ℝ}^{+}↔\left({F}\left({x}\right)\in ℝ\wedge 0<{F}\left({x}\right)\right)$
99 98 baib ${⊢}{F}\left({x}\right)\in ℝ\to \left({F}\left({x}\right)\in {ℝ}^{+}↔0<{F}\left({x}\right)\right)$
100 90 99 syl ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)\in {ℝ}^{+}↔0<{F}\left({x}\right)\right)$
101 97 100 sylibrd ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge {x}\in {A}\right)\to \left(¬{F}\left({x}\right)=0\to {F}\left({x}\right)\in {ℝ}^{+}\right)$
102 101 ralimdva ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {ℝ}^{+}\right)$
103 102 imp ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {ℝ}^{+}$
104 ffnfv ${⊢}{F}:{A}⟶{ℝ}^{+}↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {ℝ}^{+}\right)$
105 83 103 104 sylanbrc ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to {F}:{A}⟶{ℝ}^{+}$
106 1 80 81 105 amgmlem ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\right)\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}$
107 106 ex ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)=0\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}\right)$
108 79 107 syl5bir ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\to \left(¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)=0\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}\right)$
109 78 108 pm2.61d ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \wedge {F}:{A}⟶\left[0,\mathrm{+\infty }\right)\right)\to {\left({\sum }_{{M}},{F}\right)}^{\frac{1}{\left|{A}\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}{F}}{\left|{A}\right|}$