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 ) ) )