Metamath Proof Explorer


Theorem amgm2d

Description: Arithmetic-geometric mean inequality for n = 2 , derived from amgmlem . (Contributed by Stanislas Polu, 8-Sep-2020)

Ref Expression
Hypotheses amgm2d.0 ( 𝜑𝐴 ∈ ℝ+ )
amgm2d.1 ( 𝜑𝐵 ∈ ℝ+ )
Assertion amgm2d ( 𝜑 → ( ( 𝐴 · 𝐵 ) ↑𝑐 ( 1 / 2 ) ) ≤ ( ( 𝐴 + 𝐵 ) / 2 ) )

Proof

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