Metamath Proof Explorer

Theorem climleltrp

Description: The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climleltrp.k 
|- F/ k ph
climleltrp.f 
|- F/_ k F
climleltrp.z 
|- Z = ( ZZ>= ` M )
climleltrp.n 
|- ( ph -> N e. Z )
climleltrp.r 
|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. RR )
climleltrp.a 
|- ( ph -> F ~~> A )
climleltrp.c 
|- ( ph -> C e. RR )
climleltrp.l 
|- ( ph -> A <_ C )
climleltrp.x 
|- ( ph -> X e. RR+ )
Assertion climleltrp 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )

Proof

Step Hyp Ref Expression
1 climleltrp.k 
 |-  F/ k ph
2 climleltrp.f 
 |-  F/_ k F
3 climleltrp.z 
 |-  Z = ( ZZ>= ` M )
4 climleltrp.n 
 |-  ( ph -> N e. Z )
5 climleltrp.r 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. RR )
6 climleltrp.a 
 |-  ( ph -> F ~~> A )
7 climleltrp.c 
 |-  ( ph -> C e. RR )
8 climleltrp.l 
 |-  ( ph -> A <_ C )
9 climleltrp.x 
 |-  ( ph -> X e. RR+ )
10 4 3 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
11 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
12 10 11 syl 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
13 12 3 sseqtrrdi 
 |-  ( ph -> ( ZZ>= ` N ) C_ Z )
14 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
15 14 10 sseldi 
 |-  ( ph -> N e. ZZ )
16 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
17 eqidd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) = ( F ` k ) )
18 1 2 15 16 6 17 9 clim2d 
 |-  ( ph -> E. j e. ( ZZ>= ` N ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) )
19 nfv 
 |-  F/ k j e. ( ZZ>= ` N )
20 1 19 nfan 
 |-  F/ k ( ph /\ j e. ( ZZ>= ` N ) )
21 simplll 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ph )
22 uzss 
 |-  ( j e. ( ZZ>= ` N ) -> ( ZZ>= ` j ) C_ ( ZZ>= ` N ) )
23 22 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ZZ>= ` j ) C_ ( ZZ>= ` N ) )
24 simpr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` j ) )
25 23 24 sseldd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` N ) )
26 25 adantr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> k e. ( ZZ>= ` N ) )
27 simpr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( abs ` ( ( F ` k ) - A ) ) < X )
28 17 5 eqeltrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. RR )
29 28 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( F ` k ) e. RR )
30 climcl 
 |-  ( F ~~> A -> A e. CC )
31 6 30 syl 
 |-  ( ph -> A e. CC )
32 31 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> A e. CC )
33 28 recnd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. CC )
34 32 33 pncan3d 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( A + ( ( F ` k ) - A ) ) = ( F ` k ) )
35 34 eqcomd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) = ( A + ( ( F ` k ) - A ) ) )
36 35 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( F ` k ) = ( A + ( ( F ` k ) - A ) ) )
37 36 29 eqeltrrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( A + ( ( F ` k ) - A ) ) e. RR )
38 7 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> C e. RR )
39 1 2 16 15 6 5 climreclf 
 |-  ( ph -> A e. RR )
40 39 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> A e. RR )
41 29 40 resubcld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) - A ) e. RR )
42 38 41 readdcld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( C + ( ( F ` k ) - A ) ) e. RR )
43 9 rpred 
 |-  ( ph -> X e. RR )
44 43 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> X e. RR )
45 38 44 readdcld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( C + X ) e. RR )
46 8 ad2antrr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> A <_ C )
47 40 38 41 46 leadd1dd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( A + ( ( F ` k ) - A ) ) <_ ( C + ( ( F ` k ) - A ) ) )
48 33 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( F ` k ) e. CC )
49 32 adantr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> A e. CC )
50 48 49 subcld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) - A ) e. CC )
51 50 abscld 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( abs ` ( ( F ` k ) - A ) ) e. RR )
52 41 leabsd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) - A ) <_ ( abs ` ( ( F ` k ) - A ) ) )
53 simpr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( abs ` ( ( F ` k ) - A ) ) < X )
54 41 51 44 52 53 lelttrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) - A ) < X )
55 41 44 38 54 ltadd2dd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( C + ( ( F ` k ) - A ) ) < ( C + X ) )
56 37 42 45 47 55 lelttrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( A + ( ( F ` k ) - A ) ) < ( C + X ) )
57 36 56 eqbrtrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( F ` k ) < ( C + X ) )
58 29 57 jca 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )
59 21 26 27 58 syl21anc 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )
60 59 adantrl 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) -> ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )
61 60 ex 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) ) )
62 20 61 ralimdaa 
 |-  ( ( ph /\ j e. ( ZZ>= ` N ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) ) )
63 62 reximdva 
 |-  ( ph -> ( E. j e. ( ZZ>= ` N ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> E. j e. ( ZZ>= ` N ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) ) )
64 18 63 mpd 
 |-  ( ph -> E. j e. ( ZZ>= ` N ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )
65 ssrexv 
 |-  ( ( ZZ>= ` N ) C_ Z -> ( E. j e. ( ZZ>= ` N ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) ) )
66 13 64 65 sylc 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) )