Metamath Proof Explorer

Theorem climxlim2lem

Description: In this lemma for climxlim2 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climxlim2lem.1 
|- ( ph -> M e. ZZ )
climxlim2lem.2 
|- Z = ( ZZ>= ` M )
climxlim2lem.3 
|- ( ph -> F : Z --> RR* )
climxlim2lem.4 
|- ( ph -> F : Z --> CC )
climxlim2lem.5 
|- ( ph -> F ~~> A )
Assertion climxlim2lem 
|- ( ph -> F ~~>* A )

Proof

Step Hyp Ref Expression
1 climxlim2lem.1 
 |-  ( ph -> M e. ZZ )
2 climxlim2lem.2 
 |-  Z = ( ZZ>= ` M )
3 climxlim2lem.3 
 |-  ( ph -> F : Z --> RR* )
4 climxlim2lem.4 
 |-  ( ph -> F : Z --> CC )
5 climxlim2lem.5 
 |-  ( ph -> F ~~> A )
6 5 adantr 
 |-  ( ( ph /\ A e. RR ) -> F ~~> A )
7 1 adantr 
 |-  ( ( ph /\ A e. RR ) -> M e. ZZ )
8 3 adantr 
 |-  ( ( ph /\ A e. RR ) -> F : Z --> RR* )
9 simpr 
 |-  ( ( ph /\ A e. RR ) -> A e. RR )
10 7 2 8 9 xlimclim2 
 |-  ( ( ph /\ A e. RR ) -> ( F ~~>* A <-> F ~~> A ) )
11 6 10 mpbird 
 |-  ( ( ph /\ A e. RR ) -> F ~~>* A )
12 4 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
13 12 anim1i 
 |-  ( ( ( ph /\ k e. Z ) /\ ( F ` k ) =/= A ) -> ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) )
14 13 adantllr 
 |-  ( ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) /\ ( F ` k ) =/= A ) -> ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) )
15 3 adantr 
 |-  ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) -> F : Z --> RR* )
16 15 ffvelrnda 
 |-  ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) -> ( F ` k ) e. RR* )
17 simplr 
 |-  ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) -> A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )
18 eleq1 
 |-  ( y = ( F ` k ) -> ( y e. CC <-> ( F ` k ) e. CC ) )
19 neeq1 
 |-  ( y = ( F ` k ) -> ( y =/= A <-> ( F ` k ) =/= A ) )
20 18 19 anbi12d 
 |-  ( y = ( F ` k ) -> ( ( y e. CC /\ y =/= A ) <-> ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) ) )
21 fvoveq1 
 |-  ( y = ( F ` k ) -> ( abs ` ( y - A ) ) = ( abs ` ( ( F ` k ) - A ) ) )
22 21 breq2d 
 |-  ( y = ( F ` k ) -> ( x <_ ( abs ` ( y - A ) ) <-> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
23 20 22 imbi12d 
 |-  ( y = ( F ` k ) -> ( ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) <-> ( ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) )
24 23 rspcva 
 |-  ( ( ( F ` k ) e. RR* /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) -> ( ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
25 16 17 24 syl2anc 
 |-  ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
26 25 adantr 
 |-  ( ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) /\ ( F ` k ) =/= A ) -> ( ( ( F ` k ) e. CC /\ ( F ` k ) =/= A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
27 14 26 mpd 
 |-  ( ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) /\ ( F ` k ) =/= A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) )
28 27 ex 
 |-  ( ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) /\ k e. Z ) -> ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
29 28 ralrimiva 
 |-  ( ( ph /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) -> A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
30 29 ad4ant14 
 |-  ( ( ( ( ph /\ -. A e. RR ) /\ x e. RR+ ) /\ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) ) -> A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
31 climcl 
 |-  ( F ~~> A -> A e. CC )
32 5 31 syl 
 |-  ( ph -> A e. CC )
33 32 adantr 
 |-  ( ( ph /\ -. A e. RR ) -> A e. CC )
34 simpr 
 |-  ( ( ph /\ -. A e. RR ) -> -. A e. RR )
35 prfi 
 |-  { +oo , -oo } e. Fin
36 35 a1i 
 |-  ( ( ph /\ -. A e. RR ) -> { +oo , -oo } e. Fin )
37 df-xr 
 |-  RR* = ( RR u. { +oo , -oo } )
38 33 34 36 37 cnrefiisp 
 |-  ( ( ph /\ -. A e. RR ) -> E. x e. RR+ A. y e. RR* ( ( y e. CC /\ y =/= A ) -> x <_ ( abs ` ( y - A ) ) ) )
39 30 38 reximddv3 
 |-  ( ( ph /\ -. A e. RR ) -> E. x e. RR+ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
40 nfv 
 |-  F/ k ( ph /\ x e. RR+ )
41 nfra1 
 |-  F/ k A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) )
42 40 41 nfan 
 |-  F/ k ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
43 nfv 
 |-  F/ k j e. Z
44 42 43 nfan 
 |-  F/ k ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z )
45 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x
46 44 45 nfan 
 |-  F/ k ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
47 simpll 
 |-  ( ( ( A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
48 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
49 48 adantll 
 |-  ( ( ( A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
50 rspa 
 |-  ( ( A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) /\ k e. Z ) -> ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
51 47 49 50 syl2anc 
 |-  ( ( ( A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
52 neqne 
 |-  ( -. ( F ` k ) = A -> ( F ` k ) =/= A )
53 51 52 impel 
 |-  ( ( ( ( A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ -. ( F ` k ) = A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) )
54 53 ad5ant2345 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ -. ( F ` k ) = A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) )
55 54 adantllr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) /\ -. ( F ` k ) = A ) -> x <_ ( abs ` ( ( F ` k ) - A ) ) )
56 rspa 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - A ) ) < x )
57 56 adantll 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - A ) ) < x )
58 4 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> F : Z --> CC )
59 48 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
60 58 59 ffvelrnd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
61 60 adantlr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
62 32 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> A e. CC )
63 61 62 subcld 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) - A ) e. CC )
64 63 abscld 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - A ) ) e. RR )
65 64 adantl3r 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - A ) ) e. RR )
66 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
67 66 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR+ )
68 67 rpred 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR )
69 65 68 ltnled 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> -. x <_ ( abs ` ( ( F ` k ) - A ) ) ) )
70 57 69 mpbid 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> -. x <_ ( abs ` ( ( F ` k ) - A ) ) )
71 70 adantl3r 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> -. x <_ ( abs ` ( ( F ` k ) - A ) ) )
72 71 adantr 
 |-  ( ( ( ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) /\ -. ( F ` k ) = A ) -> -. x <_ ( abs ` ( ( F ` k ) - A ) ) )
73 55 72 condan 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) = A )
74 46 73 ralrimia 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
75 nfcv 
 |-  F/_ k F
76 75 1 2 4 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 ) ) )
77 5 76 mpbid 
 |-  ( ph -> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x ) )
78 77 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
79 78 r19.21bi 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
80 79 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < x )
81 74 80 reximddv3 
 |-  ( ( ( ph /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
82 81 adantllr 
 |-  ( ( ( ( ph /\ -. A e. RR ) /\ x e. RR+ ) /\ A. k e. Z ( ( F ` k ) =/= A -> x <_ ( abs ` ( ( F ` k ) - A ) ) ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
83 39 82 rexlimddv2 
 |-  ( ( ph /\ -. A e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
84 nfv 
 |-  F/ k ( ( ph /\ -. A e. RR ) /\ j e. Z )
85 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) ( F ` k ) = A
86 84 85 nfan 
 |-  F/ k ( ( ( ph /\ -. A e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
87 3 ad3antrrr 
 |-  ( ( ( ( ph /\ -. A e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> F : Z --> RR* )
88 simplr 
 |-  ( ( ( ( ph /\ -. A e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> j e. Z )
89 2 uzid3 
 |-  ( j e. Z -> j e. ( ZZ>= ` j ) )
90 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
91 90 eqeq1d 
 |-  ( k = j -> ( ( F ` k ) = A <-> ( F ` j ) = A ) )
92 91 rspcva 
 |-  ( ( j e. ( ZZ>= ` j ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> ( F ` j ) = A )
93 89 92 sylan 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> ( F ` j ) = A )
94 93 3adant1 
 |-  ( ( ph /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> ( F ` j ) = A )
95 3 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR* )
96 95 3adant3 
 |-  ( ( ph /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> ( F ` j ) e. RR* )
97 94 96 eqeltrrd 
 |-  ( ( ph /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> A e. RR* )
98 97 ad4ant134 
 |-  ( ( ( ( ph /\ -. A e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> A e. RR* )
99 rspa 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( F ` k ) = A /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) = A )
100 99 adantll 
 |-  ( ( ( ( ( ph /\ -. A e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) = A )
101 86 75 2 87 88 98 100 xlimconst2 
 |-  ( ( ( ( ph /\ -. A e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( F ` k ) = A ) -> F ~~>* A )
102 83 101 rexlimddv2 
 |-  ( ( ph /\ -. A e. RR ) -> F ~~>* A )
103 11 102 pm2.61dan 
 |-  ( ph -> F ~~>* A )