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 ffvelrnd
 |-  ( ( ( 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 ffvelrn
 |-  ( ( 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 syl6ib
 |-  ( ( ( 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 syl5bir
 |-  ( ( 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 ) ) )