Metamath Proof Explorer

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 
|- ( ph -> A e. RR+ )
young2d.1 
|- ( ph -> P e. RR+ )
young2d.2 
|- ( ph -> B e. RR+ )
young2d.3 
|- ( ph -> Q e. RR+ )
young2d.4 
|- ( ph -> ( ( 1 / P ) + ( 1 / Q ) ) = 1 )
Assertion young2d 
|- ( ph -> ( A x. B ) <_ ( ( ( A ^c P ) / P ) + ( ( B ^c Q ) / Q ) ) )

Proof

Step Hyp Ref Expression
1 young2d.0 
 |-  ( ph -> A e. RR+ )
2 young2d.1 
 |-  ( ph -> P e. RR+ )
3 young2d.2 
 |-  ( ph -> B e. RR+ )
4 young2d.3 
 |-  ( ph -> Q e. RR+ )
5 young2d.4 
 |-  ( ph -> ( ( 1 / P ) + ( 1 / Q ) ) = 1 )
6 2 rpred 
 |-  ( ph -> P e. RR )
7 1 6 rpcxpcld 
 |-  ( ph -> ( A ^c P ) e. RR+ )
8 2 rpreccld 
 |-  ( ph -> ( 1 / P ) e. RR+ )
9 4 rpred 
 |-  ( ph -> Q e. RR )
10 3 9 rpcxpcld 
 |-  ( ph -> ( B ^c Q ) e. RR+ )
11 4 rpreccld 
 |-  ( ph -> ( 1 / Q ) e. RR+ )
12 7 8 10 11 5 amgmw2d 
 |-  ( ph -> ( ( ( A ^c P ) ^c ( 1 / P ) ) x. ( ( B ^c Q ) ^c ( 1 / Q ) ) ) <_ ( ( ( A ^c P ) x. ( 1 / P ) ) + ( ( B ^c Q ) x. ( 1 / Q ) ) ) )
13 2 rpcnd 
 |-  ( ph -> P e. CC )
14 2 rpne0d 
 |-  ( ph -> P =/= 0 )
15 13 14 recidd 
 |-  ( ph -> ( P x. ( 1 / P ) ) = 1 )
16 15 oveq2d 
 |-  ( ph -> ( A ^c ( P x. ( 1 / P ) ) ) = ( A ^c 1 ) )
17 13 14 reccld 
 |-  ( ph -> ( 1 / P ) e. CC )
18 1 6 17 cxpmuld 
 |-  ( ph -> ( A ^c ( P x. ( 1 / P ) ) ) = ( ( A ^c P ) ^c ( 1 / P ) ) )
19 1 rpcnd 
 |-  ( ph -> A e. CC )
20 19 cxp1d 
 |-  ( ph -> ( A ^c 1 ) = A )
21 16 18 20 3eqtr3d 
 |-  ( ph -> ( ( A ^c P ) ^c ( 1 / P ) ) = A )
22 4 rpcnd 
 |-  ( ph -> Q e. CC )
23 4 rpne0d 
 |-  ( ph -> Q =/= 0 )
24 22 23 recidd 
 |-  ( ph -> ( Q x. ( 1 / Q ) ) = 1 )
25 24 oveq2d 
 |-  ( ph -> ( B ^c ( Q x. ( 1 / Q ) ) ) = ( B ^c 1 ) )
26 22 23 reccld 
 |-  ( ph -> ( 1 / Q ) e. CC )
27 3 9 26 cxpmuld 
 |-  ( ph -> ( B ^c ( Q x. ( 1 / Q ) ) ) = ( ( B ^c Q ) ^c ( 1 / Q ) ) )
28 3 rpcnd 
 |-  ( ph -> B e. CC )
29 28 cxp1d 
 |-  ( ph -> ( B ^c 1 ) = B )
30 25 27 29 3eqtr3d 
 |-  ( ph -> ( ( B ^c Q ) ^c ( 1 / Q ) ) = B )
31 21 30 oveq12d 
 |-  ( ph -> ( ( ( A ^c P ) ^c ( 1 / P ) ) x. ( ( B ^c Q ) ^c ( 1 / Q ) ) ) = ( A x. B ) )
32 7 rpcnd 
 |-  ( ph -> ( A ^c P ) e. CC )
33 32 13 14 divrecd 
 |-  ( ph -> ( ( A ^c P ) / P ) = ( ( A ^c P ) x. ( 1 / P ) ) )
34 10 rpcnd 
 |-  ( ph -> ( B ^c Q ) e. CC )
35 34 22 23 divrecd 
 |-  ( ph -> ( ( B ^c Q ) / Q ) = ( ( B ^c Q ) x. ( 1 / Q ) ) )
36 33 35 oveq12d 
 |-  ( ph -> ( ( ( A ^c P ) / P ) + ( ( B ^c Q ) / Q ) ) = ( ( ( A ^c P ) x. ( 1 / P ) ) + ( ( B ^c Q ) x. ( 1 / Q ) ) ) )
37 36 eqcomd 
 |-  ( ph -> ( ( ( A ^c P ) x. ( 1 / P ) ) + ( ( B ^c Q ) x. ( 1 / Q ) ) ) = ( ( ( A ^c P ) / P ) + ( ( B ^c Q ) / Q ) ) )
38 12 31 37 3brtr3d 
 |-  ( ph -> ( A x. B ) <_ ( ( ( A ^c P ) / P ) + ( ( B ^c Q ) / Q ) ) )