Theorem young2d

Description: Young's inequality for n = 2 , a direct application of amgmw2d . (Contributed by Kunhao Zheng, 6-Jul-2021)

	Ref	Expression
Hypotheses	young2d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
	young2d.1	$$⊢\phi \to P\in {ℝ}^{+}$$
	young2d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
	young2d.3	$$⊢\phi \to Q\in {ℝ}^{+}$$
	young2d.4	$$⊢\phi \to \left(\frac{1}{P}\right)+\left(\frac{1}{Q}\right)=1$$
Assertion	young2d	$$⊢\phi \to AB\le \left(\frac{A^P}{P}\right)+\left(\frac{B^Q}{Q}\right)$$

Proof

Step	Hyp	Ref	Expression
1		young2d.0	$$⊢\phi \to A\in {ℝ}^{+}$$
2		young2d.1	$$⊢\phi \to P\in {ℝ}^{+}$$
3		young2d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
4		young2d.3	$$⊢\phi \to Q\in {ℝ}^{+}$$
5		young2d.4	$$⊢\phi \to \left(\frac{1}{P}\right)+\left(\frac{1}{Q}\right)=1$$
6	2	rpred	$$⊢\phi \to P\in ℝ$$
7	1 6	rpcxpcld	$$⊢\phi \to A^P\in {ℝ}^{+}$$
8	2	rpreccld	$$⊢\phi \to \frac{1}{P}\in {ℝ}^{+}$$
9	4	rpred	$$⊢\phi \to Q\in ℝ$$
10	3 9	rpcxpcld	$$⊢\phi \to B^Q\in {ℝ}^{+}$$
11	4	rpreccld	$$⊢\phi \to \frac{1}{Q}\in {ℝ}^{+}$$
12	7 8 10 11 5	amgmw2d	$$⊢\phi \to {\left(A^P\right)}^{\frac{1}{P}}{\left(B^Q\right)}^{\frac{1}{Q}}\le A^P\left(\frac{1}{P}\right)+B^Q\left(\frac{1}{Q}\right)$$
13	2	rpcnd	$$⊢\phi \to P\in ℂ$$
14	2	rpne0d	$$⊢\phi \to P\ne 0$$
15	13 14	recidd	$$⊢\phi \to P\left(\frac{1}{P}\right)=1$$
16	15	oveq2d	$$⊢\phi \to A^{P\left(\frac{1}{P}\right)}=A^1$$
17	13 14	reccld	$$⊢\phi \to \frac{1}{P}\in ℂ$$
18	1 6 17	cxpmuld	$$⊢\phi \to A^{P\left(\frac{1}{P}\right)}={\left(A^P\right)}^{\frac{1}{P}}$$
19	1	rpcnd	$$⊢\phi \to A\in ℂ$$
20	19	cxp1d	$$⊢\phi \to A^1=A$$
21	16 18 20	3eqtr3d	$$⊢\phi \to {\left(A^P\right)}^{\frac{1}{P}}=A$$
22	4	rpcnd	$$⊢\phi \to Q\in ℂ$$
23	4	rpne0d	$$⊢\phi \to Q\ne 0$$
24	22 23	recidd	$$⊢\phi \to Q\left(\frac{1}{Q}\right)=1$$
25	24	oveq2d	$$⊢\phi \to B^{Q\left(\frac{1}{Q}\right)}=B^1$$
26	22 23	reccld	$$⊢\phi \to \frac{1}{Q}\in ℂ$$
27	3 9 26	cxpmuld	$$⊢\phi \to B^{Q\left(\frac{1}{Q}\right)}={\left(B^Q\right)}^{\frac{1}{Q}}$$
28	3	rpcnd	$$⊢\phi \to B\in ℂ$$
29	28	cxp1d	$$⊢\phi \to B^1=B$$
30	25 27 29	3eqtr3d	$$⊢\phi \to {\left(B^Q\right)}^{\frac{1}{Q}}=B$$
31	21 30	oveq12d	$$⊢\phi \to {\left(A^P\right)}^{\frac{1}{P}}{\left(B^Q\right)}^{\frac{1}{Q}}=AB$$
32	7	rpcnd	$$⊢\phi \to A^P\in ℂ$$
33	32 13 14	divrecd	$$⊢\phi \to \frac{A^P}{P}=A^P\left(\frac{1}{P}\right)$$
34	10	rpcnd	$$⊢\phi \to B^Q\in ℂ$$
35	34 22 23	divrecd	$$⊢\phi \to \frac{B^Q}{Q}=B^Q\left(\frac{1}{Q}\right)$$
36	33 35	oveq12d	$$⊢\phi \to \left(\frac{A^P}{P}\right)+\left(\frac{B^Q}{Q}\right)=A^P\left(\frac{1}{P}\right)+B^Q\left(\frac{1}{Q}\right)$$
37	36	eqcomd	$$⊢\phi \to A^P\left(\frac{1}{P}\right)+B^Q\left(\frac{1}{Q}\right)=\left(\frac{A^P}{P}\right)+\left(\frac{B^Q}{Q}\right)$$
38	12 31 37	3brtr3d	$$⊢\phi \to AB\le \left(\frac{A^P}{P}\right)+\left(\frac{B^Q}{Q}\right)$$