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 = ( 1_r ‘ ℂ_fld )
5	1 4	ringidval	⊢ 1 = ( 0_g ‘ 𝑀 )
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 = ( 0_g ‘ ℂ_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 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem amgm

Proof