Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 amgmw2d.0 
 |-  ( ph -> A e. RR+ )
2 amgmw2d.1 
 |-  ( ph -> P e. RR+ )
3 amgmw2d.2 
 |-  ( ph -> B e. RR+ )
4 amgmw2d.3 
 |-  ( ph -> Q e. RR+ )
5 amgmw2d.4 
 |-  ( ph -> ( P + Q ) = 1 )
6 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
7 fzofi 
 |-  ( 0 ..^ 2 ) e. Fin
8 7 a1i 
 |-  ( ph -> ( 0 ..^ 2 ) e. Fin )
9 2nn 
 |-  2 e. NN
10 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> 2 e. NN )
11 9 10 mpbir 
 |-  0 e. ( 0 ..^ 2 )
12 ne0i 
 |-  ( 0 e. ( 0 ..^ 2 ) -> ( 0 ..^ 2 ) =/= (/) )
13 11 12 mp1i 
 |-  ( ph -> ( 0 ..^ 2 ) =/= (/) )
14 1 3 s2cld 
 |-  ( ph -> <" A B "> e. Word RR+ )
15 wrdf 
 |-  ( <" A B "> e. Word RR+ -> <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> RR+ )
16 14 15 syl 
 |-  ( ph -> <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> RR+ )
17 s2len 
 |-  ( # ` <" A B "> ) = 2
18 17 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B "> ) ) = ( 0 ..^ 2 )
19 18 feq2i 
 |-  ( <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> RR+ <-> <" A B "> : ( 0 ..^ 2 ) --> RR+ )
20 16 19 sylib 
 |-  ( ph -> <" A B "> : ( 0 ..^ 2 ) --> RR+ )
21 2 4 s2cld 
 |-  ( ph -> <" P Q "> e. Word RR+ )
22 wrdf 
 |-  ( <" P Q "> e. Word RR+ -> <" P Q "> : ( 0 ..^ ( # ` <" P Q "> ) ) --> RR+ )
23 21 22 syl 
 |-  ( ph -> <" P Q "> : ( 0 ..^ ( # ` <" P Q "> ) ) --> RR+ )
24 s2len 
 |-  ( # ` <" P Q "> ) = 2
25 24 oveq2i 
 |-  ( 0 ..^ ( # ` <" P Q "> ) ) = ( 0 ..^ 2 )
26 25 feq2i 
 |-  ( <" P Q "> : ( 0 ..^ ( # ` <" P Q "> ) ) --> RR+ <-> <" P Q "> : ( 0 ..^ 2 ) --> RR+ )
27 23 26 sylib 
 |-  ( ph -> <" P Q "> : ( 0 ..^ 2 ) --> RR+ )
28 cnring 
 |-  CCfld e. Ring
29 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
30 28 29 mp1i 
 |-  ( ph -> CCfld e. Mnd )
31 2 rpcnd 
 |-  ( ph -> P e. CC )
32 4 rpcnd 
 |-  ( ph -> Q e. CC )
33 cnfldbas 
 |-  CC = ( Base ` CCfld )
34 cnfldadd 
 |-  + = ( +g ` CCfld )
35 33 34 gsumws2 
 |-  ( ( CCfld e. Mnd /\ P e. CC /\ Q e. CC ) -> ( CCfld gsum <" P Q "> ) = ( P + Q ) )
36 30 31 32 35 syl3anc 
 |-  ( ph -> ( CCfld gsum <" P Q "> ) = ( P + Q ) )
37 36 5 eqtrd 
 |-  ( ph -> ( CCfld gsum <" P Q "> ) = 1 )
38 6 8 13 20 27 37 amgmwlem 
 |-  ( ph -> ( ( mulGrp ` CCfld ) gsum ( <" A B "> oF ^c <" P Q "> ) ) <_ ( CCfld gsum ( <" A B "> oF x. <" P Q "> ) ) )
39 1 3 jca 
 |-  ( ph -> ( A e. RR+ /\ B e. RR+ ) )
40 2 4 jca 
 |-  ( ph -> ( P e. RR+ /\ Q e. RR+ ) )
41 ofs2 
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( P e. RR+ /\ Q e. RR+ ) ) -> ( <" A B "> oF ^c <" P Q "> ) = <" ( A ^c P ) ( B ^c Q ) "> )
42 39 40 41 syl2anc 
 |-  ( ph -> ( <" A B "> oF ^c <" P Q "> ) = <" ( A ^c P ) ( B ^c Q ) "> )
43 42 oveq2d 
 |-  ( ph -> ( ( mulGrp ` CCfld ) gsum ( <" A B "> oF ^c <" P Q "> ) ) = ( ( mulGrp ` CCfld ) gsum <" ( A ^c P ) ( B ^c Q ) "> ) )
44 6 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
45 28 44 mp1i 
 |-  ( ph -> ( mulGrp ` CCfld ) e. Mnd )
46 2 rpred 
 |-  ( ph -> P e. RR )
47 1 46 rpcxpcld 
 |-  ( ph -> ( A ^c P ) e. RR+ )
48 47 rpcnd 
 |-  ( ph -> ( A ^c P ) e. CC )
49 4 rpred 
 |-  ( ph -> Q e. RR )
50 3 49 rpcxpcld 
 |-  ( ph -> ( B ^c Q ) e. RR+ )
51 50 rpcnd 
 |-  ( ph -> ( B ^c Q ) e. CC )
52 6 33 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
53 cnfldmul 
 |-  x. = ( .r ` CCfld )
54 6 53 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
55 52 54 gsumws2 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ ( A ^c P ) e. CC /\ ( B ^c Q ) e. CC ) -> ( ( mulGrp ` CCfld ) gsum <" ( A ^c P ) ( B ^c Q ) "> ) = ( ( A ^c P ) x. ( B ^c Q ) ) )
56 45 48 51 55 syl3anc 
 |-  ( ph -> ( ( mulGrp ` CCfld ) gsum <" ( A ^c P ) ( B ^c Q ) "> ) = ( ( A ^c P ) x. ( B ^c Q ) ) )
57 43 56 eqtrd 
 |-  ( ph -> ( ( mulGrp ` CCfld ) gsum ( <" A B "> oF ^c <" P Q "> ) ) = ( ( A ^c P ) x. ( B ^c Q ) ) )
58 ofs2 
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( P e. RR+ /\ Q e. RR+ ) ) -> ( <" A B "> oF x. <" P Q "> ) = <" ( A x. P ) ( B x. Q ) "> )
59 39 40 58 syl2anc 
 |-  ( ph -> ( <" A B "> oF x. <" P Q "> ) = <" ( A x. P ) ( B x. Q ) "> )
60 59 oveq2d 
 |-  ( ph -> ( CCfld gsum ( <" A B "> oF x. <" P Q "> ) ) = ( CCfld gsum <" ( A x. P ) ( B x. Q ) "> ) )
61 1 2 rpmulcld 
 |-  ( ph -> ( A x. P ) e. RR+ )
62 61 rpcnd 
 |-  ( ph -> ( A x. P ) e. CC )
63 3 4 rpmulcld 
 |-  ( ph -> ( B x. Q ) e. RR+ )
64 63 rpcnd 
 |-  ( ph -> ( B x. Q ) e. CC )
65 33 34 gsumws2 
 |-  ( ( CCfld e. Mnd /\ ( A x. P ) e. CC /\ ( B x. Q ) e. CC ) -> ( CCfld gsum <" ( A x. P ) ( B x. Q ) "> ) = ( ( A x. P ) + ( B x. Q ) ) )
66 30 62 64 65 syl3anc 
 |-  ( ph -> ( CCfld gsum <" ( A x. P ) ( B x. Q ) "> ) = ( ( A x. P ) + ( B x. Q ) ) )
67 60 66 eqtrd 
 |-  ( ph -> ( CCfld gsum ( <" A B "> oF x. <" P Q "> ) ) = ( ( A x. P ) + ( B x. Q ) ) )
68 38 57 67 3brtr3d 
 |-  ( ph -> ( ( A ^c P ) x. ( B ^c Q ) ) <_ ( ( A x. P ) + ( B x. Q ) ) )