Metamath Proof Explorer


Theorem rlim

Description: Express the predicate: The limit of complex number function F is C , or F converges to C , in the real sense. This means that for any real x , no matter how small, there always exists a number y such that the absolute difference of any number in the function beyond y and the limit is less than x . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypotheses rlim.1
|- ( ph -> F : A --> CC )
rlim.2
|- ( ph -> A C_ RR )
rlim.4
|- ( ( ph /\ z e. A ) -> ( F ` z ) = B )
Assertion rlim
|- ( ph -> ( F ~~>r C <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) )

Proof

Step Hyp Ref Expression
1 rlim.1
 |-  ( ph -> F : A --> CC )
2 rlim.2
 |-  ( ph -> A C_ RR )
3 rlim.4
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) = B )
4 rlimrel
 |-  Rel ~~>r
5 4 brrelex2i
 |-  ( F ~~>r C -> C e. _V )
6 5 a1i
 |-  ( ph -> ( F ~~>r C -> C e. _V ) )
7 elex
 |-  ( C e. CC -> C e. _V )
8 7 ad2antrl
 |-  ( ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) -> C e. _V )
9 8 a1i
 |-  ( ph -> ( ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) -> C e. _V ) )
10 cnex
 |-  CC e. _V
11 reex
 |-  RR e. _V
12 elpm2r
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
13 10 11 12 mpanl12
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
14 1 2 13 syl2anc
 |-  ( ph -> F e. ( CC ^pm RR ) )
15 eleq1
 |-  ( f = F -> ( f e. ( CC ^pm RR ) <-> F e. ( CC ^pm RR ) ) )
16 eleq1
 |-  ( w = C -> ( w e. CC <-> C e. CC ) )
17 15 16 bi2anan9
 |-  ( ( f = F /\ w = C ) -> ( ( f e. ( CC ^pm RR ) /\ w e. CC ) <-> ( F e. ( CC ^pm RR ) /\ C e. CC ) ) )
18 simpl
 |-  ( ( f = F /\ w = C ) -> f = F )
19 18 dmeqd
 |-  ( ( f = F /\ w = C ) -> dom f = dom F )
20 fveq1
 |-  ( f = F -> ( f ` z ) = ( F ` z ) )
21 oveq12
 |-  ( ( ( f ` z ) = ( F ` z ) /\ w = C ) -> ( ( f ` z ) - w ) = ( ( F ` z ) - C ) )
22 20 21 sylan
 |-  ( ( f = F /\ w = C ) -> ( ( f ` z ) - w ) = ( ( F ` z ) - C ) )
23 22 fveq2d
 |-  ( ( f = F /\ w = C ) -> ( abs ` ( ( f ` z ) - w ) ) = ( abs ` ( ( F ` z ) - C ) ) )
24 23 breq1d
 |-  ( ( f = F /\ w = C ) -> ( ( abs ` ( ( f ` z ) - w ) ) < x <-> ( abs ` ( ( F ` z ) - C ) ) < x ) )
25 24 imbi2d
 |-  ( ( f = F /\ w = C ) -> ( ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
26 19 25 raleqbidv
 |-  ( ( f = F /\ w = C ) -> ( A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
27 26 rexbidv
 |-  ( ( f = F /\ w = C ) -> ( E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
28 27 ralbidv
 |-  ( ( f = F /\ w = C ) -> ( A. x e. RR+ E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
29 17 28 anbi12d
 |-  ( ( f = F /\ w = C ) -> ( ( ( f e. ( CC ^pm RR ) /\ w e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) ) <-> ( ( F e. ( CC ^pm RR ) /\ C e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
30 df-rlim
 |-  ~~>r = { <. f , w >. | ( ( f e. ( CC ^pm RR ) /\ w e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) ) }
31 29 30 brabga
 |-  ( ( F e. ( CC ^pm RR ) /\ C e. _V ) -> ( F ~~>r C <-> ( ( F e. ( CC ^pm RR ) /\ C e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
32 anass
 |-  ( ( ( F e. ( CC ^pm RR ) /\ C e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
33 31 32 bitrdi
 |-  ( ( F e. ( CC ^pm RR ) /\ C e. _V ) -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) )
34 33 ex
 |-  ( F e. ( CC ^pm RR ) -> ( C e. _V -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) )
35 14 34 syl
 |-  ( ph -> ( C e. _V -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) )
36 6 9 35 pm5.21ndd
 |-  ( ph -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) )
37 14 biantrurd
 |-  ( ph -> ( ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) )
38 1 fdmd
 |-  ( ph -> dom F = A )
39 38 raleqdv
 |-  ( ph -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
40 3 fvoveq1d
 |-  ( ( ph /\ z e. A ) -> ( abs ` ( ( F ` z ) - C ) ) = ( abs ` ( B - C ) ) )
41 40 breq1d
 |-  ( ( ph /\ z e. A ) -> ( ( abs ` ( ( F ` z ) - C ) ) < x <-> ( abs ` ( B - C ) ) < x ) )
42 41 imbi2d
 |-  ( ( ph /\ z e. A ) -> ( ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
43 42 ralbidva
 |-  ( ph -> ( A. z e. A ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
44 39 43 bitrd
 |-  ( ph -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
45 44 rexbidv
 |-  ( ph -> ( E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
46 45 ralbidv
 |-  ( ph -> ( A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
47 46 anbi2d
 |-  ( ph -> ( ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) )
48 36 37 47 3bitr2d
 |-  ( ph -> ( F ~~>r C <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) )