# Metamath Proof Explorer

## 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 {{A}{B}{C}}^{\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 ℕ$
8 lbfzo0 ${⊢}0\in \left(0..^3\right)↔3\in ℕ$
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 ⟨“{A}{B}{C}”⟩\in \mathrm{Word}{ℝ}^{+}$
13 wrdf ${⊢}⟨“{A}{B}{C}”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“{A}{B}{C}”⟩:\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)⟶{ℝ}^{+}$
14 s3len ${⊢}\left|⟨“{A}{B}{C}”⟩\right|=3$
15 df-3 ${⊢}3=2+1$
16 14 15 eqtri ${⊢}\left|⟨“{A}{B}{C}”⟩\right|=2+1$
17 16 oveq2i ${⊢}\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)=\left(0..^2+1\right)$
18 17 feq2i ${⊢}⟨“{A}{B}{C}”⟩:\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)⟶{ℝ}^{+}↔⟨“{A}{B}{C}”⟩:\left(0..^2+1\right)⟶{ℝ}^{+}$
19 13 18 sylib ${⊢}⟨“{A}{B}{C}”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“{A}{B}{C}”⟩:\left(0..^2+1\right)⟶{ℝ}^{+}$
20 15 oveq2i ${⊢}\left(0..^3\right)=\left(0..^2+1\right)$
21 20 feq2i ${⊢}⟨“{A}{B}{C}”⟩:\left(0..^3\right)⟶{ℝ}^{+}↔⟨“{A}{B}{C}”⟩:\left(0..^2+1\right)⟶{ℝ}^{+}$
22 19 21 sylibr ${⊢}⟨“{A}{B}{C}”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“{A}{B}{C}”⟩:\left(0..^3\right)⟶{ℝ}^{+}$
23 12 22 syl ${⊢}{\phi }\to ⟨“{A}{B}{C}”⟩:\left(0..^3\right)⟶{ℝ}^{+}$
24 4 6 11 23 amgmlem ${⊢}{\phi }\to {\left({\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}},⟨“{A}{B}{C}”⟩\right)}^{\frac{1}{\left|\left(0..^3\right)\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}{C}”⟩}{\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 ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
35 4 34 mgpplusg ${⊢}×={+}_{{\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}}}}⟨“{A}{B}{C}”⟩={A}{B}{C}$
37 27 31 36 syl2anc ${⊢}{\phi }\to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“{A}{B}{C}”⟩={A}{B}{C}$
38 3nn0 ${⊢}3\in {ℕ}_{0}$
39 hashfzo0 ${⊢}3\in {ℕ}_{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}}}},⟨“{A}{B}{C}”⟩\right)}^{\frac{1}{\left|\left(0..^3\right)\right|}}={{A}{B}{C}}^{\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}}}⟨“{A}{B}{C}”⟩={A}+{B}+{C}$
47 44 31 46 syl2anc ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}{C}”⟩={A}+{B}+{C}$
48 47 40 oveq12d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}{C}”⟩}{\left|\left(0..^3\right)\right|}=\frac{{A}+{B}+{C}}{3}$
49 24 42 48 3brtr3d ${⊢}{\phi }\to {{A}{B}{C}}^{\frac{1}{3}}\le \frac{{A}+{B}+{C}}{3}$