Metamath Proof Explorer

Theorem amgmw2d

Description: Weighted arithmetic-geometric mean inequality for n = 2 (compare amgm2d ). (Contributed by Kunhao Zheng, 20-Jun-2021)

Ref Expression
Hypotheses amgmw2d.0 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
amgmw2d.1 ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
amgmw2d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
amgmw2d.3 ⊢ ( 𝜑 → 𝑄 ∈ ℝ+ )
amgmw2d.4 ⊢ ( 𝜑 → ( 𝑃 + 𝑄 ) = 1 )
Assertion amgmw2d ( 𝜑 → ( ( 𝐴 ↑𝑐 𝑃 ) · ( 𝐵 ↑𝑐 𝑄 ) ) ≤ ( ( 𝐴 · 𝑃 ) + ( 𝐵 · 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 amgmw2d.0 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 amgmw2d.1 ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
3 amgmw2d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 amgmw2d.3 ⊢ ( 𝜑 → 𝑄 ∈ ℝ+ )
5 amgmw2d.4 ⊢ ( 𝜑 → ( 𝑃 + 𝑄 ) = 1 )
6 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
7 fzofi ⊢ ( 0 ..^ 2 ) ∈ Fin
8 7 a1i ⊢ ( 𝜑 → ( 0 ..^ 2 ) ∈ Fin )
9 2nn ⊢ 2 ∈ ℕ
10 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ )
11 9 10 mpbir ⊢ 0 ∈ ( 0 ..^ 2 )
12 ne0i ⊢ ( 0 ∈ ( 0 ..^ 2 ) → ( 0 ..^ 2 ) ≠ ∅ )
13 11 12 mp1i ⊢ ( 𝜑 → ( 0 ..^ 2 ) ≠ ∅ )
14 1 3 s2cld ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ ∈ Word ℝ+ )
15 wrdf ⊢ ( ⟨“ 𝐴 𝐵 ”⟩ ∈ Word ℝ+ → ⟨“ 𝐴 𝐵 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ⟶ ℝ+ )
16 14 15 syl ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ⟶ ℝ+ )
17 s2len ⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) = 2
18 17 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) = ( 0 ..^ 2 )
19 18 feq2i ⊢ ( ⟨“ 𝐴 𝐵 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 ”⟩ ) ) ⟶ ℝ+ ↔ ⟨“ 𝐴 𝐵 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ+ )
20 16 19 sylib ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ+ )
21 2 4 s2cld ⊢ ( 𝜑 → ⟨“ 𝑃 𝑄 ”⟩ ∈ Word ℝ+ )
22 wrdf ⊢ ( ⟨“ 𝑃 𝑄 ”⟩ ∈ Word ℝ+ → ⟨“ 𝑃 𝑄 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑃 𝑄 ”⟩ ) ) ⟶ ℝ+ )
23 21 22 syl ⊢ ( 𝜑 → ⟨“ 𝑃 𝑄 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑃 𝑄 ”⟩ ) ) ⟶ ℝ+ )
24 s2len ⊢ ( ♯ ‘ ⟨“ 𝑃 𝑄 ”⟩ ) = 2
25 24 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝑃 𝑄 ”⟩ ) ) = ( 0 ..^ 2 )
26 25 feq2i ⊢ ( ⟨“ 𝑃 𝑄 ”⟩ : ( 0 ..^ ( ♯ ‘ ⟨“ 𝑃 𝑄 ”⟩ ) ) ⟶ ℝ+ ↔ ⟨“ 𝑃 𝑄 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ+ )
27 23 26 sylib ⊢ ( 𝜑 → ⟨“ 𝑃 𝑄 ”⟩ : ( 0 ..^ 2 ) ⟶ ℝ+ )
28 cnring ⊢ ℂfld ∈ Ring
29 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
30 28 29 mp1i ⊢ ( 𝜑 → ℂfld ∈ Mnd )
31 2 rpcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
32 4 rpcnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
33 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
34 cnfldadd ⊢ + = ( +g ‘ ℂfld )
35 33 34 gsumws2 ⊢ ( ( ℂfld ∈ Mnd ∧ 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ) → ( ℂfld Σg ⟨“ 𝑃 𝑄 ”⟩ ) = ( 𝑃 + 𝑄 ) )
36 30 31 32 35 syl3anc ⊢ ( 𝜑 → ( ℂfld Σg ⟨“ 𝑃 𝑄 ”⟩ ) = ( 𝑃 + 𝑄 ) )
37 36 5 eqtrd ⊢ ( 𝜑 → ( ℂfld Σg ⟨“ 𝑃 𝑄 ”⟩ ) = 1 )
38 6 8 13 20 27 37 amgmwlem ⊢ ( 𝜑 → ( ( mulGrp ‘ ℂfld ) Σg ( ⟨“ 𝐴 𝐵 ”⟩ ∘f ↑𝑐 ⟨“ 𝑃 𝑄 ”⟩ ) ) ≤ ( ℂfld Σg ( ⟨“ 𝐴 𝐵 ”⟩ ∘f · ⟨“ 𝑃 𝑄 ”⟩ ) ) )
39 1 3 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) )
40 2 4 jca ⊢ ( 𝜑 → ( 𝑃 ∈ ℝ+ ∧ 𝑄 ∈ ℝ+ ) )
41 ofs2 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑃 ∈ ℝ+ ∧ 𝑄 ∈ ℝ+ ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f ↑𝑐 ⟨“ 𝑃 𝑄 ”⟩ ) = ⟨“ ( 𝐴 ↑𝑐 𝑃 ) ( 𝐵 ↑𝑐 𝑄 ) ”⟩ )
42 39 40 41 syl2anc ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f ↑𝑐 ⟨“ 𝑃 𝑄 ”⟩ ) = ⟨“ ( 𝐴 ↑𝑐 𝑃 ) ( 𝐵 ↑𝑐 𝑄 ) ”⟩ )
43 42 oveq2d ⊢ ( 𝜑 → ( ( mulGrp ‘ ℂfld ) Σg ( ⟨“ 𝐴 𝐵 ”⟩ ∘f ↑𝑐 ⟨“ 𝑃 𝑄 ”⟩ ) ) = ( ( mulGrp ‘ ℂfld ) Σg ⟨“ ( 𝐴 ↑𝑐 𝑃 ) ( 𝐵 ↑𝑐 𝑄 ) ”⟩ ) )
44 6 ringmgp ⊢ ( ℂfld ∈ Ring → ( mulGrp ‘ ℂfld ) ∈ Mnd )
45 28 44 mp1i ⊢ ( 𝜑 → ( mulGrp ‘ ℂfld ) ∈ Mnd )
46 2 rpred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
47 1 46 rpcxpcld ⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝑃 ) ∈ ℝ+ )
48 47 rpcnd ⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝑃 ) ∈ ℂ )
49 4 rpred ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
50 3 49 rpcxpcld ⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝑄 ) ∈ ℝ+ )
51 50 rpcnd ⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝑄 ) ∈ ℂ )
52 6 33 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
53 cnfldmul ⊢ · = ( .r ‘ ℂfld )
54 6 53 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
55 52 54 gsumws2 ⊢ ( ( ( mulGrp ‘ ℂfld ) ∈ Mnd ∧ ( 𝐴 ↑𝑐 𝑃 ) ∈ ℂ ∧ ( 𝐵 ↑𝑐 𝑄 ) ∈ ℂ ) → ( ( mulGrp ‘ ℂfld ) Σg ⟨“ ( 𝐴 ↑𝑐 𝑃 ) ( 𝐵 ↑𝑐 𝑄 ) ”⟩ ) = ( ( 𝐴 ↑𝑐 𝑃 ) · ( 𝐵 ↑𝑐 𝑄 ) ) )
56 45 48 51 55 syl3anc ⊢ ( 𝜑 → ( ( mulGrp ‘ ℂfld ) Σg ⟨“ ( 𝐴 ↑𝑐 𝑃 ) ( 𝐵 ↑𝑐 𝑄 ) ”⟩ ) = ( ( 𝐴 ↑𝑐 𝑃 ) · ( 𝐵 ↑𝑐 𝑄 ) ) )
57 43 56 eqtrd ⊢ ( 𝜑 → ( ( mulGrp ‘ ℂfld ) Σg ( ⟨“ 𝐴 𝐵 ”⟩ ∘f ↑𝑐 ⟨“ 𝑃 𝑄 ”⟩ ) ) = ( ( 𝐴 ↑𝑐 𝑃 ) · ( 𝐵 ↑𝑐 𝑄 ) ) )
58 ofs2 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑃 ∈ ℝ+ ∧ 𝑄 ∈ ℝ+ ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f · ⟨“ 𝑃 𝑄 ”⟩ ) = ⟨“ ( 𝐴 · 𝑃 ) ( 𝐵 · 𝑄 ) ”⟩ )
59 39 40 58 syl2anc ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 ”⟩ ∘f · ⟨“ 𝑃 𝑄 ”⟩ ) = ⟨“ ( 𝐴 · 𝑃 ) ( 𝐵 · 𝑄 ) ”⟩ )
60 59 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( ⟨“ 𝐴 𝐵 ”⟩ ∘f · ⟨“ 𝑃 𝑄 ”⟩ ) ) = ( ℂfld Σg ⟨“ ( 𝐴 · 𝑃 ) ( 𝐵 · 𝑄 ) ”⟩ ) )
61 1 2 rpmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝑃 ) ∈ ℝ+ )
62 61 rpcnd ⊢ ( 𝜑 → ( 𝐴 · 𝑃 ) ∈ ℂ )
63 3 4 rpmulcld ⊢ ( 𝜑 → ( 𝐵 · 𝑄 ) ∈ ℝ+ )
64 63 rpcnd ⊢ ( 𝜑 → ( 𝐵 · 𝑄 ) ∈ ℂ )
65 33 34 gsumws2 ⊢ ( ( ℂfld ∈ Mnd ∧ ( 𝐴 · 𝑃 ) ∈ ℂ ∧ ( 𝐵 · 𝑄 ) ∈ ℂ ) → ( ℂfld Σg ⟨“ ( 𝐴 · 𝑃 ) ( 𝐵 · 𝑄 ) ”⟩ ) = ( ( 𝐴 · 𝑃 ) + ( 𝐵 · 𝑄 ) ) )
66 30 62 64 65 syl3anc ⊢ ( 𝜑 → ( ℂfld Σg ⟨“ ( 𝐴 · 𝑃 ) ( 𝐵 · 𝑄 ) ”⟩ ) = ( ( 𝐴 · 𝑃 ) + ( 𝐵 · 𝑄 ) ) )
67 60 66 eqtrd ⊢ ( 𝜑 → ( ℂfld Σg ( ⟨“ 𝐴 𝐵 ”⟩ ∘f · ⟨“ 𝑃 𝑄 ”⟩ ) ) = ( ( 𝐴 · 𝑃 ) + ( 𝐵 · 𝑄 ) ) )
68 38 57 67 3brtr3d ⊢ ( 𝜑 → ( ( 𝐴 ↑𝑐 𝑃 ) · ( 𝐵 ↑𝑐 𝑄 ) ) ≤ ( ( 𝐴 · 𝑃 ) + ( 𝐵 · 𝑄 ) ) )