Metamath Proof Explorer

Theorem amgm2d

Description: Arithmetic-geometric mean inequality for n = 2 , derived from amgmlem . (Contributed by Stanislas Polu, 8-Sep-2020)

Ref Expression
Hypotheses amgm2d.0 
|- ( ph -> A e. RR+ )
amgm2d.1 
|- ( ph -> B e. RR+ )
Assertion amgm2d 
|- ( ph -> ( ( A x. B ) ^c ( 1 / 2 ) ) <_ ( ( A + B ) / 2 ) )

Proof

Step Hyp Ref Expression
1 amgm2d.0 
 |-  ( ph -> A e. RR+ )
2 amgm2d.1 
 |-  ( ph -> B e. RR+ )
3 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
4 fzofi 
 |-  ( 0 ..^ 2 ) e. Fin
5 4 a1i 
 |-  ( ph -> ( 0 ..^ 2 ) e. Fin )
6 2nn 
 |-  2 e. NN
7 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> 2 e. NN )
8 6 7 mpbir 
 |-  0 e. ( 0 ..^ 2 )
9 8 ne0ii 
 |-  ( 0 ..^ 2 ) =/= (/)
10 9 a1i 
 |-  ( ph -> ( 0 ..^ 2 ) =/= (/) )
11 1 2 s2cld 
 |-  ( ph -> <" A B "> e. Word RR+ )
12 wrdf 
 |-  ( <" A B "> e. Word RR+ -> <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> RR+ )
13 s2len 
 |-  ( # ` <" A B "> ) = 2
14 13 eqcomi 
 |-  2 = ( # ` <" A B "> )
15 14 oveq2i 
 |-  ( 0 ..^ 2 ) = ( 0 ..^ ( # ` <" A B "> ) )
16 15 feq2i 
 |-  ( <" A B "> : ( 0 ..^ 2 ) --> RR+ <-> <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> RR+ )
17 12 16 sylibr 
 |-  ( <" A B "> e. Word RR+ -> <" A B "> : ( 0 ..^ 2 ) --> RR+ )
18 11 17 syl 
 |-  ( ph -> <" A B "> : ( 0 ..^ 2 ) --> RR+ )
19 3 5 10 18 amgmlem 
 |-  ( ph -> ( ( ( mulGrp ` CCfld ) gsum <" A B "> ) ^c ( 1 / ( # ` ( 0 ..^ 2 ) ) ) ) <_ ( ( CCfld gsum <" A B "> ) / ( # ` ( 0 ..^ 2 ) ) ) )
20 cnring 
 |-  CCfld e. Ring
21 3 ringmgp 
 |-  ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
22 20 21 mp1i 
 |-  ( ph -> ( mulGrp ` CCfld ) e. Mnd )
23 1 rpcnd 
 |-  ( ph -> A e. CC )
24 2 rpcnd 
 |-  ( ph -> B e. CC )
25 cnfldbas 
 |-  CC = ( Base ` CCfld )
26 3 25 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
27 cnfldmul 
 |-  x. = ( .r ` CCfld )
28 3 27 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
29 26 28 gsumws2 
 |-  ( ( ( mulGrp ` CCfld ) e. Mnd /\ A e. CC /\ B e. CC ) -> ( ( mulGrp ` CCfld ) gsum <" A B "> ) = ( A x. B ) )
30 22 23 24 29 syl3anc 
 |-  ( ph -> ( ( mulGrp ` CCfld ) gsum <" A B "> ) = ( A x. B ) )
31 2nn0 
 |-  2 e. NN0
32 hashfzo0 
 |-  ( 2 e. NN0 -> ( # ` ( 0 ..^ 2 ) ) = 2 )
33 31 32 mp1i 
 |-  ( ph -> ( # ` ( 0 ..^ 2 ) ) = 2 )
34 33 oveq2d 
 |-  ( ph -> ( 1 / ( # ` ( 0 ..^ 2 ) ) ) = ( 1 / 2 ) )
35 30 34 oveq12d 
 |-  ( ph -> ( ( ( mulGrp ` CCfld ) gsum <" A B "> ) ^c ( 1 / ( # ` ( 0 ..^ 2 ) ) ) ) = ( ( A x. B ) ^c ( 1 / 2 ) ) )
36 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
37 20 36 mp1i 
 |-  ( ph -> CCfld e. Mnd )
38 cnfldadd 
 |-  + = ( +g ` CCfld )
39 25 38 gsumws2 
 |-  ( ( CCfld e. Mnd /\ A e. CC /\ B e. CC ) -> ( CCfld gsum <" A B "> ) = ( A + B ) )
40 37 23 24 39 syl3anc 
 |-  ( ph -> ( CCfld gsum <" A B "> ) = ( A + B ) )
41 40 33 oveq12d 
 |-  ( ph -> ( ( CCfld gsum <" A B "> ) / ( # ` ( 0 ..^ 2 ) ) ) = ( ( A + B ) / 2 ) )
42 19 35 41 3brtr3d 
 |-  ( ph -> ( ( A x. B ) ^c ( 1 / 2 ) ) <_ ( ( A + B ) / 2 ) )