Metamath Proof Explorer

Theorem amgm3d

Description: Arithmetic-geometric mean inequality for n = 3 . (Contributed by Stanislas Polu, 11-Sep-2020)

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

Proof

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