Theorem amgm2d

Description: Arithmetic-geometric mean inequality for n = 2 , derived from amgmlem . (Contributed by Stanislas Polu, 8-Sep-2020)

	Ref	Expression
Hypotheses	amgm2d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
	amgm2d.1	$$⊢\phi \to B\in {ℝ}^{+}$$
Assertion	amgm2d	$$⊢\phi \to {AB}^{\frac{1}{2}}\le \frac{A+B}{2}$$

Proof

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