Metamath Proof Explorer

Theorem rlimconst

Description: A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion rlimconst 
|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) ~~>r B )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 simpllr 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> B e. CC )
3 2 subidd 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> ( B - B ) = 0 )
4 3 fveq2d 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> ( abs ` ( B - B ) ) = ( abs ` 0 ) )
5 abs0 
 |-  ( abs ` 0 ) = 0
6 4 5 eqtrdi 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> ( abs ` ( B - B ) ) = 0 )
7 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
8 7 ad2antlr 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> 0 < y )
9 6 8 eqbrtrd 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> ( abs ` ( B - B ) ) < y )
10 9 a1d 
 |-  ( ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) /\ x e. A ) -> ( 0 <_ x -> ( abs ` ( B - B ) ) < y ) )
11 10 ralrimiva 
 |-  ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) -> A. x e. A ( 0 <_ x -> ( abs ` ( B - B ) ) < y ) )
12 breq1 
 |-  ( z = 0 -> ( z <_ x <-> 0 <_ x ) )
13 12 rspceaimv 
 |-  ( ( 0 e. RR /\ A. x e. A ( 0 <_ x -> ( abs ` ( B - B ) ) < y ) ) -> E. z e. RR A. x e. A ( z <_ x -> ( abs ` ( B - B ) ) < y ) )
14 1 11 13 sylancr 
 |-  ( ( ( A C_ RR /\ B e. CC ) /\ y e. RR+ ) -> E. z e. RR A. x e. A ( z <_ x -> ( abs ` ( B - B ) ) < y ) )
15 14 ralrimiva 
 |-  ( ( A C_ RR /\ B e. CC ) -> A. y e. RR+ E. z e. RR A. x e. A ( z <_ x -> ( abs ` ( B - B ) ) < y ) )
16 simplr 
 |-  ( ( ( A C_ RR /\ B e. CC ) /\ x e. A ) -> B e. CC )
17 16 ralrimiva 
 |-  ( ( A C_ RR /\ B e. CC ) -> A. x e. A B e. CC )
18 simpl 
 |-  ( ( A C_ RR /\ B e. CC ) -> A C_ RR )
19 simpr 
 |-  ( ( A C_ RR /\ B e. CC ) -> B e. CC )
20 17 18 19 rlim2 
 |-  ( ( A C_ RR /\ B e. CC ) -> ( ( x e. A |-> B ) ~~>r B <-> A. y e. RR+ E. z e. RR A. x e. A ( z <_ x -> ( abs ` ( B - B ) ) < y ) ) )
21 15 20 mpbird 
 |-  ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) ~~>r B )