This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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