Metamath Proof Explorer

Theorem climf2

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 ph k and F k . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climf2.1 
|- F/ k ph
climf2.nf 
|- F/_ k F
climf2.f 
|- ( ph -> F e. V )
climf2.fv 
|- ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )
Assertion climf2 
|- ( 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 climf2.1 
 |-  F/ k ph
2 climf2.nf 
 |-  F/_ k F
3 climf2.f 
 |-  ( ph -> F e. V )
4 climf2.fv 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )
5 climrel 
 |-  Rel ~~>
6 5 brrelex2i 
 |-  ( F ~~> A -> A e. _V )
7 6 a1i 
 |-  ( ph -> ( F ~~> A -> A e. _V ) )
8 elex 
 |-  ( A e. CC -> A e. _V )
9 8 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 )
10 9 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 ) )
11 simpr 
 |-  ( ( f = F /\ y = A ) -> y = A )
12 11 eleq1d 
 |-  ( ( f = F /\ y = A ) -> ( y e. CC <-> A e. CC ) )
13 nfv 
 |-  F/ x ( f = F /\ y = A )
14 2 nfeq2 
 |-  F/ k f = F
15 nfv 
 |-  F/ k y = A
16 14 15 nfan 
 |-  F/ k ( f = F /\ y = A )
17 fveq1 
 |-  ( f = F -> ( f ` k ) = ( F ` k ) )
18 17 adantr 
 |-  ( ( f = F /\ y = A ) -> ( f ` k ) = ( F ` k ) )
19 18 eleq1d 
 |-  ( ( f = F /\ y = A ) -> ( ( f ` k ) e. CC <-> ( F ` k ) e. CC ) )
20 oveq12 
 |-  ( ( ( f ` k ) = ( F ` k ) /\ y = A ) -> ( ( f ` k ) - y ) = ( ( F ` k ) - A ) )
21 17 20 sylan 
 |-  ( ( f = F /\ y = A ) -> ( ( f ` k ) - y ) = ( ( F ` k ) - A ) )
22 21 fveq2d 
 |-  ( ( f = F /\ y = A ) -> ( abs ` ( ( f ` k ) - y ) ) = ( abs ` ( ( F ` k ) - A ) ) )
23 22 breq1d 
 |-  ( ( f = F /\ y = A ) -> ( ( abs ` ( ( f ` k ) - y ) ) < x <-> ( abs ` ( ( F ` k ) - A ) ) < x ) )
24 19 23 anbi12d 
 |-  ( ( f = F /\ y = A ) -> ( ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
25 16 24 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 ) ) )
26 25 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 ) ) )
27 13 26 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 ) ) )
28 12 27 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 ) ) ) )
29 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 ) ) }
30 28 29 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 ) ) ) )
31 30 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 ) ) ) ) )
32 3 31 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 ) ) ) ) )
33 7 10 32 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 ) ) ) )
34 eluzelz 
 |-  ( k e. ( ZZ>= ` j ) -> k e. ZZ )
35 4 eleq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( F ` k ) e. CC <-> B e. CC ) )
36 4 fvoveq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( B - A ) ) )
37 36 breq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( B - A ) ) < x ) )
38 35 37 anbi12d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
39 34 38 sylan2 
 |-  ( ( ph /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) )
40 1 39 ralbida 
 |-  ( 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 ) ) )
41 40 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 ) ) )
42 41 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 ) ) )
43 42 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 ) ) ) )
44 33 43 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 ) ) ) )