Metamath Proof Explorer

Theorem dvfsumrlimge0

Description: Lemma for dvfsumrlim . Satisfy the assumption of dvfsumlem4 . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvfsum.s 
|- S = ( T (,) +oo )
dvfsum.z 
|- Z = ( ZZ>= ` M )
dvfsum.m 
|- ( ph -> M e. ZZ )
dvfsum.d 
|- ( ph -> D e. RR )
dvfsum.md 
|- ( ph -> M <_ ( D + 1 ) )
dvfsum.t 
|- ( ph -> T e. RR )
dvfsum.a 
|- ( ( ph /\ x e. S ) -> A e. RR )
dvfsum.b1 
|- ( ( ph /\ x e. S ) -> B e. V )
dvfsum.b2 
|- ( ( ph /\ x e. Z ) -> B e. RR )
dvfsum.b3 
|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
dvfsum.c 
|- ( x = k -> B = C )
dvfsumrlim.l 
|- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )
dvfsumrlim.g 
|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
dvfsumrlim.k 
|- ( ph -> ( x e. S |-> B ) ~~>r 0 )
Assertion dvfsumrlimge0 
|- ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )

Proof

Step Hyp Ref Expression
1 dvfsum.s 
 |-  S = ( T (,) +oo )
2 dvfsum.z 
 |-  Z = ( ZZ>= ` M )
3 dvfsum.m 
 |-  ( ph -> M e. ZZ )
4 dvfsum.d 
 |-  ( ph -> D e. RR )
5 dvfsum.md 
 |-  ( ph -> M <_ ( D + 1 ) )
6 dvfsum.t 
 |-  ( ph -> T e. RR )
7 dvfsum.a 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
8 dvfsum.b1 
 |-  ( ( ph /\ x e. S ) -> B e. V )
9 dvfsum.b2 
 |-  ( ( ph /\ x e. Z ) -> B e. RR )
10 dvfsum.b3 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
11 dvfsum.c 
 |-  ( x = k -> B = C )
12 dvfsumrlim.l 
 |-  ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )
13 dvfsumrlim.g 
 |-  G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
14 dvfsumrlim.k 
 |-  ( ph -> ( x e. S |-> B ) ~~>r 0 )
15 ioossre 
 |-  ( T (,) +oo ) C_ RR
16 1 15 eqsstri 
 |-  S C_ RR
17 simprl 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> x e. S )
18 16 17 sseldi 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> x e. RR )
19 18 rexrd 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> x e. RR* )
20 18 renepnfd 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> x =/= +oo )
21 icopnfsup 
 |-  ( ( x e. RR* /\ x =/= +oo ) -> sup ( ( x [,) +oo ) , RR* , < ) = +oo )
22 19 20 21 syl2anc 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> sup ( ( x [,) +oo ) , RR* , < ) = +oo )
23 6 rexrd 
 |-  ( ph -> T e. RR* )
24 17 1 eleqtrdi 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> x e. ( T (,) +oo ) )
25 23 adantr 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> T e. RR* )
26 elioopnf 
 |-  ( T e. RR* -> ( x e. ( T (,) +oo ) <-> ( x e. RR /\ T < x ) ) )
27 25 26 syl 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( x e. ( T (,) +oo ) <-> ( x e. RR /\ T < x ) ) )
28 24 27 mpbid 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( x e. RR /\ T < x ) )
29 28 simprd 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> T < x )
30 df-ioo 
 |-  (,) = ( u e. RR* , v e. RR* |-> { w e. RR* | ( u < w /\ w < v ) } )
31 df-ico 
 |-  [,) = ( u e. RR* , v e. RR* |-> { w e. RR* | ( u <_ w /\ w < v ) } )
32 xrltletr 
 |-  ( ( T e. RR* /\ x e. RR* /\ z e. RR* ) -> ( ( T < x /\ x <_ z ) -> T < z ) )
33 30 31 32 ixxss1 
 |-  ( ( T e. RR* /\ T < x ) -> ( x [,) +oo ) C_ ( T (,) +oo ) )
34 23 29 33 syl2an2r 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( x [,) +oo ) C_ ( T (,) +oo ) )
35 34 1 sseqtrrdi 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( x [,) +oo ) C_ S )
36 11 cbvmptv 
 |-  ( x e. S |-> B ) = ( k e. S |-> C )
37 14 adantr 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( x e. S |-> B ) ~~>r 0 )
38 36 37 eqbrtrrid 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( k e. S |-> C ) ~~>r 0 )
39 35 38 rlimres2 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( k e. ( x [,) +oo ) |-> C ) ~~>r 0 )
40 16 a1i 
 |-  ( ph -> S C_ RR )
41 40 7 8 10 dvmptrecl 
 |-  ( ( ph /\ x e. S ) -> B e. RR )
42 41 adantrr 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> B e. RR )
43 42 recnd 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> B e. CC )
44 rlimconst 
 |-  ( ( S C_ RR /\ B e. CC ) -> ( k e. S |-> B ) ~~>r B )
45 40 43 44 syl2an2r 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( k e. S |-> B ) ~~>r B )
46 35 45 rlimres2 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( k e. ( x [,) +oo ) |-> B ) ~~>r B )
47 41 ralrimiva 
 |-  ( ph -> A. x e. S B e. RR )
48 47 adantr 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> A. x e. S B e. RR )
49 35 sselda 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> k e. S )
50 11 eleq1d 
 |-  ( x = k -> ( B e. RR <-> C e. RR ) )
51 50 rspccva 
 |-  ( ( A. x e. S B e. RR /\ k e. S ) -> C e. RR )
52 48 49 51 syl2an2r 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> C e. RR )
53 42 adantr 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> B e. RR )
54 simpll 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> ph )
55 simplrl 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> x e. S )
56 simplrr 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> D <_ x )
57 elicopnf 
 |-  ( x e. RR -> ( k e. ( x [,) +oo ) <-> ( k e. RR /\ x <_ k ) ) )
58 18 57 syl 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> ( k e. ( x [,) +oo ) <-> ( k e. RR /\ x <_ k ) ) )
59 58 simplbda 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> x <_ k )
60 54 55 49 56 59 12 syl122anc 
 |-  ( ( ( ph /\ ( x e. S /\ D <_ x ) ) /\ k e. ( x [,) +oo ) ) -> C <_ B )
61 22 39 46 52 53 60 rlimle 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )