Metamath Proof Explorer

Theorem climuz

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climuz.k 
|- F/_ k F
climuz.m 
|- ( ph -> M e. ZZ )
climuz.z 
|- Z = ( ZZ>= ` M )
climuz.f 
|- ( ph -> F : Z --> CC )
Assertion climuz 
|- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) )

Proof

Step Hyp Ref Expression
1 climuz.k 
 |-  F/_ k F
2 climuz.m 
 |-  ( ph -> M e. ZZ )
3 climuz.z 
 |-  Z = ( ZZ>= ` M )
4 climuz.f 
 |-  ( ph -> F : Z --> CC )
5 2 3 4 climuzlem 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. y e. RR+ E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y ) ) )
6 breq2 
 |-  ( y = x -> ( ( abs ` ( ( F ` l ) - A ) ) < y <-> ( abs ` ( ( F ` l ) - A ) ) < x ) )
7 6 ralbidv 
 |-  ( y = x -> ( A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y <-> A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < x ) )
8 7 rexbidv 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y <-> E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < x ) )
9 fveq2 
 |-  ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
10 9 raleqdv 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < x <-> A. l e. ( ZZ>= ` j ) ( abs ` ( ( F ` l ) - A ) ) < x ) )
11 nfcv 
 |-  F/_ k abs
12 nfcv 
 |-  F/_ k l
13 1 12 nffv 
 |-  F/_ k ( F ` l )
14 nfcv 
 |-  F/_ k -
15 nfcv 
 |-  F/_ k A
16 13 14 15 nfov 
 |-  F/_ k ( ( F ` l ) - A )
17 11 16 nffv 
 |-  F/_ k ( abs ` ( ( F ` l ) - A ) )
18 nfcv 
 |-  F/_ k <
19 nfcv 
 |-  F/_ k x
20 17 18 19 nfbr 
 |-  F/ k ( abs ` ( ( F ` l ) - A ) ) < x
21 nfv 
 |-  F/ l ( abs ` ( ( F ` k ) - A ) ) < x
22 fveq2 
 |-  ( l = k -> ( F ` l ) = ( F ` k ) )
23 22 fvoveq1d 
 |-  ( l = k -> ( abs ` ( ( F ` l ) - A ) ) = ( abs ` ( ( F ` k ) - A ) ) )
24 23 breq1d 
 |-  ( l = k -> ( ( abs ` ( ( F ` l ) - A ) ) < x <-> ( abs ` ( ( F ` k ) - A ) ) < x ) )
25 20 21 24 cbvralw 
 |-  ( A. l e. ( ZZ>= ` j ) ( abs ` ( ( F ` l ) - A ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
26 25 a1i 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` j ) ( abs ` ( ( F ` l ) - A ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
27 10 26 bitrd 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
28 27 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
29 28 a1i 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
30 8 29 bitrd 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
31 30 cbvralvw 
 |-  ( A. y e. RR+ E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
32 31 anbi2i 
 |-  ( ( A e. CC /\ A. y e. RR+ E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y ) <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
33 32 a1i 
 |-  ( ph -> ( ( A e. CC /\ A. y e. RR+ E. i e. Z A. l e. ( ZZ>= ` i ) ( abs ` ( ( F ` l ) - A ) ) < y ) <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
34 5 33 bitrd 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) )