Metamath Proof Explorer


Theorem rlim2lt

Description: Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-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 )
Assertion rlim2lt
|- ( 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 ) ) )

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 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 ) ) )
5 simplr
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> y e. RR )
6 simpl
 |-  ( ( A C_ RR /\ y e. RR ) -> A C_ RR )
7 6 sselda
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> z e. RR )
8 ltle
 |-  ( ( y e. RR /\ z e. RR ) -> ( y < z -> y <_ z ) )
9 5 7 8 syl2anc
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( y < z -> y <_ z ) )
10 9 imim1d
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> ( y < z -> ( abs ` ( B - C ) ) < x ) ) )
11 10 ralimdva
 |-  ( ( A C_ RR /\ y e. RR ) -> ( A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) )
12 2 11 sylan
 |-  ( ( ph /\ y e. RR ) -> ( A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) )
13 12 reximdva
 |-  ( ph -> ( E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) )
14 13 ralimdv
 |-  ( ph -> ( A. x e. RR+ E. y e. RR 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 ) ) )
15 4 14 sylbid
 |-  ( 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 ) ) )
16 peano2re
 |-  ( y e. RR -> ( y + 1 ) e. RR )
17 16 adantl
 |-  ( ( ph /\ y e. RR ) -> ( y + 1 ) e. RR )
18 ltp1
 |-  ( y e. RR -> y < ( y + 1 ) )
19 18 ad2antlr
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> y < ( y + 1 ) )
20 16 ad2antlr
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( y + 1 ) e. RR )
21 ltletr
 |-  ( ( y e. RR /\ ( y + 1 ) e. RR /\ z e. RR ) -> ( ( y < ( y + 1 ) /\ ( y + 1 ) <_ z ) -> y < z ) )
22 5 20 7 21 syl3anc
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y < ( y + 1 ) /\ ( y + 1 ) <_ z ) -> y < z ) )
23 19 22 mpand
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y + 1 ) <_ z -> y < z ) )
24 23 imim1d
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y < z -> ( abs ` ( B - C ) ) < x ) -> ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) )
25 24 ralimdva
 |-  ( ( A C_ RR /\ y e. RR ) -> ( A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) )
26 2 25 sylan
 |-  ( ( ph /\ y e. RR ) -> ( A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) )
27 breq1
 |-  ( w = ( y + 1 ) -> ( w <_ z <-> ( y + 1 ) <_ z ) )
28 27 rspceaimv
 |-  ( ( ( y + 1 ) e. RR /\ A. z e. A ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) -> E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) )
29 17 26 28 syl6an
 |-  ( ( ph /\ y e. RR ) -> ( A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) )
30 29 rexlimdva
 |-  ( ph -> ( E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) )
31 30 ralimdv
 |-  ( ph -> ( A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> A. x e. RR+ E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) )
32 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 ) ) )
33 31 32 sylibrd
 |-  ( ph -> ( A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> ( z e. A |-> B ) ~~>r C ) )
34 15 33 impbid
 |-  ( 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 ) ) )