Theorem amgm4d

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

	Ref	Expression
Hypotheses	amgm4d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
	amgm4d.1	$$⊢\phi \to B\in {ℝ}^{+}$$
	amgm4d.2	$$⊢\phi \to C\in {ℝ}^{+}$$
	amgm4d.3	$$⊢\phi \to D\in {ℝ}^{+}$$
Assertion	amgm4d	$$⊢\phi \to {ABCD}^{\frac{1}{4}}\le \frac{A+B+\left(C+D\right)}{4}$$

Proof

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