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 ) ) ) )