# Metamath Proof Explorer

## 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 {{A}{B}}^{\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 ℕ$
7 lbfzo0 ${⊢}0\in \left(0..^2\right)↔2\in ℕ$
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 ⟨“{A}{B}”⟩\in \mathrm{Word}{ℝ}^{+}$
12 wrdf ${⊢}⟨“{A}{B}”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“{A}{B}”⟩:\left(0..^\left|⟨“{A}{B}”⟩\right|\right)⟶{ℝ}^{+}$
13 s2len ${⊢}\left|⟨“{A}{B}”⟩\right|=2$
14 13 eqcomi ${⊢}2=\left|⟨“{A}{B}”⟩\right|$
15 14 oveq2i ${⊢}\left(0..^2\right)=\left(0..^\left|⟨“{A}{B}”⟩\right|\right)$
16 15 feq2i ${⊢}⟨“{A}{B}”⟩:\left(0..^2\right)⟶{ℝ}^{+}↔⟨“{A}{B}”⟩:\left(0..^\left|⟨“{A}{B}”⟩\right|\right)⟶{ℝ}^{+}$
17 12 16 sylibr ${⊢}⟨“{A}{B}”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“{A}{B}”⟩:\left(0..^2\right)⟶{ℝ}^{+}$
18 11 17 syl ${⊢}{\phi }\to ⟨“{A}{B}”⟩:\left(0..^2\right)⟶{ℝ}^{+}$
19 3 5 10 18 amgmlem ${⊢}{\phi }\to {\left({\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}},⟨“{A}{B}”⟩\right)}^{\frac{1}{\left|\left(0..^2\right)\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}”⟩}{\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 ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
28 3 27 mgpplusg ${⊢}×={+}_{{\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}}}}⟨“{A}{B}”⟩={A}{B}$
30 22 23 24 29 syl3anc ${⊢}{\phi }\to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“{A}{B}”⟩={A}{B}$
31 2nn0 ${⊢}2\in {ℕ}_{0}$
32 hashfzo0 ${⊢}2\in {ℕ}_{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}}}},⟨“{A}{B}”⟩\right)}^{\frac{1}{\left|\left(0..^2\right)\right|}}={{A}{B}}^{\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}}}⟨“{A}{B}”⟩={A}+{B}$
40 37 23 24 39 syl3anc ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}”⟩={A}+{B}$
41 40 33 oveq12d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}”⟩}{\left|\left(0..^2\right)\right|}=\frac{{A}+{B}}{2}$
42 19 35 41 3brtr3d ${⊢}{\phi }\to {{A}{B}}^{\frac{1}{2}}\le \frac{{A}+{B}}{2}$