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

Theorem jensenlem2 22781
Description: Lemma for jensen 22782. (Contributed by Mario Carneiro, 21-Jun-2015.)
Hypotheses
Ref Expression
jensen.1
jensen.2
jensen.3
jensen.4
jensen.5
jensen.6
jensen.7
jensen.8
jensenlem.1
jensenlem.2
jensenlem.s
jensenlem.l
jensenlem.3
jensenlem.4
jensenlem.5
Assertion
Ref Expression
jensenlem2
Distinct variable groups:   , , , , ,   , , , , ,   , , , , ,   , , , , ,   , , , , ,   , , , , ,   , , , , , ,   , , ,   S, , , , ,

Proof of Theorem jensenlem2
StepHypRef Expression
1 cnfld0 18033 . . . . . . 7
2 cnrng 18031 . . . . . . . 8
3 rngabl 16850 . . . . . . . 8
42, 3mp1i 12 . . . . . . 7
5 jensen.4 . . . . . . . 8
6 jensenlem.2 . . . . . . . . 9
76unssad 3647 . . . . . . . 8
8 ssfi 7668 . . . . . . . 8
95, 7, 8syl2anc 661 . . . . . . 7
10 resubdrg 18231 . . . . . . . . 9
1110simpli 458 . . . . . . . 8
12 subrgsubg 17047 . . . . . . . 8
1311, 12mp1i 12 . . . . . . 7
14 remulcl 9504 . . . . . . . . . 10
1514adantl 466 . . . . . . . . 9
16 jensen.5 . . . . . . . . . 10
17 0re 9523 . . . . . . . . . . 11
18 pnfxr 11231 . . . . . . . . . . 11
19 icossre 11515 . . . . . . . . . . 11
2017, 18, 19mp2an 672 . . . . . . . . . 10
21 fss 5687 . . . . . . . . . 10
2216, 20, 21sylancl 662 . . . . . . . . 9
23 jensen.6 . . . . . . . . . 10
24 jensen.1 . . . . . . . . . 10
25 fss 5687 . . . . . . . . . 10
2623, 24, 25syl2anc 661 . . . . . . . . 9
27 inidm 3673 . . . . . . . . 9
2815, 22, 26, 5, 5, 27off 6467 . . . . . . . 8
29 fssres 5699 . . . . . . . 8
3028, 7, 29syl2anc 661 . . . . . . 7
31 c0ex 9517 . . . . . . . . 9
3231a1i 11 . . . . . . . 8
3330, 9, 32fdmfifsupp 7765 . . . . . . 7
341, 4, 9, 13, 30, 33gsumsubgcl 16567 . . . . . 6
3534recnd 9549 . . . . 5
36 ax-resscn 9476 . . . . . . . 8
3720, 36sstri 3479 . . . . . . 7
386unssbd 3648 . . . . . . . . 9
39 vex 3084 . . . . . . . . . 10
4039snss 4116 . . . . . . . . 9
4138, 40sylibr 212 . . . . . . . 8
4216, 41ffvelrnd 5967 . . . . . . 7
4337, 42sseldi 3468 . . . . . 6
4423, 41ffvelrnd 5967 . . . . . . . 8
4524, 44sseldd 3471 . . . . . . 7
4645recnd 9549 . . . . . 6
4743, 46mulcld 9543 . . . . 5
48 jensen.2 . . . . . . . 8
49 jensen.3 . . . . . . . 8
50 jensen.7 . . . . . . . 8
51 jensen.8 . . . . . . . 8
52 jensenlem.1 . . . . . . . 8
53 jensenlem.s . . . . . . . 8
54 jensenlem.l . . . . . . . 8
5524, 48, 49, 5, 16, 23, 50, 51, 52, 6, 53, 54jensenlem1 22780 . . . . . . 7
56 jensenlem.3 . . . . . . . . 9
5756rpred 11166 . . . . . . . 8
58 elrege0 11537 . . . . . . . . . 10
5958simplbi 460 . . . . . . . . 9
6042, 59syl 16 . . . . . . . 8
6157, 60readdcld 9550 . . . . . . 7
6255, 61eqeltrd 2542 . . . . . 6
6362recnd 9549 . . . . 5
64 0red 9524 . . . . . . 7
6556rpgt0d 11169 . . . . . . 7
6658simprbi 464 . . . . . . . . . 10
6742, 66syl 16 . . . . . . . . 9
6857, 60addge01d 10064 . . . . . . . . 9
6967, 68mpbid 210 . . . . . . . 8
7069, 55breqtrrd 4435 . . . . . . 7
7164, 57, 62, 65, 70ltletrd 9668 . . . . . 6
7271gt0ne0d 10041 . . . . 5
7335, 47, 63, 72divdird 10282 . . . 4
74 cnfldbas 18015 . . . . . . 7
75 cnfldadd 18016 . . . . . . 7
76 rngcmn 16851 . . . . . . . 8
772, 76mp1i 12 . . . . . . 7
787sselda 3470 . . . . . . . . . 10
7916ffvelrnda 5966 . . . . . . . . . 10
8078, 79syldan 470 . . . . . . . . 9
8137, 80sseldi 3468 . . . . . . . 8
8224adantr 465 . . . . . . . . . 10
8323ffvelrnda 5966 . . . . . . . . . . 11
8478, 83syldan 470 . . . . . . . . . 10
8582, 84sseldd 3471 . . . . . . . . 9
8685recnd 9549 . . . . . . . 8
8781, 86mulcld 9543 . . . . . . 7
88 fveq2 5813 . . . . . . . 8
89 fveq2 5813 . . . . . . . 8
9088, 89oveq12d 6240 . . . . . . 7
9174, 75, 77, 9, 87, 41, 52, 47, 90gsumunsn 16619 . . . . . 6
9216feqmptd 5867 . . . . . . . . . 10
9323feqmptd 5867 . . . . . . . . . 10
945, 79, 83, 92, 93offval2 6469 . . . . . . . . 9
9594reseq1d 5226 . . . . . . . 8
96 resmpt 5274 . . . . . . . . 9
976, 96syl 16 . . . . . . . 8
9895, 97eqtrd 2495 . . . . . . 7
9998oveq2d 6238 . . . . . 6
10094reseq1d 5226 . . . . . . . . 9
101 resmpt 5274 . . . . . . . . . 10
1027, 101syl 16 . . . . . . . . 9
103100, 102eqtrd 2495 . . . . . . . 8
104103oveq2d 6238 . . . . . . 7
105104oveq1d 6237 . . . . . 6
10691, 99, 1053eqtr4d 2505 . . . . 5
107106oveq1d 6237 . . . 4
10857recnd 9549 . . . . . 6
10956rpne0d 11171 . . . . . 6
11035, 108, 63, 109, 72dmdcand 10273 . . . . 5
11163, 108, 63, 72divsubdird 10283 . . . . . . . 8
11255oveq1d 6237 . . . . . . . . . 10
113108, 43pncan2d 9858 . . . . . . . . . 10
114112, 113eqtrd 2495 . . . . . . . . 9
115114oveq1d 6237 . . . . . . . 8
11663, 72dividd 10242 . . . . . . . . 9
117116oveq1d 6237 . . . . . . . 8
118111, 115, 1173eqtr3rd 2504 . . . . . . 7
119118oveq1d 6237 . . . . . 6
12043, 46, 63, 72div23d 10281 . . . . . 6
121119, 120eqtr4d 2498 . . . . 5
122110, 121oveq12d 6240 . . . 4
12373, 107, 1223eqtr4d 2505 . . 3
124 jensenlem.4 . . . . 5
12557, 62, 72redivcld 10296 . . . . . 6
12656rpge0d 11170 . . . . . . 7
127 divge0 10335 . . . . . . 7
12857, 126, 62, 71, 127syl22anc 1220 . . . . . 6
12963mulid1d 9540 . . . . . . . 8
13070, 129breqtrrd 4435 . . . . . . 7
131 1red 9538 . . . . . . . 8
132 ledivmul 10342 . . . . . . . 8
13357, 131, 62, 71, 132syl112anc 1223 . . . . . . 7
134130, 133mpbird 232 . . . . . 6
135 1re 9522 . . . . . . 7
13617, 135elicc2i 11500 . . . . . 6
137125, 128, 134, 136syl3anbrc 1172 . . . . 5
138124, 44, 1373jca 1168 . . . 4
13924, 49cvxcl 22778 . . . 4
140138, 139mpdan 668 . . 3
141123, 140eqeltrd 2542 . 2
14248, 140ffvelrnd 5967 . . . 4
14348, 124ffvelrnd 5967 . . . . . 6
144125, 143remulcld 9551 . . . . 5
14548, 44ffvelrnd 5967 . . . . . . 7
14660, 145remulcld 9551 . . . . . 6
147146, 62, 72redivcld 10296 . . . . 5
148144, 147readdcld 9550 . . . 4
149 fco 5689 . . . . . . . . . . 11
15048, 23, 149syl2anc 661 . . . . . . . . . 10
15115, 22, 150, 5, 5, 27off 6467 . . . . . . . . 9
152 fssres 5699 . . . . . . . . 9
153151, 7, 152syl2anc 661 . . . . . . . 8
154153, 9, 32fdmfifsupp 7765 . . . . . . . 8
1551, 4, 9, 13, 153, 154gsumsubgcl 16567 . . . . . . 7
156155, 57, 109redivcld 10296 . . . . . 6
157125, 156remulcld 9551 . . . . 5
158 resubcl 9810 . . . . . . 7
159135, 125, 158sylancr 663 . . . . . 6
160159, 145remulcld 9551 . . . . 5
161157, 160readdcld 9550 . . . 4
162 oveq2 6230 . . . . . . . . . . . 12
163162oveq1d 6237 . . . . . . . . . . 11
164163fveq2d 5817 . . . . . . . . . 10
165 fveq2 5813 . . . . . . . . . . . 12
166165oveq2d 6238 . . . . . . . . . . 11
167166oveq1d 6237 . . . . . . . . . 10
168164, 167breq12d 4422 . . . . . . . . 9
169168imbi2d 316 . . . . . . . 8
170 oveq2 6230 . . . . . . . . . . . 12
171170oveq2d 6238 . . . . . . . . . . 11
172171fveq2d 5817 . . . . . . . . . 10
173 fveq2 5813 . . . . . . . . . . . 12
174173oveq2d 6238 . . . . . . . . . . 11
175174oveq2d 6238 . . . . . . . . . 10
176172, 175breq12d 4422 . . . . . . . . 9
177176imbi2d 316 . . . . . . . 8
178 oveq1 6229 . . . . . . . . . . . 12
179 oveq2 6230 . . . . . . . . . . . . 13
180179oveq1d 6237 . . . . . . . . . . . 12
181178, 180oveq12d 6240 . . . . . . . . . . 11
182181fveq2d 5817 . . . . . . . . . 10
183 oveq1 6229 . . . . . . . . . . 11
184179oveq1d 6237 . . . . . . . . . . 11
185183, 184oveq12d 6240 . . . . . . . . . 10
186182, 185breq12d 4422 . . . . . . . . 9
187186imbi2d 316 . . . . . . . 8
18851expcom 435 . . . . . . . 8
189169, 177, 187, 188vtocl3ga 3149 . . . . . . 7
190124, 44, 137, 189syl3anc 1219 . . . . . 6
191190pm2.43i 47 . . . . 5
192118oveq1d 6237 . . . . . . 7
193145recnd 9549 . . . . . . . 8
19443, 193, 63, 72div23d 10281 . . . . . . 7
195192, 194eqtr4d 2498 . . . . . 6
196195oveq2d 6238 . . . . 5
197191, 196breqtrd 4433 . . . 4
198194, 192eqtr4d 2498 . . . . . 6
199198oveq2d 6238 . . . . 5
200 jensenlem.5 . . . . . . 7
20157, 62, 65, 71divgt0d 10405 . . . . . . . 8
202 lemul2 10319 . . . . . . . 8
203143, 156, 125, 201, 202syl112anc 1223 . . . . . . 7
204200, 203mpbid 210 . . . . . 6
205144, 157, 160, 204leadd1dd 10090 . . . . 5