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 )