Metamath Proof Explorer

Theorem climf

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . Similar to clim , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses climf.nf 
|- F/_ k F
climf.f 
|- ( ph -> F e. V )
climf.fv 
|- ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )
Assertion climf 
|- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )

Proof

Step Hyp Ref Expression
1 climf.nf 
 |-  F/_ k F
2 climf.f 
 |-  ( ph -> F e. V )
3 climf.fv 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )
4 climrel 
 |-  Rel ~~>
5 4 brrelex2i 
 |-  ( F ~~> A -> A e. _V )
6 5 a1i 
 |-  ( ph -> ( F ~~> A -> A e. _V ) )
7 elex 
 |-  ( A e. CC -> A e. _V )
8 7 adantr 
 |-  ( ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> A e. _V )
9 8 a1i 
 |-  ( ph -> ( ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> A e. _V ) )
10 simpr 
 |-  ( ( f = F /\ y = A ) -> y = A )
11 10 eleq1d 
 |-  ( ( f = F /\ y = A ) -> ( y e. CC <-> A e. CC ) )
12 nfv 
 |-  F/ x ( f = F /\ y = A )
13 1 nfeq2 
 |-  F/ k f = F
14 nfv 
 |-  F/ k y = A
15 13 14 nfan 
 |-  F/ k ( f = F /\ y = A )
16 fveq1 
 |-  ( f = F -> ( f ` k ) = ( F ` k ) )
17 16 adantr 
 |-  ( ( f = F /\ y = A ) -> ( f ` k ) = ( F ` k ) )
18 17 eleq1d 
 |-  ( ( f = F /\ y = A ) -> ( ( f ` k ) e. CC <-> ( F ` k ) e. CC ) )
19 oveq12 
 |-  ( ( ( f ` k ) = ( F ` k ) /\ y = A ) -> ( ( f ` k ) - y ) = ( ( F ` k ) - A ) )
20 16 19 sylan 
 |-  ( ( f = F /\ y = A ) -> ( ( f ` k ) - y ) = ( ( F ` k ) - A ) )
21 20 fveq2d 
 |-  ( ( f = F /\ y = A ) -> ( abs ` ( ( f ` k ) - y ) ) = ( abs ` ( ( F ` k ) - A ) ) )
22 21 breq1d 
 |-  ( ( f = F /\ y = A ) -> ( ( abs ` ( ( f ` k ) - y ) ) < x <-> ( abs ` ( ( F ` k ) - A ) ) < x ) )
23 18 22 anbi12d 
 |-  ( ( f = F /\ y = A ) -> ( ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
24 15 23 ralbid 
 |-  ( ( f = F /\ y = A ) -> ( A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
25 24 rexbidv 
 |-  ( ( f = F /\ y = A ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
26 12 25 ralbid 
 |-  ( ( f = F /\ y = A ) -> ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
27 11 26 anbi12d 
 |-  ( ( f = F /\ y = A ) -> ( ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
28 df-clim 
 |-  ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }
29 27 28 brabga 
 |-  ( ( F e. V /\ A e. _V ) -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
30 29 ex 
 |-  ( F e. V -> ( A e. _V -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) ) )
31 2 30 syl 
 |-  ( ph -> ( A e. _V -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) ) )
32 6 9 31 pm5.21ndd 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
33 eluzelz 
 |-  ( k e. ( ZZ>= ` j ) -> k e. ZZ )
34 3 eleq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( F ` k ) e. CC <-> B e. CC ) )
35 3 fvoveq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( B - A ) ) )
36 35 breq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( B - A ) ) < x ) )
37 34 36 anbi12d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
38 33 37 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
39 38 ralbidva 
 |-  ( ph -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
40 39 rexbidv 
 |-  ( ph -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
41 40 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
42 41 anbi2d 
 |-  ( ph -> ( ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
43 32 42 bitrd 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )