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	$$⊢\phi \to A\in {ℝ}^{+}$$
	amgmw2d.1	$$⊢\phi \to P\in {ℝ}^{+}$$
	amgmw2d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
	amgmw2d.3	$$⊢\phi \to Q\in {ℝ}^{+}$$
	amgmw2d.4	$$⊢\phi \to P+Q=1$$
Assertion	amgmw2d	$$⊢\phi \to A^P{B}^Q\le AP+BQ$$

Proof

Step	Hyp	Ref	Expression
1		amgmw2d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
2		amgmw2d.1	$$⊢\phi \to P\in {ℝ}^{+}$$
3		amgmw2d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
4		amgmw2d.3	$$⊢\phi \to Q\in {ℝ}^{+}$$
5		amgmw2d.4	$$⊢\phi \to P+Q=1$$
6		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
7		fzofi	$$⊢\left(0..^2\right)\in \mathrm{Fin}$$
8	7	a1i	$$⊢\phi \to \left(0..^2\right)\in \mathrm{Fin}$$
9		2nn	$$⊢2\in \mathbb{N}$$
10		lbfzo0	$$⊢0\in \left(0..^2\right)\leftrightarrow 2\in \mathbb{N}$$
11	9 10	mpbir	$$⊢0\in \left(0..^2\right)$$
12		ne0i	$$⊢0\in \left(0..^2\right)\to \left(0..^2\right)\ne \varnothing$$
13	11 12	mp1i	$$⊢\phi \to \left(0..^2\right)\ne \varnothing$$
14	1 3	s2cld	$$⊢\phi \to ⟨“AB”⟩\in \mathrm{Word}{ℝ}^{+}$$
15		wrdf	$$⊢⟨“AB”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“AB”⟩:\left(0..^\left|⟨“AB”⟩\right|\right)⟶{ℝ}^{+}$$
16	14 15	syl	$$⊢\phi \to ⟨“AB”⟩:\left(0..^\left|⟨“AB”⟩\right|\right)⟶{ℝ}^{+}$$
17		s2len	$$⊢\left|⟨“AB”⟩\right|=2$$
18	17	oveq2i	$$⊢\left(0..^\left|⟨“AB”⟩\right|\right)=\left(0..^2\right)$$
19	18	feq2i	$$⊢⟨“AB”⟩:\left(0..^\left|⟨“AB”⟩\right|\right)⟶{ℝ}^{+}\leftrightarrow ⟨“AB”⟩:\left(0..^2\right)⟶{ℝ}^{+}$$
20	16 19	sylib	$$⊢\phi \to ⟨“AB”⟩:\left(0..^2\right)⟶{ℝ}^{+}$$
21	2 4	s2cld	$$⊢\phi \to ⟨“PQ”⟩\in \mathrm{Word}{ℝ}^{+}$$
22		wrdf	$$⊢⟨“PQ”⟩\in \mathrm{Word}{ℝ}^{+}\to ⟨“PQ”⟩:\left(0..^\left|⟨“PQ”⟩\right|\right)⟶{ℝ}^{+}$$
23	21 22	syl	$$⊢\phi \to ⟨“PQ”⟩:\left(0..^\left|⟨“PQ”⟩\right|\right)⟶{ℝ}^{+}$$
24		s2len	$$⊢\left|⟨“PQ”⟩\right|=2$$
25	24	oveq2i	$$⊢\left(0..^\left|⟨“PQ”⟩\right|\right)=\left(0..^2\right)$$
26	25	feq2i	$$⊢⟨“PQ”⟩:\left(0..^\left|⟨“PQ”⟩\right|\right)⟶{ℝ}^{+}\leftrightarrow ⟨“PQ”⟩:\left(0..^2\right)⟶{ℝ}^{+}$$
27	23 26	sylib	$$⊢\phi \to ⟨“PQ”⟩:\left(0..^2\right)⟶{ℝ}^{+}$$
28		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
29		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
30	28 29	mp1i	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
31	2	rpcnd	$$⊢\phi \to P\in ℂ$$
32	4	rpcnd	$$⊢\phi \to Q\in ℂ$$
33		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
34		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
35	33 34	gsumws2	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge P\in ℂ\wedge Q\in ℂ\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“PQ”⟩=P+Q$$
36	30 31 32 35	syl3anc	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“PQ”⟩=P+Q$$
37	36 5	eqtrd	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“PQ”⟩=1$$
38	6 8 13 20 27 37	amgmwlem	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left(⟨“AB”⟩{{\uparrow }_c}_f⟨“PQ”⟩\right)\le {\sum }_{{ℂ}_{\mathrm{fld}}}\left(⟨“AB”⟩{\times }_f⟨“PQ”⟩\right)$$
39	1 3	jca	$$⊢\phi \to \left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)$$
40	2 4	jca	$$⊢\phi \to \left(P\in {ℝ}^{+}\wedge Q\in {ℝ}^{+}\right)$$
41		ofs2	$$⊢\left(\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\wedge \left(P\in {ℝ}^{+}\wedge Q\in {ℝ}^{+}\right)\right)\to ⟨“AB”⟩{{\uparrow }_c}_f⟨“PQ”⟩=⟨“A^P{B}^Q”⟩$$
42	39 40 41	syl2anc	$$⊢\phi \to ⟨“AB”⟩{{\uparrow }_c}_f⟨“PQ”⟩=⟨“A^P{B}^Q”⟩$$
43	42	oveq2d	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left(⟨“AB”⟩{{\uparrow }_c}_f⟨“PQ”⟩\right)={\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“A^P{B}^Q”⟩$$
44	6	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
45	28 44	mp1i	$$⊢\phi \to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
46	2	rpred	$$⊢\phi \to P\in ℝ$$
47	1 46	rpcxpcld	$$⊢\phi \to A^P\in {ℝ}^{+}$$
48	47	rpcnd	$$⊢\phi \to A^P\in ℂ$$
49	4	rpred	$$⊢\phi \to Q\in ℝ$$
50	3 49	rpcxpcld	$$⊢\phi \to B^Q\in {ℝ}^{+}$$
51	50	rpcnd	$$⊢\phi \to B^Q\in ℂ$$
52	6 33	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
53		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
54	6 53	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
55	52 54	gsumws2	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge A^P\in ℂ\wedge B^Q\in ℂ\right)\to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“A^P{B}^Q”⟩=A^P{B}^Q$$
56	45 48 51 55	syl3anc	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}⟨“A^P{B}^Q”⟩=A^P{B}^Q$$
57	43 56	eqtrd	$$⊢\phi \to {\sum }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left(⟨“AB”⟩{{\uparrow }_c}_f⟨“PQ”⟩\right)=A^P{B}^Q$$
58		ofs2	$$⊢\left(\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\wedge \left(P\in {ℝ}^{+}\wedge Q\in {ℝ}^{+}\right)\right)\to ⟨“AB”⟩{\times }_f⟨“PQ”⟩=⟨“APBQ”⟩$$
59	39 40 58	syl2anc	$$⊢\phi \to ⟨“AB”⟩{\times }_f⟨“PQ”⟩=⟨“APBQ”⟩$$
60	59	oveq2d	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left(⟨“AB”⟩{\times }_f⟨“PQ”⟩\right)={\sum }_{{ℂ}_{\mathrm{fld}}}⟨“APBQ”⟩$$
61	1 2	rpmulcld	$$⊢\phi \to AP\in {ℝ}^{+}$$
62	61	rpcnd	$$⊢\phi \to AP\in ℂ$$
63	3 4	rpmulcld	$$⊢\phi \to BQ\in {ℝ}^{+}$$
64	63	rpcnd	$$⊢\phi \to BQ\in ℂ$$
65	33 34	gsumws2	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge AP\in ℂ\wedge BQ\in ℂ\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“APBQ”⟩=AP+BQ$$
66	30 62 64 65	syl3anc	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}⟨“APBQ”⟩=AP+BQ$$
67	60 66	eqtrd	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left(⟨“AB”⟩{\times }_f⟨“PQ”⟩\right)=AP+BQ$$
68	38 57 67	3brtr3d	$$⊢\phi \to A^P{B}^Q\le AP+BQ$$