Theorem amgm3d

Description: Arithmetic-geometric mean inequality for n = 3 . (Contributed by Stanislas Polu, 11-Sep-2020)

	Ref	Expression
Hypotheses	amgm3d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
	amgm3d.1	$$⊢\phi \to B\in {ℝ}^{+}$$
	amgm3d.2	$$⊢\phi \to C\in {ℝ}^{+}$$
Assertion	amgm3d	$$⊢\phi \to {ABC}^{\frac{1}{3}}\le \frac{A+B+C}{3}$$

Proof

Step	Hyp	Ref	Expression
1		amgm3d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
2		amgm3d.1	$$⊢\phi \to B\in {ℝ}^{+}$$
3		amgm3d.2	$$⊢\phi \to C\in {ℝ}^{+}$$
4		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
5		fzofi	$$⊢\left(0..^3\right)\in \mathrm{Fin}$$
6	5	a1i	$$⊢\phi \to \left(0..^3\right)\in \mathrm{Fin}$$
7		3nn	$$⊢3\in \mathbb{N}$$
8		lbfzo0	$$⊢0\in \left(0..^3\right)\leftrightarrow 3\in \mathbb{N}$$
9	7 8	mpbir	$$⊢0\in \left(0..^3\right)$$
10		ne0i	$$⊢0\in \left(0..^3\right)\to \left(0..^3\right)\ne \varnothing$$
11	9 10	mp1i	$$⊢\phi \to \left(0..^3\right)\ne \varnothing$$
12	1 2 3	s3cld	$$⊢\phi \to ⟨“ABC”⟩\in \mathrm{Word}{ℝ}^{+}$$
13		wrdf	$$⊢⟨“ABC”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“ABC”⟩:\left(0..^\left|⟨“ABC”⟩\right|\right)⟶{ℝ}^{+}$$
14		s3len	$$⊢\left|⟨“ABC”⟩\right|=3$$
15		df-3	$$⊢3=2+1$$
16	14 15	eqtri	$$⊢\left|⟨“ABC”⟩\right|=2+1$$
17	16	oveq2i	$$⊢\left(0..^\left|⟨“ABC”⟩\right|\right)=\left(0..^2+1\right)$$
18	17	feq2i	$$⊢⟨“ABC”⟩:\left(0..^\left|⟨“ABC”⟩\right|\right)⟶{ℝ}^{+}\leftrightarrow ⟨“ABC”⟩:\left(0..^2+1\right)⟶{ℝ}^{+}$$
19	13 18	sylib	$$⊢⟨“ABC”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“ABC”⟩:\left(0..^2+1\right)⟶{ℝ}^{+}$$
20	15	oveq2i	$$⊢\left(0..^3\right)=\left(0..^2+1\right)$$
21	20	feq2i	$$⊢⟨“ABC”⟩:\left(0..^3\right)⟶{ℝ}^{+}\leftrightarrow ⟨“ABC”⟩:\left(0..^2+1\right)⟶{ℝ}^{+}$$
22	19 21	sylibr	$$⊢⟨“ABC”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“ABC”⟩:\left(0..^3\right)⟶{ℝ}^{+}$$
23	12 22	syl	$$⊢\phi \to ⟨“ABC”⟩:\left(0..^3\right)⟶{ℝ}^{+}$$
24	4 6 11 23	amgmlem	$$⊢\phi \to {\left({\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}},⟨“ABC”⟩\right)}^{\frac{1}{\left|\left(0..^3\right)\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“ABC”⟩}{\left|\left(0..^3\right)\right|}$$
25		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
26	4	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
27	25 26	mp1i	$$⊢\phi \to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
28	1	rpcnd	$$⊢\phi \to A\in ℂ$$
29	2	rpcnd	$$⊢\phi \to B\in ℂ$$
30	3	rpcnd	$$⊢\phi \to C\in ℂ$$
31	28 29 30	jca32	$$⊢\phi \to \left(A\in ℂ\wedge \left(B\in ℂ\wedge C\in ℂ\right)\right)$$
32		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
33	4 32	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
34		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
35	4 34	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
36	33 35	gsumws3	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge \left(A\in ℂ\wedge \left(B\in ℂ\wedge C\in ℂ\right)\right)\right)\to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“ABC”⟩=ABC$$
37	27 31 36	syl2anc	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“ABC”⟩=ABC$$
38		3nn0	$$⊢3\in {\mathbb{N}}_0$$
39		hashfzo0	$$⊢3\in {\mathbb{N}}_0\to \left|\left(0..^3\right)\right|=3$$
40	38 39	mp1i	$$⊢\phi \to \left|\left(0..^3\right)\right|=3$$
41	40	oveq2d	$$⊢\phi \to \frac{1}{\left|\left(0..^3\right)\right|}=\frac{1}{3}$$
42	37 41	oveq12d	$$⊢\phi \to {\left({\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}},⟨“ABC”⟩\right)}^{\frac{1}{\left|\left(0..^3\right)\right|}}={ABC}^{\frac{1}{3}}$$
43		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
44	25 43	mp1i	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
45		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
46	32 45	gsumws3	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge \left(A\in ℂ\wedge \left(B\in ℂ\wedge C\in ℂ\right)\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“ABC”⟩=A+B+C$$
47	44 31 46	syl2anc	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“ABC”⟩=A+B+C$$
48	47 40	oveq12d	$$⊢\phi \to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“ABC”⟩}{\left|\left(0..^3\right)\right|}=\frac{A+B+C}{3}$$
49	24 42 48	3brtr3d	$$⊢\phi \to {ABC}^{\frac{1}{3}}\le \frac{A+B+C}{3}$$