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 = {mulGrp}_{ℂ_{fld}}$
	Assertion	amgm	$⊢ (A \in Fin \land A \neq \emptyset \land F : A ⟶ [0, +∞)) \to {(\sum_{M}, F)}^{\frac{1}{\|A\|}} \leq \frac{\sum_{ℂ_{fld}} F}{\|A\|}$

Proof

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

Metamath Proof Explorer

Theorem amgm

Proof