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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
amgm3d.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
amgm3d.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion amgm3d ( 𝜑 → ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) ↑𝑐 ( 1 / 3 ) ) ≤ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) / 3 ) )

Proof

Step Hyp Ref Expression
1 amgm3d.0 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 amgm3d.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3 amgm3d.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
5 fzofi ⊢ ( 0 ..^ 3 ) ∈ Fin
6 5 a1i ⊢ ( 𝜑 → ( 0 ..^ 3 ) ∈ Fin )
7 3nn ⊢ 3 ∈ ℕ
8 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 3 ) ↔ 3 ∈ ℕ )
9 7 8 mpbir ⊢ 0 ∈ ( 0 ..^ 3 )
10 ne0i ⊢ ( 0 ∈ ( 0 ..^ 3 ) → ( 0 ..^ 3 ) ≠ ∅ )
11 9 10 mp1i ⊢ ( 𝜑 → ( 0 ..^ 3 ) ≠ ∅ )
12 1 2 3 s3cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ )
13 wrdf ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ ℝ+ )
14 s3len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
15 df-3 ⊢ 3 = ( 2 + 1 )
16 14 15 eqtri ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 2 + 1 )
17 16 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = ( 0 ..^ ( 2 + 1 ) )
18 17 feq2i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ⟶ ℝ+ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( 2 + 1 ) ) ⟶ ℝ+ )
19 13 18 sylib ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( 2 + 1 ) ) ⟶ ℝ+ )
20 15 oveq2i ⊢ ( 0 ..^ 3 ) = ( 0 ..^ ( 2 + 1 ) )
21 20 feq2i ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ ℝ+ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ ( 2 + 1 ) ) ⟶ ℝ+ )
22 19 21 sylibr ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ ℝ+ )
23 12 22 syl ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ : ( 0 ..^ 3 ) ⟶ ℝ+ )
24 4 6 11 23 amgmlem ⊢ ( 𝜑 → ( ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ↑𝑐 ( 1 / ( ♯ ‘ ( 0 ..^ 3 ) ) ) ) ≤ ( ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) / ( ♯ ‘ ( 0 ..^ 3 ) ) ) )
25 cnring ⊢ ℂfld ∈ Ring
26 4 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
27 25 26 mp1i ⊢ ( 𝜑 → ( mulGrp ‘ ℂfld ) ∈ Mnd )
28 1 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
29 2 rpcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
30 3 rpcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
31 28 29 30 jca32 ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) )
32 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
33 4 32 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
34 cnfldmul ⊢ · = ( .r ‘ ℂfld )
35 4 34 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
36 33 35 gsumws3 ⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) ) → ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )
37 27 31 36 syl2anc ⊢ ( 𝜑 → ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )
38 3nn0 ⊢ 3 ∈ ℕ0
39 hashfzo0 ⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
40 38 39 mp1i ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
41 40 oveq2d ⊢ ( 𝜑 → ( 1 / ( ♯ ‘ ( 0 ..^ 3 ) ) ) = ( 1 / 3 ) )
42 37 41 oveq12d ⊢ ( 𝜑 → ( ( ( mulGrp ‘ ℂfld ) Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ↑𝑐 ( 1 / ( ♯ ‘ ( 0 ..^ 3 ) ) ) ) = ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) ↑𝑐 ( 1 / 3 ) ) )
43 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
44 25 43 mp1i ⊢ ( 𝜑 → ℂfld ∈ Mnd )
45 cnfldadd ⊢ + = ( +g ‘ ℂfld )
46 32 45 gsumws3 ⊢ ( ( ℂfld ∈ Mnd ∧ ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) ) → ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )
47 44 31 46 syl2anc ⊢ ( 𝜑 → ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 𝐴 + ( 𝐵 + 𝐶 ) ) )
48 47 40 oveq12d ⊢ ( 𝜑 → ( ( ℂfld Σg ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) / ( ♯ ‘ ( 0 ..^ 3 ) ) ) = ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) / 3 ) )
49 24 42 48 3brtr3d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝐵 · 𝐶 ) ) ↑𝑐 ( 1 / 3 ) ) ≤ ( ( 𝐴 + ( 𝐵 + 𝐶 ) ) / 3 ) )