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	⊢ ( 𝜑 → ( ( 𝐴 ↑𝑐 𝑃 ) · ( 𝐵 ↑𝑐 𝑄 ) ) ≤ ( ( 𝐴 · 𝑃 ) + ( 𝐵 · 𝑄 ) ) )