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 φ A +
amgm4d.1 φ B +
amgm4d.2 φ C +
amgm4d.3 φ D +
Assertion amgm4d φ A B C D 1 4 A + B + C + D 4

Proof

Step Hyp Ref Expression
1 amgm4d.0 φ A +
2 amgm4d.1 φ B +
3 amgm4d.2 φ C +
4 amgm4d.3 φ D +
5 eqid mulGrp fld = mulGrp fld
6 fzofi 0 ..^ 4 Fin
7 6 a1i φ 0 ..^ 4 Fin
8 4nn 4
9 lbfzo0 0 0 ..^ 4 4
10 8 9 mpbir 0 0 ..^ 4
11 ne0i 0 0 ..^ 4 0 ..^ 4
12 10 11 mp1i φ 0 ..^ 4
13 1 2 3 4 s4cld φ ⟨“ ABCD ”⟩ Word +
14 wrdf ⟨“ ABCD ”⟩ Word + ⟨“ ABCD ”⟩ : 0 ..^ ⟨“ ABCD ”⟩ +
15 13 14 syl φ ⟨“ ABCD ”⟩ : 0 ..^ ⟨“ ABCD ”⟩ +
16 s4len ⟨“ ABCD ”⟩ = 4
17 16 a1i φ ⟨“ ABCD ”⟩ = 4
18 17 oveq2d φ 0 ..^ ⟨“ ABCD ”⟩ = 0 ..^ 4
19 18 feq2d φ ⟨“ ABCD ”⟩ : 0 ..^ ⟨“ ABCD ”⟩ + ⟨“ ABCD ”⟩ : 0 ..^ 4 +
20 15 19 mpbid φ ⟨“ ABCD ”⟩ : 0 ..^ 4 +
21 5 7 12 20 amgmlem φ mulGrp fld ⟨“ ABCD ”⟩ 1 0 ..^ 4 fld ⟨“ ABCD ”⟩ 0 ..^ 4
22 cnring fld Ring
23 5 ringmgp fld Ring mulGrp fld Mnd
24 22 23 mp1i φ mulGrp fld Mnd
25 1 rpcnd φ A
26 2 rpcnd φ B
27 3 rpcnd φ C
28 4 rpcnd φ D
29 27 28 jca φ C D
30 25 26 29 jca32 φ A B C D
31 cnfldbas = Base fld
32 5 31 mgpbas = Base mulGrp fld
33 cnfldmul × = fld
34 5 33 mgpplusg × = + mulGrp fld
35 32 34 gsumws4 mulGrp fld Mnd A B C D mulGrp fld ⟨“ ABCD ”⟩ = A B C D
36 24 30 35 syl2anc φ mulGrp fld ⟨“ ABCD ”⟩ = A B C D
37 4nn0 4 0
38 hashfzo0 4 0 0 ..^ 4 = 4
39 37 38 mp1i φ 0 ..^ 4 = 4
40 39 oveq2d φ 1 0 ..^ 4 = 1 4
41 36 40 oveq12d φ mulGrp fld ⟨“ ABCD ”⟩ 1 0 ..^ 4 = A B C D 1 4
42 ringmnd fld Ring fld Mnd
43 22 42 mp1i φ fld Mnd
44 cnfldadd + = + fld
45 31 44 gsumws4 fld Mnd A B C D fld ⟨“ ABCD ”⟩ = A + B + C + D
46 43 30 45 syl2anc φ fld ⟨“ ABCD ”⟩ = A + B + C + D
47 46 39 oveq12d φ fld ⟨“ ABCD ”⟩ 0 ..^ 4 = A + B + C + D 4
48 21 41 47 3brtr3d φ A B C D 1 4 A + B + C + D 4