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 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ 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 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 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 imbitrdi ⊢ ( ( ( 𝐴 ∈ 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 biimtrrid ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ¬ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 0 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) ) )
109 78 108 pm2.61d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹 : 𝐴 ⟶ ( 0 [,) +∞ ) ) → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )