Metamath Proof Explorer

Theorem amgm

Description: Inequality of arithmetic and geometric means. Here ( M gsum F ) calculates the group sum within the multiplicative monoid of the complex numbers (or in other words, it multiplies the elements F ( x ) , x e. A together), and ( CCfld gsum F ) calculates the group sum in the additive group (i.e. the sum of the elements). This is Metamath 100 proof #38. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypothesis amgm.1 
|- M = ( mulGrp ` CCfld )
Assertion amgm 
|- ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )

Proof

Step Hyp Ref Expression
1 amgm.1 
 |-  M = ( mulGrp ` CCfld )
2 cnfldbas 
 |-  CC = ( Base ` CCfld )
3 1 2 mgpbas 
 |-  CC = ( Base ` M )
4 cnfld1 
 |-  1 = ( 1r ` CCfld )
5 1 4 ringidval 
 |-  1 = ( 0g ` M )
6 cnfldmul 
 |-  x. = ( .r ` CCfld )
7 1 6 mgpplusg 
 |-  x. = ( +g ` M )
8 cncrng 
 |-  CCfld e. CRing
9 1 crngmgp 
 |-  ( CCfld e. CRing -> M e. CMnd )
10 8 9 mp1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> M e. CMnd )
11 simpl1 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> A e. Fin )
12 simpl3 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> F : A --> ( 0 [,) +oo ) )
13 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
14 ax-resscn 
 |-  RR C_ CC
15 13 14 sstri 
 |-  ( 0 [,) +oo ) C_ CC
16 fss 
 |-  ( ( F : A --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> F : A --> CC )
17 12 15 16 sylancl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> F : A --> CC )
18 1ex 
 |-  1 e. _V
19 18 a1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> 1 e. _V )
20 17 11 19 fdmfifsupp 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> F finSupp 1 )
21 disjdif 
 |-  ( { x } i^i ( A \ { x } ) ) = (/)
22 21 a1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( { x } i^i ( A \ { x } ) ) = (/) )
23 undif2 
 |-  ( { x } u. ( A \ { x } ) ) = ( { x } u. A )
24 simprl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> x e. A )
25 24 snssd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> { x } C_ A )
26 ssequn1 
 |-  ( { x } C_ A <-> ( { x } u. A ) = A )
27 25 26 sylib 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( { x } u. A ) = A )
28 23 27 eqtr2id 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> A = ( { x } u. ( A \ { x } ) ) )
29 3 5 7 10 11 17 20 22 28 gsumsplit 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( M gsum F ) = ( ( M gsum ( F |` { x } ) ) x. ( M gsum ( F |` ( A \ { x } ) ) ) ) )
30 12 25 feqresmpt 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( F |` { x } ) = ( y e. { x } |-> ( F ` y ) ) )
31 30 oveq2d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( M gsum ( F |` { x } ) ) = ( M gsum ( y e. { x } |-> ( F ` y ) ) ) )
32 cnring 
 |-  CCfld e. Ring
33 1 ringmgp 
 |-  ( CCfld e. Ring -> M e. Mnd )
