Metamath Proof Explorer

Theorem climuzlem

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 climuzlem.1 
|- ( ph -> M e. ZZ )
climuzlem.2 
|- Z = ( ZZ>= ` M )
climuzlem.3 
|- ( ph -> F : Z --> CC )
Assertion climuzlem 
|- ( 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 climuzlem.1 
 |-  ( ph -> M e. ZZ )
2 climuzlem.2 
 |-  Z = ( ZZ>= ` M )
3 climuzlem.3 
 |-  ( ph -> F : Z --> CC )
4 climcl 
 |-  ( F ~~> A -> A e. CC )
5 4 adantl 
 |-  ( ( ph /\ F ~~> A ) -> A e. CC )
6 id 
 |-  ( F ~~> A -> F ~~> A )
7 climrel 
 |-  Rel ~~>
8 7 brrelex1i 
 |-  ( F ~~> A -> F e. _V )
9 eqidd 
 |-  ( ( F ~~> A /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
10 8 9 clim 
 |-  ( F ~~> A -> ( 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 ) ) ) )
11 6 10 mpbid 
 |-  ( 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 ) ) )
12 11 simprd 
 |-  ( F ~~> A -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
13 12 adantl 
 |-  ( ( ph /\ F ~~> A ) -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
14 simpr 
 |-  ( ( 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 ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
15 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
16 1 15 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
17 16 adantr 
 |-  ( ( ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
18 14 17 mpbird 
 |-  ( ( ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
19 simpr 
 |-  ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> ( abs ` ( ( F ` k ) - A ) ) < x )
20 19 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
21 20 reximi 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
22 21 a1i 
 |-  ( ( ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
23 18 22 mpd 
 |-  ( ( ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
24 23 ex 
 |-  ( ph -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
25 24 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
26 25 ralimdva 
 |-  ( 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. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
27 26 adantr 
 |-  ( ( ph /\ F ~~> A ) -> ( 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. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
28 13 27 mpd 
 |-  ( ( ph /\ F ~~> A ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
29 5 28 jca 
 |-  ( ( ph /\ F ~~> A ) -> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
30 simprl 
 |-  ( ( ph /\ ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> A e. CC )
31 nfv 
 |-  F/ j ph
32 nfre1 
 |-  F/ j E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x )
33 2 uzssz2 
 |-  Z C_ ZZ
34 33 sseli 
 |-  ( j e. Z -> j e. ZZ )
35 34 3ad2ant2 
 |-  ( ( ph /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) -> j e. ZZ )
36 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ph )
37 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
38 37 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
39 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
40 36 38 39 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
41 40 adantr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> ( F ` k ) e. CC )
42 simpr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> ( abs ` ( ( F ` k ) - A ) ) < x )
43 41 42 jca 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < x ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
44 43 ex 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
45 44 ralimdva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
46 45 3impia 
 |-  ( ( ph /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
47 rspe 
 |-  ( ( 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 ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
48 35 46 47 syl2anc 
 |-  ( ( ph /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
49 48 3exp 
 |-  ( ph -> ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
50 31 32 49 rexlimd 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
51 50 ralimdv 
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
52 51 imp 
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
53 52 adantrl 
 |-  ( ( ph /\ ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
54 30 53 jca 
 |-  ( ( ph /\ ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < 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 ) ) )
55 2 fvexi 
 |-  Z e. _V
56 55 a1i 
 |-  ( ph -> Z e. _V )
57 3 56 fexd 
 |-  ( ph -> F e. _V )
58 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
59 57 58 clim 
 |-  ( 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 ) ) ) )
60 59 adantr 
 |-  ( ( ph /\ ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> ( 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 ) ) ) )
61 54 60 mpbird 
 |-  ( ( ph /\ ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) -> F ~~> A )
62 29 61 impbida 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) ) )