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 φA+
amgm3d.1 φB+
amgm3d.2 φC+
Assertion amgm3d φABC13A+B+C3

Proof

Step Hyp Ref Expression
1 amgm3d.0 φA+
2 amgm3d.1 φB+
3 amgm3d.2 φC+
4 eqid mulGrpfld=mulGrpfld
5 fzofi 0..^3Fin
6 5 a1i φ0..^3Fin
7 3nn 3
8 lbfzo0 00..^33
9 7 8 mpbir 00..^3
10 ne0i 00..^30..^3
11 9 10 mp1i φ0..^3
12 1 2 3 s3cld φ⟨“ABC”⟩Word+
13 wrdf ⟨“ABC”⟩Word+⟨“ABC”⟩:0..^⟨“ABC”⟩+
14 s3len ⟨“ABC”⟩=3
15 df-3 3=2+1
16 14 15 eqtri ⟨“ABC”⟩=2+1
17 16 oveq2i 0..^⟨“ABC”⟩=0..^2+1
18 17 feq2i ⟨“ABC”⟩:0..^⟨“ABC”⟩+⟨“ABC”⟩:0..^2+1+
19 13 18 sylib ⟨“ABC”⟩Word+⟨“ABC”⟩:0..^2+1+
20 15 oveq2i 0..^3=0..^2+1
21 20 feq2i ⟨“ABC”⟩:0..^3+⟨“ABC”⟩:0..^2+1+
22 19 21 sylibr ⟨“ABC”⟩Word+⟨“ABC”⟩:0..^3+
23 12 22 syl φ⟨“ABC”⟩:0..^3+
24 4 6 11 23 amgmlem φmulGrpfld⟨“ABC”⟩10..^3fld⟨“ABC”⟩0..^3
25 cnring fldRing
26 4 ringmgp fldRingmulGrpfldMnd
27 25 26 mp1i φmulGrpfldMnd
28 1 rpcnd φA
29 2 rpcnd φB
30 3 rpcnd φC
31 28 29 30 jca32 φABC
32 cnfldbas =Basefld
33 4 32 mgpbas =BasemulGrpfld
34 cnfldmul ×=fld
35 4 34 mgpplusg ×=+mulGrpfld
36 33 35 gsumws3 mulGrpfldMndABCmulGrpfld⟨“ABC”⟩=ABC
37 27 31 36 syl2anc φmulGrpfld⟨“ABC”⟩=ABC
38 3nn0 30
39 hashfzo0 300..^3=3
40 38 39 mp1i φ0..^3=3
41 40 oveq2d φ10..^3=13
42 37 41 oveq12d φmulGrpfld⟨“ABC”⟩10..^3=ABC13
43 ringmnd fldRingfldMnd
44 25 43 mp1i φfldMnd
45 cnfldadd +=+fld
46 32 45 gsumws3 fldMndABCfld⟨“ABC”⟩=A+B+C
47 44 31 46 syl2anc φfld⟨“ABC”⟩=A+B+C
48 47 40 oveq12d φfld⟨“ABC”⟩0..^3=A+B+C3
49 24 42 48 3brtr3d φABC13A+B+C3