34 32 33 mp1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> M e. Mnd )
35 17 24 ffvelcdmd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( F ` x ) e. CC )
36 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
37 3 36 gsumsn 
 |-  ( ( M e. Mnd /\ x e. A /\ ( F ` x ) e. CC ) -> ( M gsum ( y e. { x } |-> ( F ` y ) ) ) = ( F ` x ) )
38 34 24 35 37 syl3anc 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( M gsum ( y e. { x } |-> ( F ` y ) ) ) = ( F ` x ) )
39 simprr 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( F ` x ) = 0 )
40 31 38 39 3eqtrd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( M gsum ( F |` { x } ) ) = 0 )
41 40 oveq1d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( ( M gsum ( F |` { x } ) ) x. ( M gsum ( F |` ( A \ { x } ) ) ) ) = ( 0 x. ( M gsum ( F |` ( A \ { x } ) ) ) ) )
42 diffi 
 |-  ( A e. Fin -> ( A \ { x } ) e. Fin )
43 11 42 syl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( A \ { x } ) e. Fin )
44 difss 
 |-  ( A \ { x } ) C_ A
45 fssres 
 |-  ( ( F : A --> CC /\ ( A \ { x } ) C_ A ) -> ( F |` ( A \ { x } ) ) : ( A \ { x } ) --> CC )
46 17 44 45 sylancl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( F |` ( A \ { x } ) ) : ( A \ { x } ) --> CC )
47 46 43 19 fdmfifsupp 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( F |` ( A \ { x } ) ) finSupp 1 )
48 3 5 10 43 46 47 gsumcl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( M gsum ( F |` ( A \ { x } ) ) ) e. CC )
49 48 mul02d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( 0 x. ( M gsum ( F |` ( A \ { x } ) ) ) ) = 0 )
50 29 41 49 3eqtrd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( M gsum F ) = 0 )
51 50 oveq1d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) = ( 0 ^c ( 1 / ( # ` A ) ) ) )
52 simpl2 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> A =/= (/) )
53 hashnncl 
 |-  ( A e. Fin -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
54 11 53 syl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( ( # ` A ) e. NN <-> A =/= (/) ) )
55 52 54 mpbird 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( # ` A ) e. NN )
56 55 nncnd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( # ` A ) e. CC )
57 55 nnne0d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( # ` A ) =/= 0 )
58 56 57 reccld 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( 1 / ( # ` A ) ) e. CC )
59 56 57 recne0d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( 1 / ( # ` A ) ) =/= 0 )
60 58 59 0cxpd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( 0 ^c ( 1 / ( # ` A ) ) ) = 0 )
61 51 60 eqtrd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) = 0 )
62 cnfld0 
 |-  0 = ( 0g ` CCfld )
63 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
64 32 63 mp1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> CCfld e. CMnd )
65 rege0subm 
 |-  ( 0 [,) +oo ) e. ( SubMnd ` CCfld )
66 65 a1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( 0 [,) +oo ) e. ( SubMnd ` CCfld ) )
67 c0ex 
 |-  0 e. _V
68 67 a1i 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> 0 e. _V )
69 12 11 68 fdmfifsupp 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> F finSupp 0 )
70 62 64 11 66 12 69 gsumsubmcl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( CCfld gsum F ) e. ( 0 [,) +oo ) )
71 elrege0 
 |-  ( ( CCfld gsum F ) e. ( 0 [,) +oo ) <-> ( ( CCfld gsum F ) e. RR /\ 0 <_ ( CCfld gsum F ) ) )
72 70 71 sylib 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( ( CCfld gsum F ) e. RR /\ 0 <_ ( CCfld gsum F ) ) )
73 55 nnred 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( # ` A ) e. RR )
74 55 nngt0d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> 0 < ( # ` A ) )
75 divge0 
 |-  ( ( ( ( CCfld gsum F ) e. RR /\ 0 <_ ( CCfld gsum F ) ) /\ ( ( # ` A ) e. RR /\ 0 < ( # ` A ) ) ) -> 0 <_ ( ( CCfld gsum F ) / ( # ` A ) ) )
76 72 73 74 75 syl12anc 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> 0 <_ ( ( CCfld gsum F ) / ( # ` A ) ) )
77 61 76 eqbrtrd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ ( x e. A /\ ( F ` x ) = 0 ) ) -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )
78 77 rexlimdvaa 
 |-  ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( E. x e. A ( F ` x ) = 0 -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) ) )
79 ralnex 
 |-  ( A. x e. A -. ( F ` x ) = 0 <-> -. E. x e. A ( F ` x ) = 0 )
80 simpl1 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> A e. Fin )
81 simpl2 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> A =/= (/) )
82 simpl3 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> F : A --> ( 0 [,) +oo ) )
83 82 ffnd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> F Fn A )
84 ffvelcdm 
 |-  ( ( F : A --> ( 0 [,) +oo ) /\ x e. A ) -> ( F ` x ) e. ( 0 [,) +oo ) )
85 84 3ad2antl3 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( F ` x ) e. ( 0 [,) +oo ) )
86 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
87 85 86 sylib 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
88 87 simprd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> 0 <_ ( F ` x ) )
89 0re 
 |-  0 e. RR
90 87 simpld 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( F ` x ) e. RR )
91 leloe 
 |-  ( ( 0 e. RR /\ ( F ` x ) e. RR ) -> ( 0 <_ ( F ` x ) <-> ( 0 < ( F ` x ) \/ 0 = ( F ` x ) ) ) )
92 89 90 91 sylancr 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( 0 <_ ( F ` x ) <-> ( 0 < ( F ` x ) \/ 0 = ( F ` x ) ) ) )
93 88 92 mpbid 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( 0 < ( F ` x ) \/ 0 = ( F ` x ) ) )
94 93 ord 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( -. 0 < ( F ` x ) -> 0 = ( F ` x ) ) )
95 eqcom 
 |-  ( 0 = ( F ` x ) <-> ( F ` x ) = 0 )
96 94 95 imbitrdi 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( -. 0 < ( F ` x ) -> ( F ` x ) = 0 ) )
97 96 con1d 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( -. ( F ` x ) = 0 -> 0 < ( F ` x ) ) )
98 elrp 
 |-  ( ( F ` x ) e. RR+ <-> ( ( F ` x ) e. RR /\ 0 < ( F ` x ) ) )
99 98 baib 
 |-  ( ( F ` x ) e. RR -> ( ( F ` x ) e. RR+ <-> 0 < ( F ` x ) ) )
100 90 99 syl 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( ( F ` x ) e. RR+ <-> 0 < ( F ` x ) ) )
101 97 100 sylibrd 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ x e. A ) -> ( -. ( F ` x ) = 0 -> ( F ` x ) e. RR+ ) )
102 101 ralimdva 
 |-  ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( A. x e. A -. ( F ` x ) = 0 -> A. x e. A ( F ` x ) e. RR+ ) )
103 102 imp 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> A. x e. A ( F ` x ) e. RR+ )
104 ffnfv 
 |-  ( F : A --> RR+ <-> ( F Fn A /\ A. x e. A ( F ` x ) e. RR+ ) )
105 83 103 104 sylanbrc 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> F : A --> RR+ )
106 1 80 81 105 amgmlem 
 |-  ( ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) /\ A. x e. A -. ( F ` x ) = 0 ) -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )
107 106 ex 
 |-  ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( A. x e. A -. ( F ` x ) = 0 -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) ) )
108 79 107 biimtrrid 
 |-  ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( -. E. x e. A ( F ` x ) = 0 -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) ) )
109 78 108 pm2.61d 
 |-  ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )