Metamath Proof Explorer

Theorem constlimc

Description: Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses constlimc.f 
|- F = ( x e. A |-> B )
constlimc.a 
|- ( ph -> A C_ CC )
constlimc.b 
|- ( ph -> B e. CC )
constlimc.c 
|- ( ph -> C e. CC )
Assertion constlimc 
|- ( ph -> B e. ( F limCC C ) )

Proof

Step Hyp Ref Expression
1 constlimc.f 
 |-  F = ( x e. A |-> B )
2 constlimc.a 
 |-  ( ph -> A C_ CC )
3 constlimc.b 
 |-  ( ph -> B e. CC )
4 constlimc.c 
 |-  ( ph -> C e. CC )
5 1rp 
 |-  1 e. RR+
6 5 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> 1 e. RR+ )
7 simpr 
 |-  ( ( ph /\ v e. A ) -> v e. A )
8 vex 
 |-  v e. _V
9 nfcv 
 |-  F/_ x B
10 csbtt 
 |-  ( ( v e. _V /\ F/_ x B ) -> [_ v / x ]_ B = B )
11 8 9 10 mp2an 
 |-  [_ v / x ]_ B = B
12 11 3 eqeltrid 
 |-  ( ph -> [_ v / x ]_ B e. CC )
13 12 adantr 
 |-  ( ( ph /\ v e. A ) -> [_ v / x ]_ B e. CC )
14 1 fvmpts 
 |-  ( ( v e. A /\ [_ v / x ]_ B e. CC ) -> ( F ` v ) = [_ v / x ]_ B )
15 7 13 14 syl2anc 
 |-  ( ( ph /\ v e. A ) -> ( F ` v ) = [_ v / x ]_ B )
16 15 oveq1d 
 |-  ( ( ph /\ v e. A ) -> ( ( F ` v ) - B ) = ( [_ v / x ]_ B - B ) )
17 11 oveq1i 
 |-  ( [_ v / x ]_ B - B ) = ( B - B )
18 16 17 eqtrdi 
 |-  ( ( ph /\ v e. A ) -> ( ( F ` v ) - B ) = ( B - B ) )
19 18 fveq2d 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( F ` v ) - B ) ) = ( abs ` ( B - B ) ) )
20 3 subidd 
 |-  ( ph -> ( B - B ) = 0 )
21 20 fveq2d 
 |-  ( ph -> ( abs ` ( B - B ) ) = ( abs ` 0 ) )
22 21 adantr 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( B - B ) ) = ( abs ` 0 ) )
23 abs0 
 |-  ( abs ` 0 ) = 0
24 23 a1i 
 |-  ( ( ph /\ v e. A ) -> ( abs ` 0 ) = 0 )
25 19 22 24 3eqtrd 
 |-  ( ( ph /\ v e. A ) -> ( abs ` ( ( F ` v ) - B ) ) = 0 )
26 25 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( abs ` ( ( F ` v ) - B ) ) = 0 )
27 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
28 27 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> 0 < y )
29 26 28 eqbrtrd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( abs ` ( ( F ` v ) - B ) ) < y )
30 29 a1d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ v e. A ) -> ( ( v =/= C /\ ( abs ` ( v - C ) ) < 1 ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) )
31 30 ralrimiva 
 |-  ( ( ph /\ y e. RR+ ) -> A. v e. A ( ( v =/= C /\ ( abs ` ( v - C ) ) < 1 ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) )
32 brimralrspcev 
 |-  ( ( 1 e. RR+ /\ A. v e. A ( ( v =/= C /\ ( abs ` ( v - C ) ) < 1 ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) ) -> E. w e. RR+ A. v e. A ( ( v =/= C /\ ( abs ` ( v - C ) ) < w ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) )
33 6 31 32 syl2anc 
 |-  ( ( ph /\ y e. RR+ ) -> E. w e. RR+ A. v e. A ( ( v =/= C /\ ( abs ` ( v - C ) ) < w ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) )
34 33 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= C /\ ( abs ` ( v - C ) ) < w ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) )
35 3 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
36 35 1 fmptd 
 |-  ( ph -> F : A --> CC )
37 36 2 4 ellimc3 
 |-  ( ph -> ( B e. ( F limCC C ) <-> ( B e. CC /\ A. y e. RR+ E. w e. RR+ A. v e. A ( ( v =/= C /\ ( abs ` ( v - C ) ) < w ) -> ( abs ` ( ( F ` v ) - B ) ) < y ) ) ) )
38 3 34 37 mpbir2and 
 |-  ( ph -> B e. ( F limCC C ) )