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

Theorem dvfsumrlimge0 22725
 Description: Lemma for dvfsumrlim 22726. Satisfy the assumption of dvfsumlem4 22724. (Contributed by Mario Carneiro, 18-May-2016.)
Hypotheses
Ref Expression
dvfsum.s
dvfsum.z
dvfsum.m
dvfsum.d
dvfsum.md
dvfsum.t
dvfsum.a
dvfsum.b1
dvfsum.b2
dvfsum.b3
dvfsum.c
dvfsumrlim.l
dvfsumrlim.g
dvfsumrlim.k
Assertion
Ref Expression
dvfsumrlimge0
Distinct variable groups:   ,   ,   ,,   ,,   ,,   ,,   ,   ,
Allowed substitution hints:   (,)   ()   ()   ()   (,)   (,)   ()

Proof of Theorem dvfsumrlimge0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . 6
2 ioossre 11642 . . . . . 6
31, 2eqsstri 3474 . . . . 5
4 simprl 758 . . . . 5
53, 4sseldi 3442 . . . 4
65rexrd 9675 . . 3
75renepnfd 9676 . . 3
8 icopnfsup 12032 . . 3
96, 7, 8syl2anc 661 . 2
10 dvfsum.t . . . . . . 7
1110rexrd 9675 . . . . . 6
1211adantr 465 . . . . 5
134, 1syl6eleq 2502 . . . . . . 7
14 elioopnf 11674 . . . . . . . 8
1512, 14syl 17 . . . . . . 7
1613, 15mpbid 212 . . . . . 6
1716simprd 463 . . . . 5
18 df-ioo 11588 . . . . . 6
19 df-ico 11590 . . . . . 6
20 xrltletr 11415 . . . . . 6
2118, 19, 20ixxss1 11602 . . . . 5
2212, 17, 21syl2anc 661 . . . 4
2322, 1syl6sseqr 3491 . . 3
24 dvfsum.c . . . . 5
2524cbvmptv 4489 . . . 4
26 dvfsumrlim.k . . . . 5
2726adantr 465 . . . 4
2825, 27syl5eqbrr 4431 . . 3
2923, 28rlimres2 13535 . 2
303a1i 11 . . . 4
313a1i 11 . . . . . . 7
32 dvfsum.a . . . . . . 7
33 dvfsum.b1 . . . . . . 7
34 dvfsum.b3 . . . . . . 7
3531, 32, 33, 34dvmptrecl 22719 . . . . . 6
3635adantrr 717 . . . . 5
3736recnd 9654 . . . 4
38 rlimconst 13518 . . . 4
3930, 37, 38syl2anc 661 . . 3
4023, 39rlimres2 13535 . 2
4123sselda 3444 . . 3
4235ralrimiva 2820 . . . . 5
4342adantr 465 . . . 4
4424eleq1d 2473 . . . . 5
4544rspccva 3161 . . . 4
4643, 45sylan 471 . . 3
4741, 46syldan 470 . 2