Metamath Proof Explorer

Theorem rlim3

Description: Restrict the range of the domain bound to reals greater than some D e. RR . (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlim2.1 
|- ( ph -> A. z e. A B e. CC )
rlim2.2 
|- ( ph -> A C_ RR )
rlim2.3 
|- ( ph -> C e. CC )
rlim3.4 
|- ( ph -> D e. RR )
Assertion rlim3 
|- ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )

Proof

Step Hyp Ref Expression
1 rlim2.1 
 |-  ( ph -> A. z e. A B e. CC )
2 rlim2.2 
 |-  ( ph -> A C_ RR )
3 rlim2.3 
 |-  ( ph -> C e. CC )
4 rlim3.4 
 |-  ( ph -> D e. RR )
5 1 2 3 rlim2 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) )
6 simpr 
 |-  ( ( ph /\ w e. RR ) -> w e. RR )
7 4 adantr 
 |-  ( ( ph /\ w e. RR ) -> D e. RR )
8 6 7 ifcld 
 |-  ( ( ph /\ w e. RR ) -> if ( D <_ w , w , D ) e. RR )
9 max1 
 |-  ( ( D e. RR /\ w e. RR ) -> D <_ if ( D <_ w , w , D ) )
10 4 9 sylan 
 |-  ( ( ph /\ w e. RR ) -> D <_ if ( D <_ w , w , D ) )
11 elicopnf 
 |-  ( D e. RR -> ( if ( D <_ w , w , D ) e. ( D [,) +oo ) <-> ( if ( D <_ w , w , D ) e. RR /\ D <_ if ( D <_ w , w , D ) ) ) )
12 7 11 syl 
 |-  ( ( ph /\ w e. RR ) -> ( if ( D <_ w , w , D ) e. ( D [,) +oo ) <-> ( if ( D <_ w , w , D ) e. RR /\ D <_ if ( D <_ w , w , D ) ) ) )
13 8 10 12 mpbir2and 
 |-  ( ( ph /\ w e. RR ) -> if ( D <_ w , w , D ) e. ( D [,) +oo ) )
14 2 4 jca 
 |-  ( ph -> ( A C_ RR /\ D e. RR ) )
15 max2 
 |-  ( ( D e. RR /\ w e. RR ) -> w <_ if ( D <_ w , w , D ) )
16 15 ad4ant23 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> w <_ if ( D <_ w , w , D ) )
17 simplr 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> w e. RR )
18 simpllr 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> D e. RR )
19 17 18 ifcld 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> if ( D <_ w , w , D ) e. RR )
20 simpll 
 |-  ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) -> A C_ RR )
21 20 sselda 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> z e. RR )
22 letr 
 |-  ( ( w e. RR /\ if ( D <_ w , w , D ) e. RR /\ z e. RR ) -> ( ( w <_ if ( D <_ w , w , D ) /\ if ( D <_ w , w , D ) <_ z ) -> w <_ z ) )
23 17 19 21 22 syl3anc 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> ( ( w <_ if ( D <_ w , w , D ) /\ if ( D <_ w , w , D ) <_ z ) -> w <_ z ) )
24 16 23 mpand 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> ( if ( D <_ w , w , D ) <_ z -> w <_ z ) )
25 24 imim1d 
 |-  ( ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) /\ z e. A ) -> ( ( w <_ z -> ( abs ` ( B - C ) ) < x ) -> ( if ( D <_ w , w , D ) <_ z -> ( abs ` ( B - C ) ) < x ) ) )
26 25 ralimdva 
 |-  ( ( ( A C_ RR /\ D e. RR ) /\ w e. RR ) -> ( A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( if ( D <_ w , w , D ) <_ z -> ( abs ` ( B - C ) ) < x ) ) )
27 14 26 sylan 
 |-  ( ( ph /\ w e. RR ) -> ( A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( if ( D <_ w , w , D ) <_ z -> ( abs ` ( B - C ) ) < x ) ) )
28 breq1 
 |-  ( y = if ( D <_ w , w , D ) -> ( y <_ z <-> if ( D <_ w , w , D ) <_ z ) )
29 28 rspceaimv 
 |-  ( ( if ( D <_ w , w , D ) e. ( D [,) +oo ) /\ A. z e. A ( if ( D <_ w , w , D ) <_ z -> ( abs ` ( B - C ) ) < x ) ) -> E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) )
30 13 27 29 syl6an 
 |-  ( ( ph /\ w e. RR ) -> ( A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) -> E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
31 30 rexlimdva 
 |-  ( ph -> ( E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) -> E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
32 31 ralimdv 
 |-  ( ph -> ( A. x e. RR+ E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) -> A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
33 5 32 sylbid 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C -> A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
34 pnfxr 
 |-  +oo e. RR*
35 icossre 
 |-  ( ( D e. RR /\ +oo e. RR* ) -> ( D [,) +oo ) C_ RR )
36 4 34 35 sylancl 
 |-  ( ph -> ( D [,) +oo ) C_ RR )
37 ssrexv 
 |-  ( ( D [,) +oo ) C_ RR -> ( E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
38 36 37 syl 
 |-  ( ph -> ( E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
39 38 ralimdv 
 |-  ( ph -> ( A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
40 1 2 3 rlim2 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
41 39 40 sylibrd 
 |-  ( ph -> ( A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> ( z e. A |-> B ) ~~>r C ) )
42 33 41 impbid 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. ( D [,) +oo ) A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )