# Metamath Proof Explorer

## 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 {{A}{B}{C}{D}}^{\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 ℕ$
9 lbfzo0 ${⊢}0\in \left(0..^4\right)↔4\in ℕ$
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 ⟨“{A}{B}{C}{D}”⟩\in \mathrm{Word}{ℝ}^{+}$
14 wrdf ${⊢}⟨“{A}{B}{C}{D}”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“{A}{B}{C}{D}”⟩:\left(0..^\left|⟨“{A}{B}{C}{D}”⟩\right|\right)⟶{ℝ}^{+}$
15 13 14 syl ${⊢}{\phi }\to ⟨“{A}{B}{C}{D}”⟩:\left(0..^\left|⟨“{A}{B}{C}{D}”⟩\right|\right)⟶{ℝ}^{+}$
16 s4len ${⊢}\left|⟨“{A}{B}{C}{D}”⟩\right|=4$
17 16 a1i ${⊢}{\phi }\to \left|⟨“{A}{B}{C}{D}”⟩\right|=4$
18 17 oveq2d ${⊢}{\phi }\to \left(0..^\left|⟨“{A}{B}{C}{D}”⟩\right|\right)=\left(0..^4\right)$
19 18 feq2d ${⊢}{\phi }\to \left(⟨“{A}{B}{C}{D}”⟩:\left(0..^\left|⟨“{A}{B}{C}{D}”⟩\right|\right)⟶{ℝ}^{+}↔⟨“{A}{B}{C}{D}”⟩:\left(0..^4\right)⟶{ℝ}^{+}\right)$
20 15 19 mpbid ${⊢}{\phi }\to ⟨“{A}{B}{C}{D}”⟩:\left(0..^4\right)⟶{ℝ}^{+}$
21 5 7 12 20 amgmlem ${⊢}{\phi }\to {\left({\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}},⟨“{A}{B}{C}{D}”⟩\right)}^{\frac{1}{\left|\left(0..^4\right)\right|}}\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}{C}{D}”⟩}{\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 ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
34 5 33 mgpplusg ${⊢}×={+}_{{\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}}}}⟨“{A}{B}{C}{D}”⟩={A}{B}{C}{D}$
36 24 30 35 syl2anc ${⊢}{\phi }\to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“{A}{B}{C}{D}”⟩={A}{B}{C}{D}$
37 4nn0 ${⊢}4\in {ℕ}_{0}$
38 hashfzo0 ${⊢}4\in {ℕ}_{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}}}},⟨“{A}{B}{C}{D}”⟩\right)}^{\frac{1}{\left|\left(0..^4\right)\right|}}={{A}{B}{C}{D}}^{\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}}}⟨“{A}{B}{C}{D}”⟩={A}+{B}+\left({C}+{D}\right)$
46 43 30 45 syl2anc ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}{C}{D}”⟩={A}+{B}+\left({C}+{D}\right)$
47 46 39 oveq12d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}⟨“{A}{B}{C}{D}”⟩}{\left|\left(0..^4\right)\right|}=\frac{{A}+{B}+\left({C}+{D}\right)}{4}$
48 21 41 47 3brtr3d ${⊢}{\phi }\to {{A}{B}{C}{D}}^{\frac{1}{4}}\le \frac{{A}+{B}+\left({C}+{D}\right)}{4}$