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 𝑀 = ( mulGrp ‘ ℂfld )
Assertion amgm ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 amgm.1 𝑀 = ( mulGrp ‘ ℂfld )
2 cnfldbas ℂ = ( Base ‘ ℂfld )
3 1 2 mgpbas ℂ = ( Base ‘ 𝑀 )
4 cnfld1 1 = ( 1r ‘ ℂfld )
5 1 4 ringidval 1 = ( 0g𝑀 )
6 cnfldmul · = ( .r ‘ ℂfld )
7 1 6 mgpplusg · = ( +g𝑀 )
8 cncrng fld ∈ CRing
9 1 crngmgp ( ℂfld ∈ CRing → 𝑀 ∈ CMnd )
10 8 9 mp1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝑀 ∈ CMnd )
11 simpl1 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐴 ∈ Fin )
12 simpl3 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) )
13 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
14 ax-resscn ℝ ⊆ ℂ
15 13 14 sstri ( 0 [,) +∞ ) ⊆ ℂ
16 fss ( ( 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
17 12 15 16 sylancl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
18 1ex 1 ∈ V
19 18 a1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 1 ∈ V )
20 17 11 19 fdmfifsupp ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐹 finSupp 1 )
21 disjdif ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅
22 21 a1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( { 𝑥 } ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ )
23 undif2 ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) = ( { 𝑥 } ∪ 𝐴 )
24 simprl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝑥𝐴 )
25 24 snssd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → { 𝑥 } ⊆ 𝐴 )
26 ssequn1 ( { 𝑥 } ⊆ 𝐴 ↔ ( { 𝑥 } ∪ 𝐴 ) = 𝐴 )
27 25 26 sylib ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( { 𝑥 } ∪ 𝐴 ) = 𝐴 )
28 23 27 eqtr2id ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐴 = ( { 𝑥 } ∪ ( 𝐴 ∖ { 𝑥 } ) ) )
29 3 5 7 10 11 17 20 22 28 gsumsplit ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝑀 Σg 𝐹 ) = ( ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) )
30 12 25 feqresmpt ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝐹 ↾ { 𝑥 } ) = ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹𝑦 ) ) )
31 30 oveq2d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) = ( 𝑀 Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹𝑦 ) ) ) )
32 cnring fld ∈ Ring
33 1 ringmgp ( ℂfld ∈ Ring → 𝑀 ∈ Mnd )
34 32 33 mp1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝑀 ∈ Mnd )
35 17 24 ffvelrnd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝐹𝑥 ) ∈ ℂ )
36 fveq2 ( 𝑦 = 𝑥 → ( 𝐹𝑦 ) = ( 𝐹𝑥 ) )
37 3 36 gsumsn ( ( 𝑀 ∈ Mnd ∧ 𝑥𝐴 ∧ ( 𝐹𝑥 ) ∈ ℂ ) → ( 𝑀 Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹𝑦 ) ) ) = ( 𝐹𝑥 ) )
38 34 24 35 37 syl3anc ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝐹𝑦 ) ) ) = ( 𝐹𝑥 ) )
39 simprr ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝐹𝑥 ) = 0 )
40 31 38 39 3eqtrd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) = 0 )
41 40 oveq1d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ( 𝑀 Σg ( 𝐹 ↾ { 𝑥 } ) ) · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = ( 0 · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) )
42 diffi ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
43 11 42 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
44 difss ( 𝐴 ∖ { 𝑥 } ) ⊆ 𝐴
45 fssres ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐴 ∖ { 𝑥 } ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) : ( 𝐴 ∖ { 𝑥 } ) ⟶ ℂ )
46 17 44 45 sylancl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) : ( 𝐴 ∖ { 𝑥 } ) ⟶ ℂ )
47 46 43 19 fdmfifsupp ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) finSupp 1 )
48 3 5 10 43 46 47 gsumcl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ∈ ℂ )
49 48 mul02d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 0 · ( 𝑀 Σg ( 𝐹 ↾ ( 𝐴 ∖ { 𝑥 } ) ) ) ) = 0 )
50 29 41 49 3eqtrd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 𝑀 Σg 𝐹 ) = 0 )
51 50 oveq1d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = ( 0 ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) )
52 simpl2 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐴 ≠ ∅ )
53 hashnncl ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
54 11 53 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
55 52 54 mpbird ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
56 55 nncnd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
57 55 nnne0d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ≠ 0 )
58 56 57 reccld ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 1 / ( ♯ ‘ 𝐴 ) ) ∈ ℂ )
59 56 57 recne0d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 1 / ( ♯ ‘ 𝐴 ) ) ≠ 0 )
60 58 59 0cxpd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 0 ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = 0 )
61 51 60 eqtrd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) = 0 )
62 cnfld0 0 = ( 0g ‘ ℂfld )
63 ringcmn ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
64 32 63 mp1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ℂfld ∈ CMnd )
65 rege0subm ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld )
66 65 a1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld ) )
67 c0ex 0 ∈ V
68 67 a1i ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 0 ∈ V )
69 12 11 68 fdmfifsupp ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 𝐹 finSupp 0 )
70 62 64 11 66 12 69 gsumsubmcl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ℂfld Σg 𝐹 ) ∈ ( 0 [,) +∞ ) )
71 elrege0 ( ( ℂfld Σg 𝐹 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ℂfld Σg 𝐹 ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg 𝐹 ) ) )
72 70 71 sylib ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ( ℂfld Σg 𝐹 ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg 𝐹 ) ) )
73 55 nnred ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ )
74 55 nngt0d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 0 < ( ♯ ‘ 𝐴 ) )
75 divge0 ( ( ( ( ℂfld Σg 𝐹 ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg 𝐹 ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ♯ ‘ 𝐴 ) ) ) → 0 ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
76 72 73 74 75 syl12anc ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → 0 ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
77 61 76 eqbrtrd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ( 𝑥𝐴 ∧ ( 𝐹𝑥 ) = 0 ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
78 77 rexlimdvaa ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
79 ralnex ( ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ↔ ¬ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 0 )
80 simpl1 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → 𝐴 ∈ Fin )
81 simpl2 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → 𝐴 ≠ ∅ )
82 simpl3 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) )
83 82 ffnd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → 𝐹 Fn 𝐴 )
84 ffvelrn ( ( 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ( 0 [,) +∞ ) )
85 84 3ad2antl3 ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ( 0 [,) +∞ ) )
86 elrege0 ( ( 𝐹𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑥 ) ) )
87 85 86 sylib ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( ( 𝐹𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑥 ) ) )
88 87 simprd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → 0 ≤ ( 𝐹𝑥 ) )
89 0re 0 ∈ ℝ
90 87 simpld ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ℝ )
91 leloe ( ( 0 ∈ ℝ ∧ ( 𝐹𝑥 ) ∈ ℝ ) → ( 0 ≤ ( 𝐹𝑥 ) ↔ ( 0 < ( 𝐹𝑥 ) ∨ 0 = ( 𝐹𝑥 ) ) ) )
92 89 90 91 sylancr ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( 0 ≤ ( 𝐹𝑥 ) ↔ ( 0 < ( 𝐹𝑥 ) ∨ 0 = ( 𝐹𝑥 ) ) ) )
93 88 92 mpbid ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( 0 < ( 𝐹𝑥 ) ∨ 0 = ( 𝐹𝑥 ) ) )
94 93 ord ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( ¬ 0 < ( 𝐹𝑥 ) → 0 = ( 𝐹𝑥 ) ) )
95 eqcom ( 0 = ( 𝐹𝑥 ) ↔ ( 𝐹𝑥 ) = 0 )
96 94 95 syl6ib ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( ¬ 0 < ( 𝐹𝑥 ) → ( 𝐹𝑥 ) = 0 ) )
97 96 con1d ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( ¬ ( 𝐹𝑥 ) = 0 → 0 < ( 𝐹𝑥 ) ) )
98 elrp ( ( 𝐹𝑥 ) ∈ ℝ+ ↔ ( ( 𝐹𝑥 ) ∈ ℝ ∧ 0 < ( 𝐹𝑥 ) ) )
99 98 baib ( ( 𝐹𝑥 ) ∈ ℝ → ( ( 𝐹𝑥 ) ∈ ℝ+ ↔ 0 < ( 𝐹𝑥 ) ) )
100 90 99 syl ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( ( 𝐹𝑥 ) ∈ ℝ+ ↔ 0 < ( 𝐹𝑥 ) ) )
101 97 100 sylibrd ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ 𝑥𝐴 ) → ( ¬ ( 𝐹𝑥 ) = 0 → ( 𝐹𝑥 ) ∈ ℝ+ ) )
102 101 ralimdva ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 → ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ ℝ+ ) )
103 102 imp ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ ℝ+ )
104 ffnfv ( 𝐹 : 𝐴 ⟶ ℝ+ ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝐹𝑥 ) ∈ ℝ+ ) )
105 83 103 104 sylanbrc ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → 𝐹 : 𝐴 ⟶ ℝ+ )
106 1 80 81 105 amgmlem ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) ∧ ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )
107 106 ex ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ∀ 𝑥𝐴 ¬ ( 𝐹𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
108 79 107 syl5bir ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ¬ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
109 78 108 pm2.61d ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )