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	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	young2d.1	⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
	young2d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	young2d.3	⊢ ( 𝜑 → 𝑄 ∈ ℝ+ )
	young2d.4	⊢ ( 𝜑 → ( ( 1 / 𝑃 ) + ( 1 / 𝑄 ) ) = 1 )
Assertion	young2d	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ≤ ( ( ( 𝐴 ↑𝑐 𝑃 ) / 𝑃 ) + ( ( 𝐵 ↑𝑐 𝑄 ) / 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		young2d.0	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		young2d.1	⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
3		young2d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4		young2d.3	⊢ ( 𝜑 → 𝑄 ∈ ℝ+ )
5		young2d.4	⊢ ( 𝜑 → ( ( 1 / 𝑃 ) + ( 1 / 𝑄 ) ) = 1 )
6	2	rpred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
7	1 6	rpcxpcld	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝑃 ) ∈ ℝ+ )
8	2	rpreccld	⊢ ( 𝜑 → ( 1 / 𝑃 ) ∈ ℝ+ )
9	4	rpred	⊢ ( 𝜑 → 𝑄 ∈ ℝ )
10	3 9	rpcxpcld	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝑄 ) ∈ ℝ+ )
11	4	rpreccld	⊢ ( 𝜑 → ( 1 / 𝑄 ) ∈ ℝ+ )
12	7 8 10 11 5	amgmw2d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑𝑐 𝑃 ) ↑𝑐 ( 1 / 𝑃 ) ) · ( ( 𝐵 ↑𝑐 𝑄 ) ↑𝑐 ( 1 / 𝑄 ) ) ) ≤ ( ( ( 𝐴 ↑𝑐 𝑃 ) · ( 1 / 𝑃 ) ) + ( ( 𝐵 ↑𝑐 𝑄 ) · ( 1 / 𝑄 ) ) ) )
13	2	rpcnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
14	2	rpne0d	⊢ ( 𝜑 → 𝑃 ≠ 0 )
15	13 14	recidd	⊢ ( 𝜑 → ( 𝑃 · ( 1 / 𝑃 ) ) = 1 )
16	15	oveq2d	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 ( 𝑃 · ( 1 / 𝑃 ) ) ) = ( 𝐴 ↑𝑐 1 ) )
17	13 14	reccld	⊢ ( 𝜑 → ( 1 / 𝑃 ) ∈ ℂ )
18	1 6 17	cxpmuld	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 ( 𝑃 · ( 1 / 𝑃 ) ) ) = ( ( 𝐴 ↑𝑐 𝑃 ) ↑𝑐 ( 1 / 𝑃 ) ) )
19	1	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
20	19	cxp1d	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 1 ) = 𝐴 )
21	16 18 20	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 ↑𝑐 𝑃 ) ↑𝑐 ( 1 / 𝑃 ) ) = 𝐴 )
22	4	rpcnd	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
23	4	rpne0d	⊢ ( 𝜑 → 𝑄 ≠ 0 )
24	22 23	recidd	⊢ ( 𝜑 → ( 𝑄 · ( 1 / 𝑄 ) ) = 1 )
25	24	oveq2d	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 ( 𝑄 · ( 1 / 𝑄 ) ) ) = ( 𝐵 ↑𝑐 1 ) )
26	22 23	reccld	⊢ ( 𝜑 → ( 1 / 𝑄 ) ∈ ℂ )
27	3 9 26	cxpmuld	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 ( 𝑄 · ( 1 / 𝑄 ) ) ) = ( ( 𝐵 ↑𝑐 𝑄 ) ↑𝑐 ( 1 / 𝑄 ) ) )
28	3	rpcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
29	28	cxp1d	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 1 ) = 𝐵 )
30	25 27 29	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐵 ↑𝑐 𝑄 ) ↑𝑐 ( 1 / 𝑄 ) ) = 𝐵 )
31	21 30	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑𝑐 𝑃 ) ↑𝑐 ( 1 / 𝑃 ) ) · ( ( 𝐵 ↑𝑐 𝑄 ) ↑𝑐 ( 1 / 𝑄 ) ) ) = ( 𝐴 · 𝐵 ) )
32	7	rpcnd	⊢ ( 𝜑 → ( 𝐴 ↑𝑐 𝑃 ) ∈ ℂ )
33	32 13 14	divrecd	⊢ ( 𝜑 → ( ( 𝐴 ↑𝑐 𝑃 ) / 𝑃 ) = ( ( 𝐴 ↑𝑐 𝑃 ) · ( 1 / 𝑃 ) ) )
34	10	rpcnd	⊢ ( 𝜑 → ( 𝐵 ↑𝑐 𝑄 ) ∈ ℂ )
35	34 22 23	divrecd	⊢ ( 𝜑 → ( ( 𝐵 ↑𝑐 𝑄 ) / 𝑄 ) = ( ( 𝐵 ↑𝑐 𝑄 ) · ( 1 / 𝑄 ) ) )
36	33 35	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑𝑐 𝑃 ) / 𝑃 ) + ( ( 𝐵 ↑𝑐 𝑄 ) / 𝑄 ) ) = ( ( ( 𝐴 ↑𝑐 𝑃 ) · ( 1 / 𝑃 ) ) + ( ( 𝐵 ↑𝑐 𝑄 ) · ( 1 / 𝑄 ) ) ) )
37	36	eqcomd	⊢ ( 𝜑 → ( ( ( 𝐴 ↑𝑐 𝑃 ) · ( 1 / 𝑃 ) ) + ( ( 𝐵 ↑𝑐 𝑄 ) · ( 1 / 𝑄 ) ) ) = ( ( ( 𝐴 ↑𝑐 𝑃 ) / 𝑃 ) + ( ( 𝐵 ↑𝑐 𝑄 ) / 𝑄 ) ) )
38	12 31 37	3brtr3d	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ≤ ( ( ( 𝐴 ↑𝑐 𝑃 ) / 𝑃 ) + ( ( 𝐵 ↑𝑐 𝑄 ) / 𝑄 ) ) )