Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jensen Structured version   Unicode version

Theorem jensen 20817
 Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.)
Hypotheses
Ref Expression
jensen.1
jensen.2
jensen.3
jensen.4
jensen.5
jensen.6
jensen.7 fld g
jensen.8
Assertion
Ref Expression
jensen fld g fld g fld g fld g fld g fld g
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,   ,,,,,

Proof of Theorem jensen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 jensen.7 . . . . . 6 fld g
2 jensen.5 . . . . . . . . 9
3 ffn 5583 . . . . . . . . 9
42, 3syl 16 . . . . . . . 8
5 fnresdm 5546 . . . . . . . 8
64, 5syl 16 . . . . . . 7
76oveq2d 6089 . . . . . 6 fld g fld g
81, 7breqtrrd 4230 . . . . 5 fld g
9 ssid 3359 . . . . 5
108, 9jctil 524 . . . 4 fld g
11 jensen.4 . . . . 5
12 sseq1 3361 . . . . . . . . 9
13 reseq2 5133 . . . . . . . . . . . . 13
14 res0 5142 . . . . . . . . . . . . 13
1513, 14syl6eq 2483 . . . . . . . . . . . 12
1615oveq2d 6089 . . . . . . . . . . 11 fld g fld g
17 cnfld0 16715 . . . . . . . . . . . 12 fld
1817gsum0 14770 . . . . . . . . . . 11 fld g
1916, 18syl6eq 2483 . . . . . . . . . 10 fld g
2019breq2d 4216 . . . . . . . . 9 fld g
2112, 20anbi12d 692 . . . . . . . 8 fld g
22 reseq2 5133 . . . . . . . . . . 11
2322oveq2d 6089 . . . . . . . . . 10 fld g fld g
2423, 19oveq12d 6091 . . . . . . . . 9 fld g fld g fld g
25 reseq2 5133 . . . . . . . . . . . . 13
2625oveq2d 6089 . . . . . . . . . . . 12 fld g fld g
2726, 19oveq12d 6091 . . . . . . . . . . 11 fld g fld g fld g
2827breq2d 4216 . . . . . . . . . 10 fld g fld g fld g
2928rabbidv 2940 . . . . . . . . 9 fld g fld g fld g
3024, 29eleq12d 2503 . . . . . . . 8 fld g fld g fld g fld g fld g fld g
3121, 30imbi12d 312 . . . . . . 7 fld g fld g fld g fld g fld g fld g fld g
3231imbi2d 308 . . . . . 6 fld g fld g fld g fld g fld g fld g fld g
33 sseq1 3361 . . . . . . . . 9
34 reseq2 5133 . . . . . . . . . . 11
3534oveq2d 6089 . . . . . . . . . 10 fld g fld g
3635breq2d 4216 . . . . . . . . 9 fld g fld g
3733, 36anbi12d 692 . . . . . . . 8 fld g fld g
38 reseq2 5133 . . . . . . . . . . 11
3938oveq2d 6089 . . . . . . . . . 10 fld g fld g
4039, 35oveq12d 6091 . . . . . . . . 9 fld g fld g fld g fld g
41 reseq2 5133 . . . . . . . . . . . . 13
4241oveq2d 6089 . . . . . . . . . . . 12 fld g fld g
4342, 35oveq12d 6091 . . . . . . . . . . 11 fld g fld g fld g fld g
4443breq2d 4216 . . . . . . . . . 10 fld g fld g fld g fld g
4544rabbidv 2940 . . . . . . . . 9 fld g fld g fld g fld g
4640, 45eleq12d 2503 . . . . . . . 8 fld g fld g fld g fld g fld g fld g fld g fld g
4737, 46imbi12d 312 . . . . . . 7 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
4847imbi2d 308 . . . . . 6 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
49 sseq1 3361 . . . . . . . . 9
50 reseq2 5133 . . . . . . . . . . 11
5150oveq2d 6089 . . . . . . . . . 10 fld g fld g
5251breq2d 4216 . . . . . . . . 9 fld g fld g
5349, 52anbi12d 692 . . . . . . . 8 fld g fld g
54 reseq2 5133 . . . . . . . . . . 11
5554oveq2d 6089 . . . . . . . . . 10 fld g fld g
5655, 51oveq12d 6091 . . . . . . . . 9 fld g fld g fld g fld g
57 reseq2 5133 . . . . . . . . . . . . 13
5857oveq2d 6089 . . . . . . . . . . . 12 fld g fld g
5958, 51oveq12d 6091 . . . . . . . . . . 11 fld g fld g fld g fld g
6059breq2d 4216 . . . . . . . . . 10 fld g fld g fld g fld g
6160rabbidv 2940 . . . . . . . . 9 fld g fld g fld g fld g
6256, 61eleq12d 2503 . . . . . . . 8 fld g fld g fld g fld g fld g fld g fld g fld g
6353, 62imbi12d 312 . . . . . . 7 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
6463imbi2d 308 . . . . . 6 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
65 sseq1 3361 . . . . . . . . 9
66 reseq2 5133 . . . . . . . . . . 11
6766oveq2d 6089 . . . . . . . . . 10 fld g fld g
6867breq2d 4216 . . . . . . . . 9 fld g fld g
6965, 68anbi12d 692 . . . . . . . 8 fld g fld g
70 reseq2 5133 . . . . . . . . . . 11
7170oveq2d 6089 . . . . . . . . . 10 fld g fld g
7271, 67oveq12d 6091 . . . . . . . . 9 fld g fld g fld g fld g
73 reseq2 5133 . . . . . . . . . . . . 13
7473oveq2d 6089 . . . . . . . . . . . 12 fld g fld g
7574, 67oveq12d 6091 . . . . . . . . . . 11 fld g fld g fld g fld g
7675breq2d 4216 . . . . . . . . . 10 fld g fld g fld g fld g
7776rabbidv 2940 . . . . . . . . 9 fld g fld g fld g fld g
7872, 77eleq12d 2503 . . . . . . . 8 fld g fld g fld g fld g fld g fld g fld g fld g
7969, 78imbi12d 312 . . . . . . 7 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
8079imbi2d 308 . . . . . 6 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
81 0re 9081 . . . . . . . . . 10
8281ltnri 9172 . . . . . . . . 9
8382pm2.21i 125 . . . . . . . 8 fld g fld g
8483adantl 453 . . . . . . 7 fld g fld g
8584a1i 11 . . . . . 6 fld g fld g
86 impexp 434 . . . . . . . . . . . 12 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
87 simprl 733 . . . . . . . . . . . . . 14 fld g
8887unssad 3516 . . . . . . . . . . . . 13 fld g
89 simpr 448 . . . . . . . . . . . . . . 15 fld g fld g fld g
90 jensen.1 . . . . . . . . . . . . . . . . . . 19
9190ad3antrrr 711 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
92 jensen.2 . . . . . . . . . . . . . . . . . . 19
9392ad3antrrr 711 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
94 simplll 735 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g fld g fld g fld g
95 jensen.3 . . . . . . . . . . . . . . . . . . 19
9694, 95sylan 458 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
9794, 11syl 16 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
9894, 2syl 16 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
99 jensen.6 . . . . . . . . . . . . . . . . . . 19
10094, 99syl 16 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
1011ad3antrrr 711 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g fld g
102 jensen.8 . . . . . . . . . . . . . . . . . . 19
10394, 102sylan 458 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
104 simpllr 736 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
10587adantr 452 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g
106 eqid 2435 . . . . . . . . . . . . . . . . . 18 fld g fld g
107 eqid 2435 . . . . . . . . . . . . . . . . . 18 fld g fld g
108 cnrng 16713 . . . . . . . . . . . . . . . . . . . . . . 23 fld
109 rngcmn 15684 . . . . . . . . . . . . . . . . . . . . . . 23 fld fld CMnd
110108, 109mp1i 12 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld CMnd
11111ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23 fld g
112 ssfi 7321 . . . . . . . . . . . . . . . . . . . . . . 23
113111, 88, 112syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22 fld g
114 rege0subm 16745 . . . . . . . . . . . . . . . . . . . . . . 23 SubMndfld
115114a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 fld g SubMndfld
1162ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23 fld g
117 fssres 5602 . . . . . . . . . . . . . . . . . . . . . . 23
118116, 88, 117syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22 fld g
119113, 118fisuppfi 14763 . . . . . . . . . . . . . . . . . . . . . 22 fld g
12017, 110, 113, 115, 118, 119gsumsubmcl 15514 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
121 elrege0 10997 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld g fld g
122121simplbi 447 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
123120, 122syl 16 . . . . . . . . . . . . . . . . . . . 20 fld g fld g
124123adantr 452 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g fld g fld g fld g fld g
125 simprl 733 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g fld g fld g fld g fld g
126124, 125elrpd 10636 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g fld g
127 simprr 734 . . . . . . . . . . . . . . . . . . . 20 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
128 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld g fld g fld g
129128breq1d 4214 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g fld g fld g fld g fld g fld g fld g
130129elrab 3084 . . . . . . . . . . . . . . . . . . . 20 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
131127, 130sylib 189 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
132131simpld 446 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g fld g fld g
133131simprd 450 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
13491, 93, 96, 97, 98, 100, 101, 103, 104, 105, 106, 107, 126, 132, 133jensenlem2 20816 . . . . . . . . . . . . . . . . 17 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
135 fveq2 5720 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g fld g
136135breq1d 4214 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g fld g fld g fld g fld g
137136elrab 3084 . . . . . . . . . . . . . . . . 17 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
138134, 137sylibr 204 . . . . . . . . . . . . . . . 16 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
139138expr 599 . . . . . . . . . . . . . . 15 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
14089, 139embantd 52 . . . . . . . . . . . . . 14 fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g fld g
141 cnfldbas 16697 . . . . . . . . . . . . . . . . . . . . 21 fld
142 rngmnd 15663 . . . . . . . . . . . . . . . . . . . . . 22 fld fld
143108, 142mp1i 12 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g fld
144 ssfi 7321 . . . . . . . . . . . . . . . . . . . . . . 23
145111, 87, 144syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22 fld g
146145adantr 452 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
147 ssun2 3503 . . . . . . . . . . . . . . . . . . . . . . 23
148 vex 2951 . . . . . . . . . . . . . . . . . . . . . . . 24
149148snid 3833 . . . . . . . . . . . . . . . . . . . . . . 23
150147, 149sselii 3337 . . . . . . . . . . . . . . . . . . . . . 22
151150a1i 11 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
152 remulcl 9065 . . . . . . . . . . . . . . . . . . . . . . . . . 26
153152adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25
154 elrege0 10997 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
155154simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
156155ssriv 3344 . . . . . . . . . . . . . . . . . . . . . . . . . 26
157 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1582, 156, 157sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25
159 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . . . 26
16099, 90, 159syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
161 inidm 3542 . . . . . . . . . . . . . . . . . . . . . . . . 25
162153, 158, 160, 11, 11, 161off 6312 . . . . . . . . . . . . . . . . . . . . . . . 24
163 ax-resscn 9037 . . . . . . . . . . . . . . . . . . . . . . . 24
164 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . 24
165162, 163, 164sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 23
166165ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld g
16787adantr 452 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld g
168 fssres 5602 . . . . . . . . . . . . . . . . . . . . . 22
169166, 167, 168syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
1702ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld g fld g
171111adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld g fld g
172 fex 5961 . . . . . . . . . . . . . . . . . . . . . . . . . 26
173170, 171, 172syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld g fld g
17499ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld g fld g
175 fex 5961 . . . . . . . . . . . . . . . . . . . . . . . . . 26
176174, 171, 175syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld g fld g
177 offres 6311 . . . . . . . . . . . . . . . . . . . . . . . . 25
178173, 176, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24 fld g fld g
179178cnveqd 5040 . . . . . . . . . . . . . . . . . . . . . . 23 fld g fld g
180179imaeq1d 5194 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld g
181156, 163sstri 3349 . . . . . . . . . . . . . . . . . . . . . . . . . 26
182 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . . . 26
183170, 181, 182sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld g fld g
184 fssres 5602 . . . . . . . . . . . . . . . . . . . . . . . . 25
185183, 167, 184syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24 fld g fld g
186 eldifi 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
187186adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld g fld g
188 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189187, 188syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld g fld g
190 difun2 3699 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
191 difss 3466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
192190, 191eqsstri 3370 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
193192sseli 3336 . . . . . . . . . . . . . . . . . . . . . . . . . 26
194 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fld g fld g fld g
19588adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 fld g fld g
196170, 195feqresmpt 5772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 fld g fld g
197196oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fld g fld g fld g fld g
198113adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 fld g fld g
199195sselda 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 fld g fld g
200170ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 fld g fld g
201199, 200syldan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 fld g fld g
202181, 201sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 fld g fld g
203198, 202gsumfsum 16756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fld g fld g fld g
204194, 197, 2033eqtrrd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 fld g fld g
205 elrege0 10997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
206201, 205sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 fld g fld g
207206simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fld g fld g
208206simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 fld g fld g
209198, 207, 208fsum00 12567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 fld g fld g
210204, 209mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 fld g fld g
211210r19.21bi 2796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld g fld g
212193, 211sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld g fld g
213189, 212eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . 24 fld g fld g
214185, 213suppss 5855 . . . . . . . . . . . . . . . . . . . . . . 23 fld g fld g
215 mul02 9234 . . . . . . . . . . . . . . . . . . . . . . . 24
216215adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23 fld g fld g
21790ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 fld g fld g
218217, 163syl6ss 3352 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld g fld g
219 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . . 25
220174, 218, 219syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24 fld g fld g
221 fssres 5602 . . . . . . . . . . . . . . . . . . . . . . . 24
222220, 167, 221syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23 fld g fld g
223214, 216, 185, 222, 146suppssof1 6338 . . . . . . . . . . . . . . . . . . . . . 22 fld g fld g
224180, 223eqsstrd 3374 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
225141, 17, 143, 146, 151, 169, 224gsumpt 15535 . . . . . . . . . . . . . . . . . . . 20 fld g fld g fld g
226 fvres 5737 . . . . . . . . . . . . . . . . . . . . 21
227151, 226syl 16 . . . . . . . . . . . . . . . . . . . 20 fld g fld g
228170, 3syl 16 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
229 ffn 5583 . . . . . . . . . . . . . . . . . . . . . 22
230174, 229syl 16 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
231167, 151sseldd 3341 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g
232 fnfvof 6309 . . . . . . . . . . . . . . . . . . . . 21
233228, 230, 171, 231, 232syl22anc 1185 . . . . . . . . . . . . . . . . . . . 20 fld g fld g
234225, 227, 2333eqtrd 2471 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g
235141, 17, 143, 146, 151, 185, 214gsumpt 15535 . . . . . . . . . . . . . . . . . . . 20 fld g fld g fld g
236 fvres 5737 . . . . . . . . . . . . . . . . . . . . 21
237151, 236syl 16 . . . . . . . . . . . . . . . . . . . 20 fld g fld g
238235, 237eqtrd 2467 . . . . . . . . . . . . . . . . . . 19 fld g fld g fld g
239234, 238oveq12d 6091 . . . . . . . . . . . . . . . . . 18 fld g fld g fld g fld g
240220, 231ffvelrnd 5863 . . . . . . . . . . . . . . . . . . 19 fld g fld g
241183, 231ffvelrnd 5863 . . . . . . . . . . . . . . . . . . 19 fld g fld g
242 simplrr 738 . . . . . . . . . . . . . . . . . . . . 21 fld g fld g fld g
243242, 238breqtrd 4228 . . . . . . . . . . . . . . . . . . . 20