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

Theorem jensenlem2 22122
Description: Lemma for jensen 22123. (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 17550 . . . . . . 7
2 cnrng 17548 . . . . . . . 8
3 rngabl 16502 . . . . . . . 8
42, 3mp1i 12 . . . . . . 7
5 jensen.4 . . . . . . . 8
6 jensenlem.2 . . . . . . . . 9
76unssad 3510 . . . . . . . 8
8 ssfi 7492 . . . . . . . 8
95, 7, 8syl2anc 646 . . . . . . 7
10 resubdrg 17746 . . . . . . . . 9
1110simpli 448 . . . . . . . 8
12 subrgsubg 16684 . . . . . . . 8
1311, 12mp1i 12 . . . . . . 7
14 remulcl 9313 . . . . . . . . . 10
1514adantl 456 . . . . . . . . 9
16 jensen.5 . . . . . . . . . 10
17 0re 9332 . . . . . . . . . . 11
18 pnfxr 11037 . . . . . . . . . . 11
19 icossre 11321 . . . . . . . . . . 11
2017, 18, 19mp2an 657 . . . . . . . . . 10
21 fss 5537 . . . . . . . . . 10
2216, 20, 21sylancl 647 . . . . . . . . 9
23 jensen.6 . . . . . . . . . 10
24 jensen.1 . . . . . . . . . 10
25 fss 5537 . . . . . . . . . 10
2623, 24, 25syl2anc 646 . . . . . . . . 9
27 inidm 3536 . . . . . . . . 9
2815, 22, 26, 5, 5, 27off 6304 . . . . . . . 8
29 fssres 5548 . . . . . . . 8
3028, 7, 29syl2anc 646 . . . . . . 7
319, 30fisuppfi 7587 . . . . . . 7
321, 4, 9, 13, 30, 31gsumsubgcl 16328 . . . . . 6
3332recnd 9358 . . . . 5
34 ax-resscn 9285 . . . . . . . 8
3520, 34sstri 3342 . . . . . . 7
366unssbd 3511 . . . . . . . . 9
37 vex 2954 . . . . . . . . . 10
3837snss 3974 . . . . . . . . 9
3936, 38sylibr 206 . . . . . . . 8
4016, 39ffvelrnd 5814 . . . . . . 7
4135, 40sseldi 3331 . . . . . 6
4223, 39ffvelrnd 5814 . . . . . . . 8
4324, 42sseldd 3334 . . . . . . 7
4443recnd 9358 . . . . . 6
4541, 44mulcld 9352 . . . . 5
46 jensen.2 . . . . . . . 8
47 jensen.3 . . . . . . . 8
48 jensen.7 . . . . . . . 8
49 jensen.8 . . . . . . . 8
50 jensenlem.1 . . . . . . . 8
51 jensenlem.s . . . . . . . 8
52 jensenlem.l . . . . . . . 8
5324, 46, 47, 5, 16, 23, 48, 49, 50, 6, 51, 52jensenlem1 22121 . . . . . . 7
54 jensenlem.3 . . . . . . . . 9
5554rpred 10972 . . . . . . . 8
56 elrege0 11337 . . . . . . . . . 10
5756simplbi 450 . . . . . . . . 9
5840, 57syl 16 . . . . . . . 8
5955, 58readdcld 9359 . . . . . . 7
6053, 59eqeltrd 2496 . . . . . 6
6160recnd 9358 . . . . 5
62 0red 9333 . . . . . . 7
6354rpgt0d 10975 . . . . . . 7
6456simprbi 454 . . . . . . . . . 10
6540, 64syl 16 . . . . . . . . 9
6655, 58addge01d 9873 . . . . . . . . 9
6765, 66mpbid 204 . . . . . . . 8
6867, 53breqtrrd 4293 . . . . . . 7
6962, 55, 60, 63, 68ltletrd 9477 . . . . . 6
7069gt0ne0d 9850 . . . . 5
7133, 45, 61, 70divdird 10091 . . . 4
72 cnfldbas 17532 . . . . . . 7
73 cnfldadd 17533 . . . . . . 7
74 rngcmn 16503 . . . . . . . 8
752, 74mp1i 12 . . . . . . 7
767sselda 3333 . . . . . . . . . 10
7716ffvelrnda 5813 . . . . . . . . . 10
7876, 77syldan 460 . . . . . . . . 9
7935, 78sseldi 3331 . . . . . . . 8
8024adantr 455 . . . . . . . . . 10
8123ffvelrnda 5813 . . . . . . . . . . 11
8276, 81syldan 460 . . . . . . . . . 10
8380, 82sseldd 3334 . . . . . . . . 9
8483recnd 9358 . . . . . . . 8
8579, 84mulcld 9352 . . . . . . 7
86 fveq2 5661 . . . . . . . 8
87 fveq2 5661 . . . . . . . 8
8886, 87oveq12d 6079 . . . . . . 7
8972, 73, 75, 9, 85, 39, 50, 45, 88gsumunsn 16350 . . . . . 6
9016feqmptd 5714 . . . . . . . . . 10
9123feqmptd 5714 . . . . . . . . . 10
925, 77, 81, 90, 91offval2 6306 . . . . . . . . 9
9392reseq1d 5080 . . . . . . . 8
94 resmpt 5128 . . . . . . . . 9
956, 94syl 16 . . . . . . . 8
9693, 95eqtrd 2454 . . . . . . 7
9796oveq2d 6077 . . . . . 6
9892reseq1d 5080 . . . . . . . . 9
99 resmpt 5128 . . . . . . . . . 10
1007, 99syl 16 . . . . . . . . 9
10198, 100eqtrd 2454 . . . . . . . 8
102101oveq2d 6077 . . . . . . 7
103102oveq1d 6076 . . . . . 6
10489, 97, 1033eqtr4d 2464 . . . . 5
105104oveq1d 6076 . . . 4
10655recnd 9358 . . . . . 6
10754rpne0d 10977 . . . . . 6
10833, 106, 61, 107, 70dmdcand 10082 . . . . 5
10961, 106, 61, 70divsubdird 10092 . . . . . . . 8
11053oveq1d 6076 . . . . . . . . . 10
111106, 41pncan2d 9667 . . . . . . . . . 10
112110, 111eqtrd 2454 . . . . . . . . 9
113112oveq1d 6076 . . . . . . . 8
11461, 70dividd 10051 . . . . . . . . 9
115114oveq1d 6076 . . . . . . . 8
116109, 113, 1153eqtr3rd 2463 . . . . . . 7
117116oveq1d 6076 . . . . . 6
11841, 44, 61, 70div23d 10090 . . . . . 6
119117, 118eqtr4d 2457 . . . . 5
120108, 119oveq12d 6079 . . . 4
12171, 105, 1203eqtr4d 2464 . . 3
122 jensenlem.4 . . . . 5
12355, 60, 70redivcld 10105 . . . . . 6
12454rpge0d 10976 . . . . . . 7
125 divge0 10144 . . . . . . 7
12655, 124, 60, 69, 125syl22anc 1204 . . . . . 6
12761mulid1d 9349 . . . . . . . 8
12868, 127breqtrrd 4293 . . . . . . 7
129 1red 9347 . . . . . . . 8
130 ledivmul 10151 . . . . . . . 8
13155, 129, 60, 69, 130syl112anc 1207 . . . . . . 7
132128, 131mpbird 226 . . . . . 6
133 1re 9331 . . . . . . 7
13417, 133elicc2i 11306 . . . . . 6
135123, 126, 132, 134syl3anbrc 1157 . . . . 5
136122, 42, 1353jca 1153 . . . 4
13724, 47cvxcl 22119 . . . 4
138136, 137mpdan 653 . . 3
139121, 138eqeltrd 2496 . 2
14046, 138ffvelrnd 5814 . . . 4
14146, 122ffvelrnd 5814 . . . . . 6
142123, 141remulcld 9360 . . . . 5
14346, 42ffvelrnd 5814 . . . . . . 7
14458, 143remulcld 9360 . . . . . 6
145144, 60, 70redivcld 10105 . . . . 5
146142, 145readdcld 9359 . . . 4
147 fco 5538 . . . . . . . . . . 11
14846, 23, 147syl2anc 646 . . . . . . . . . 10
14915, 22, 148, 5, 5, 27off 6304 . . . . . . . . 9
150 fssres 5548 . . . . . . . . 9
151149, 7, 150syl2anc 646 . . . . . . . 8
1529, 151fisuppfi 7587 . . . . . . . 8
1531, 4, 9, 13, 151, 152gsumsubgcl 16328 . . . . . . 7
154153, 55, 107redivcld 10105 . . . . . 6
155123, 154remulcld 9360 . . . . 5
156 resubcl 9619 . . . . . . 7
157133, 123, 156sylancr 648 . . . . . 6
158157, 143remulcld 9360 . . . . 5
159155, 158readdcld 9359 . . . 4
160 oveq2 6069 . . . . . . . . . . . 12
161160oveq1d 6076 . . . . . . . . . . 11
162161fveq2d 5665 . . . . . . . . . 10
163 fveq2 5661 . . . . . . . . . . . 12
164163oveq2d 6077 . . . . . . . . . . 11
165164oveq1d 6076 . . . . . . . . . 10
166162, 165breq12d 4280 . . . . . . . . 9
167166imbi2d 310 . . . . . . . 8
168 oveq2 6069 . . . . . . . . . . . 12
169168oveq2d 6077 . . . . . . . . . . 11
170169fveq2d 5665 . . . . . . . . . 10
171 fveq2 5661 . . . . . . . . . . . 12
172171oveq2d 6077 . . . . . . . . . . 11
173172oveq2d 6077 . . . . . . . . . 10
174170, 173breq12d 4280 . . . . . . . . 9
175174imbi2d 310 . . . . . . . 8
176 oveq1 6068 . . . . . . . . . . . 12
177 oveq2 6069 . . . . . . . . . . . . 13
178177oveq1d 6076 . . . . . . . . . . . 12
179176, 178oveq12d 6079 . . . . . . . . . . 11
180179fveq2d 5665 . . . . . . . . . 10
181 oveq1 6068 . . . . . . . . . . 11
182177oveq1d 6076 . . . . . . . . . . 11
183181, 182oveq12d 6079 . . . . . . . . . 10
184180, 183breq12d 4280 . . . . . . . . 9
185184imbi2d 310 . . . . . . . 8
18649expcom 428 . . . . . . . 8
187167, 175, 185, 186vtocl3ga 3018 . . . . . . 7
188122, 42, 135, 187syl3anc 1203 . . . . . 6
189188pm2.43i 46 . . . . 5
190116oveq1d 6076 . . . . . . 7
191143recnd 9358 . . . . . . . 8
19241, 191, 61, 70div23d 10090 . . . . . . 7
193190, 192eqtr4d 2457 . . . . . 6
194193oveq2d 6077 . . . . 5
195189, 194breqtrd 4291 . . . 4
196192, 190eqtr4d 2457 . . . . . 6
197196oveq2d 6077 . . . . 5
198 jensenlem.5 . . . . . . 7
19955, 60, 63, 69divgt0d 10214 . . . . . . . 8
200 lemul2 10128 . . . . . . . 8
201141, 154, 123, 199, 200syl112anc 1207 . . . . . . 7
202198, 201mpbid 204 . . . . . 6
203142, 155, 158, 202leadd1dd 9899 . . . . 5