Metamath Proof Explorer

Theorem ellimcabssub0

Description: An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ellimcabssub0.f 
|- F = ( x e. A |-> B )
ellimcabssub0.g 
|- G = ( x e. A |-> ( B - C ) )
ellimcabssub0.a 
|- ( ph -> A C_ CC )
ellimcabssub0.b 
|- ( ( ph /\ x e. A ) -> B e. CC )
ellimcabssub0.p 
|- ( ph -> D e. CC )
ellimcabssub0.c 
|- ( ph -> C e. CC )
Assertion ellimcabssub0 
|- ( ph -> ( C e. ( F limCC D ) <-> 0 e. ( G limCC D ) ) )

Proof

Step Hyp Ref Expression
1 ellimcabssub0.f 
 |-  F = ( x e. A |-> B )
2 ellimcabssub0.g 
 |-  G = ( x e. A |-> ( B - C ) )
3 ellimcabssub0.a 
 |-  ( ph -> A C_ CC )
4 ellimcabssub0.b 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
5 ellimcabssub0.p 
 |-  ( ph -> D e. CC )
6 ellimcabssub0.c 
 |-  ( ph -> C e. CC )
7 0cnd 
 |-  ( ph -> 0 e. CC )
8 6 7 2thd 
 |-  ( ph -> ( C e. CC <-> 0 e. CC ) )
9 6 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
10 4 9 subcld 
 |-  ( ( ph /\ x e. A ) -> ( B - C ) e. CC )
11 10 2 fmptd 
 |-  ( ph -> G : A --> CC )
12 11 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( G ` z ) e. CC )
13 12 subid1d 
 |-  ( ( ph /\ z e. A ) -> ( ( G ` z ) - 0 ) = ( G ` z ) )
14 simpr 
 |-  ( ( ph /\ z e. A ) -> z e. A )
15 csbov1g 
 |-  ( z e. _V -> [_ z / x ]_ ( B - C ) = ( [_ z / x ]_ B - C ) )
16 15 elv 
 |-  [_ z / x ]_ ( B - C ) = ( [_ z / x ]_ B - C )
17 sban 
 |-  ( [ z / x ] ( ph /\ x e. A ) <-> ( [ z / x ] ph /\ [ z / x ] x e. A ) )
18 nfv 
 |-  F/ x ph
19 18 sbf 
 |-  ( [ z / x ] ph <-> ph )
20 clelsb1 
 |-  ( [ z / x ] x e. A <-> z e. A )
21 19 20 anbi12i 
 |-  ( ( [ z / x ] ph /\ [ z / x ] x e. A ) <-> ( ph /\ z e. A ) )
22 17 21 bitri 
 |-  ( [ z / x ] ( ph /\ x e. A ) <-> ( ph /\ z e. A ) )
23 4 nfth 
 |-  F/ x ( ( ph /\ x e. A ) -> B e. CC )
24 23 sbf 
 |-  ( [ z / x ] ( ( ph /\ x e. A ) -> B e. CC ) <-> ( ( ph /\ x e. A ) -> B e. CC ) )
25 sbim 
 |-  ( [ z / x ] ( ( ph /\ x e. A ) -> B e. CC ) <-> ( [ z / x ] ( ph /\ x e. A ) -> [ z / x ] B e. CC ) )
26 24 25 sylbb1 
 |-  ( ( ( ph /\ x e. A ) -> B e. CC ) -> ( [ z / x ] ( ph /\ x e. A ) -> [ z / x ] B e. CC ) )
27 22 26 syl5bir 
 |-  ( ( ( ph /\ x e. A ) -> B e. CC ) -> ( ( ph /\ z e. A ) -> [ z / x ] B e. CC ) )
28 4 27 ax-mp 
 |-  ( ( ph /\ z e. A ) -> [ z / x ] B e. CC )
29 sbsbc 
 |-  ( [ z / x ] B e. CC <-> [. z / x ]. B e. CC )
30 sbcel1g 
 |-  ( z e. _V -> ( [. z / x ]. B e. CC <-> [_ z / x ]_ B e. CC ) )
31 30 elv 
 |-  ( [. z / x ]. B e. CC <-> [_ z / x ]_ B e. CC )
32 29 31 bitri 
 |-  ( [ z / x ] B e. CC <-> [_ z / x ]_ B e. CC )
33 28 32 sylib 
 |-  ( ( ph /\ z e. A ) -> [_ z / x ]_ B e. CC )
34 6 adantr 
 |-  ( ( ph /\ z e. A ) -> C e. CC )
35 33 34 subcld 
 |-  ( ( ph /\ z e. A ) -> ( [_ z / x ]_ B - C ) e. CC )
36 16 35 eqeltrid 
 |-  ( ( ph /\ z e. A ) -> [_ z / x ]_ ( B - C ) e. CC )
37 2 fvmpts 
 |-  ( ( z e. A /\ [_ z / x ]_ ( B - C ) e. CC ) -> ( G ` z ) = [_ z / x ]_ ( B - C ) )
