Metamath Proof Explorer

Theorem rlimresb

Description: The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimresb.1 
|- ( ph -> F : A --> CC )
rlimresb.2 
|- ( ph -> A C_ RR )
rlimresb.3 
|- ( ph -> B e. RR )
Assertion rlimresb 
|- ( ph -> ( F ~~>r C <-> ( F |` ( B [,) +oo ) ) ~~>r C ) )

Proof

Step Hyp Ref Expression
1 rlimresb.1 
 |-  ( ph -> F : A --> CC )
2 rlimresb.2 
 |-  ( ph -> A C_ RR )
3 rlimresb.3 
 |-  ( ph -> B e. RR )
4 rlimcl 
 |-  ( ( x e. A |-> ( F ` x ) ) ~~>r C -> C e. CC )
5 4 a1i 
 |-  ( ph -> ( ( x e. A |-> ( F ` x ) ) ~~>r C -> C e. CC ) )
6 rlimcl 
 |-  ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C -> C e. CC )
7 6 a1i 
 |-  ( ph -> ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C -> C e. CC ) )
8 2 adantr 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> A C_ RR )
9 simprrl 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> x e. A )
10 8 9 sseldd 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> x e. RR )
11 3 adantr 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> B e. RR )
12 elicopnf 
 |-  ( B e. RR -> ( z e. ( B [,) +oo ) <-> ( z e. RR /\ B <_ z ) ) )
13 3 12 syl 
 |-  ( ph -> ( z e. ( B [,) +oo ) <-> ( z e. RR /\ B <_ z ) ) )
14 13 biimpa 
 |-  ( ( ph /\ z e. ( B [,) +oo ) ) -> ( z e. RR /\ B <_ z ) )
15 14 adantrr 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> ( z e. RR /\ B <_ z ) )
16 15 simpld 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> z e. RR )
17 15 simprd 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> B <_ z )
18 simprrr 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> z <_ x )
19 11 16 10 17 18 letrd 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> B <_ x )
20 elicopnf 
 |-  ( B e. RR -> ( x e. ( B [,) +oo ) <-> ( x e. RR /\ B <_ x ) ) )
21 11 20 syl 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> ( x e. ( B [,) +oo ) <-> ( x e. RR /\ B <_ x ) ) )
22 10 19 21 mpbir2and 
 |-  ( ( ph /\ ( z e. ( B [,) +oo ) /\ ( x e. A /\ z <_ x ) ) ) -> x e. ( B [,) +oo ) )
23 22 anassrs 
 |-  ( ( ( ph /\ z e. ( B [,) +oo ) ) /\ ( x e. A /\ z <_ x ) ) -> x e. ( B [,) +oo ) )
24 23 anassrs 
 |-  ( ( ( ( ph /\ z e. ( B [,) +oo ) ) /\ x e. A ) /\ z <_ x ) -> x e. ( B [,) +oo ) )
25 biimt 
 |-  ( x e. ( B [,) +oo ) -> ( ( abs ` ( ( F ` x ) - C ) ) < y <-> ( x e. ( B [,) +oo ) -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
26 24 25 syl 
 |-  ( ( ( ( ph /\ z e. ( B [,) +oo ) ) /\ x e. A ) /\ z <_ x ) -> ( ( abs ` ( ( F ` x ) - C ) ) < y <-> ( x e. ( B [,) +oo ) -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
27 26 pm5.74da 
 |-  ( ( ( ph /\ z e. ( B [,) +oo ) ) /\ x e. A ) -> ( ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) <-> ( z <_ x -> ( x e. ( B [,) +oo ) -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) ) )
28 bi2.04 
 |-  ( ( z <_ x -> ( x e. ( B [,) +oo ) -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) <-> ( x e. ( B [,) +oo ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
29 27 28 bitrdi 
 |-  ( ( ( ph /\ z e. ( B [,) +oo ) ) /\ x e. A ) -> ( ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) <-> ( x e. ( B [,) +oo ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) ) )
30 29 pm5.74da 
 |-  ( ( ph /\ z e. ( B [,) +oo ) ) -> ( ( x e. A -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) ) ) )
31 elin 
 |-  ( x e. ( A i^i ( B [,) +oo ) ) <-> ( x e. A /\ x e. ( B [,) +oo ) ) )
32 31 imbi1i 
 |-  ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) <-> ( ( x e. A /\ x e. ( B [,) +oo ) ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
33 impexp 
 |-  ( ( ( x e. A /\ x e. ( B [,) +oo ) ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) ) )
34 32 33 bitri 
 |-  ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) ) )
35 30 34 bitr4di 
 |-  ( ( ph /\ z e. ( B [,) +oo ) ) -> ( ( x e. A -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) <-> ( x e. ( A i^i ( B [,) +oo ) ) -> ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) ) )
36 35 ralbidv2 
 |-  ( ( ph /\ z e. ( B [,) +oo ) ) -> ( A. x e. A ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) <-> A. x e. ( A i^i ( B [,) +oo ) ) ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
37 36 rexbidva 
 |-  ( ph -> ( E. z e. ( B [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) <-> E. z e. ( B [,) +oo ) A. x e. ( A i^i ( B [,) +oo ) ) ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
38 37 ralbidv 
 |-  ( ph -> ( A. y e. RR+ E. z e. ( B [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) <-> A. y e. RR+ E. z e. ( B [,) +oo ) A. x e. ( A i^i ( B [,) +oo ) ) ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
39 38 adantr 
 |-  ( ( ph /\ C e. CC ) -> ( A. y e. RR+ E. z e. ( B [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) <-> A. y e. RR+ E. z e. ( B [,) +oo ) A. x e. ( A i^i ( B [,) +oo ) ) ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
40 1 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. CC )
41 40 ralrimiva 
 |-  ( ph -> A. x e. A ( F ` x ) e. CC )
42 41 adantr 
 |-  ( ( ph /\ C e. CC ) -> A. x e. A ( F ` x ) e. CC )
43 2 adantr 
 |-  ( ( ph /\ C e. CC ) -> A C_ RR )
44 simpr 
 |-  ( ( ph /\ C e. CC ) -> C e. CC )
45 3 adantr 
 |-  ( ( ph /\ C e. CC ) -> B e. RR )
46 42 43 44 45 rlim3 
 |-  ( ( ph /\ C e. CC ) -> ( ( x e. A |-> ( F ` x ) ) ~~>r C <-> A. y e. RR+ E. z e. ( B [,) +oo ) A. x e. A ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
47 elinel1 
 |-  ( x e. ( A i^i ( B [,) +oo ) ) -> x e. A )
48 47 40 sylan2 
 |-  ( ( ph /\ x e. ( A i^i ( B [,) +oo ) ) ) -> ( F ` x ) e. CC )
49 48 ralrimiva 
 |-  ( ph -> A. x e. ( A i^i ( B [,) +oo ) ) ( F ` x ) e. CC )
50 49 adantr 
 |-  ( ( ph /\ C e. CC ) -> A. x e. ( A i^i ( B [,) +oo ) ) ( F ` x ) e. CC )
51 inss1 
 |-  ( A i^i ( B [,) +oo ) ) C_ A
52 51 2 sstrid 
 |-  ( ph -> ( A i^i ( B [,) +oo ) ) C_ RR )
53 52 adantr 
 |-  ( ( ph /\ C e. CC ) -> ( A i^i ( B [,) +oo ) ) C_ RR )
54 50 53 44 45 rlim3 
 |-  ( ( ph /\ C e. CC ) -> ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C <-> A. y e. RR+ E. z e. ( B [,) +oo ) A. x e. ( A i^i ( B [,) +oo ) ) ( z <_ x -> ( abs ` ( ( F ` x ) - C ) ) < y ) ) )
55 39 46 54 3bitr4d 
 |-  ( ( ph /\ C e. CC ) -> ( ( x e. A |-> ( F ` x ) ) ~~>r C <-> ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C ) )
56 55 ex 
 |-  ( ph -> ( C e. CC -> ( ( x e. A |-> ( F ` x ) ) ~~>r C <-> ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C ) ) )
57 5 7 56 pm5.21ndd 
 |-  ( ph -> ( ( x e. A |-> ( F ` x ) ) ~~>r C <-> ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C ) )
58 1 feqmptd 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
59 58 breq1d 
 |-  ( ph -> ( F ~~>r C <-> ( x e. A |-> ( F ` x ) ) ~~>r C ) )
60 resres 
 |-  ( ( F |` A ) |` ( B [,) +oo ) ) = ( F |` ( A i^i ( B [,) +oo ) ) )
61 ffn 
 |-  ( F : A --> CC -> F Fn A )
62 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
63 1 61 62 3syl 
 |-  ( ph -> ( F |` A ) = F )
64 63 reseq1d 
 |-  ( ph -> ( ( F |` A ) |` ( B [,) +oo ) ) = ( F |` ( B [,) +oo ) ) )
65 58 reseq1d 
 |-  ( ph -> ( F |` ( A i^i ( B [,) +oo ) ) ) = ( ( x e. A |-> ( F ` x ) ) |` ( A i^i ( B [,) +oo ) ) ) )
66 resmpt 
 |-  ( ( A i^i ( B [,) +oo ) ) C_ A -> ( ( x e. A |-> ( F ` x ) ) |` ( A i^i ( B [,) +oo ) ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) )
67 51 66 ax-mp 
 |-  ( ( x e. A |-> ( F ` x ) ) |` ( A i^i ( B [,) +oo ) ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) )
68 65 67 eqtrdi 
 |-  ( ph -> ( F |` ( A i^i ( B [,) +oo ) ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) )
69 60 64 68 3eqtr3a 
 |-  ( ph -> ( F |` ( B [,) +oo ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) )
70 69 breq1d 
 |-  ( ph -> ( ( F |` ( B [,) +oo ) ) ~~>r C <-> ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ~~>r C ) )
71 57 59 70 3bitr4d 
 |-  ( ph -> ( F ~~>r C <-> ( F |` ( B [,) +oo ) ) ~~>r C ) )