Metamath Proof Explorer

Theorem amgm4d

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

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

Proof

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