38 14 36 37 syl2anc 
 |-  ( ( ph /\ z e. A ) -> ( G ` z ) = [_ z / x ]_ ( B - C ) )
39 1 fvmpts 
 |-  ( ( z e. A /\ [_ z / x ]_ B e. CC ) -> ( F ` z ) = [_ z / x ]_ B )
40 14 33 39 syl2anc 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) = [_ z / x ]_ B )
41 40 oveq1d 
 |-  ( ( ph /\ z e. A ) -> ( ( F ` z ) - C ) = ( [_ z / x ]_ B - C ) )
42 16 41 eqtr4id 
 |-  ( ( ph /\ z e. A ) -> [_ z / x ]_ ( B - C ) = ( ( F ` z ) - C ) )
43 13 38 42 3eqtrrd 
 |-  ( ( ph /\ z e. A ) -> ( ( F ` z ) - C ) = ( ( G ` z ) - 0 ) )
44 43 fveq2d 
 |-  ( ( ph /\ z e. A ) -> ( abs ` ( ( F ` z ) - C ) ) = ( abs ` ( ( G ` z ) - 0 ) ) )
45 44 breq1d 
 |-  ( ( ph /\ z e. A ) -> ( ( abs ` ( ( F ` z ) - C ) ) < y <-> ( abs ` ( ( G ` z ) - 0 ) ) < y ) )
46 45 imbi2d 
 |-  ( ( ph /\ z e. A ) -> ( ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( F ` z ) - C ) ) < y ) <-> ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( G ` z ) - 0 ) ) < y ) ) )
47 46 ralbidva 
 |-  ( ph -> ( A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( F ` z ) - C ) ) < y ) <-> A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( G ` z ) - 0 ) ) < y ) ) )
48 47 rexbidv 
 |-  ( ph -> ( E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( F ` z ) - C ) ) < y ) <-> E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( G ` z ) - 0 ) ) < y ) ) )
49 48 ralbidv 
 |-  ( ph -> ( A. y e. RR+ E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( F ` z ) - C ) ) < y ) <-> A. y e. RR+ E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( G ` z ) - 0 ) ) < y ) ) )
50 8 49 anbi12d 
 |-  ( ph -> ( ( C e. CC /\ A. y e. RR+ E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( F ` z ) - C ) ) < y ) ) <-> ( 0 e. CC /\ A. y e. RR+ E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( G ` z ) - 0 ) ) < y ) ) ) )
51 4 1 fmptd 
 |-  ( ph -> F : A --> CC )
52 51 3 5 ellimc3 
 |-  ( ph -> ( C e. ( F limCC D ) <-> ( C e. CC /\ A. y e. RR+ E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( F ` z ) - C ) ) < y ) ) ) )
53 11 3 5 ellimc3 
 |-  ( ph -> ( 0 e. ( G limCC D ) <-> ( 0 e. CC /\ A. y e. RR+ E. w e. RR+ A. z e. A ( ( z =/= D /\ ( abs ` ( z - D ) ) < w ) -> ( abs ` ( ( G ` z ) - 0 ) ) < y ) ) ) )
54 50 52 53 3bitr4d 
 |-  ( ph -> ( C e. ( F limCC D ) <-> 0 e. ( G limCC D ) ) )