Metamath Proof Explorer

Theorem fnlimabslt

Description: A sequence of function values, approximates the corresponding limit function value, all but finitely many times. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimabslt.p 
|- F/ m ph
fnlimabslt.f 
|- F/_ m F
fnlimabslt.n 
|- F/_ x F
fnlimabslt.m 
|- ( ph -> M e. ZZ )
fnlimabslt.z 
|- Z = ( ZZ>= ` M )
fnlimabslt.b 
|- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
fnlimabslt.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
fnlimabslt.g 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
fnlimabslt.x 
|- ( ph -> X e. D )
fnlimabslt.y 
|- ( ph -> Y e. RR+ )
Assertion fnlimabslt 
|- ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. RR /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )

Proof

Step Hyp Ref Expression
1 fnlimabslt.p 
 |-  F/ m ph
2 fnlimabslt.f 
 |-  F/_ m F
3 fnlimabslt.n 
 |-  F/_ x F
4 fnlimabslt.m 
 |-  ( ph -> M e. ZZ )
5 fnlimabslt.z 
 |-  Z = ( ZZ>= ` M )
6 fnlimabslt.b 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
7 fnlimabslt.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
8 fnlimabslt.g 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
9 fnlimabslt.x 
 |-  ( ph -> X e. D )
10 fnlimabslt.y 
 |-  ( ph -> Y e. RR+ )
11 eqid 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
12 nfcv 
 |-  F/_ x Z
13 nfcv 
 |-  F/_ x ( ZZ>= ` n )
14 nfcv 
 |-  F/_ x m
15 3 14 nffv 
 |-  F/_ x ( F ` m )
16 15 nfdm 
 |-  F/_ x dom ( F ` m )
17 13 16 nfiin 
 |-  F/_ x |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
18 12 17 nfiun 
 |-  F/_ x U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
19 nfcv 
 |-  F/_ y U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
20 nfv 
 |-  F/ y ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~>
21 nfcv 
 |-  F/_ x y
22 15 21 nffv 
 |-  F/_ x ( ( F ` m ) ` y )
23 12 22 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` y ) )
24 nfcv 
 |-  F/_ x dom ~~>
25 23 24 nfel 
 |-  F/ x ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~>
26 fveq2 
 |-  ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
27 26 mpteq2dv 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` y ) ) )
28 27 eleq1d 
 |-  ( x = y -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> ) )
29 18 19 20 25 28 cbvrabw 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> }
30 ssrab2 
 |-  { y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
31 29 30 eqsstri 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
32 7 31 eqsstri 
 |-  D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
33 32 9 sseldi 
 |-  ( ph -> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
34 1 5 6 11 33 allbutfifvre 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR )
35 nfv 
 |-  F/ j ph
36 nfcv 
 |-  F/_ j ( m e. Z |-> ( ( F ` m ) ` X ) )
37 3 7 8 9 fnlimcnv 
 |-  ( ph -> ( m e. Z |-> ( ( F ` m ) ` X ) ) ~~> ( G ` X ) )
38 nfcv 
 |-  F/_ l ( ( F ` m ) ` X )
39 nfcv 
 |-  F/_ m l
40 2 39 nffv 
 |-  F/_ m ( F ` l )
41 nfcv 
 |-  F/_ m X
42 40 41 nffv 
 |-  F/_ m ( ( F ` l ) ` X )
43 fveq2 
 |-  ( m = l -> ( F ` m ) = ( F ` l ) )
44 43 fveq1d 
 |-  ( m = l -> ( ( F ` m ) ` X ) = ( ( F ` l ) ` X ) )
45 38 42 44 cbvmpt 
 |-  ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( l e. Z |-> ( ( F ` l ) ` X ) )
46 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
47 46 fveq1d 
 |-  ( l = j -> ( ( F ` l ) ` X ) = ( ( F ` j ) ` X ) )
48 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
49 fvexd 
 |-  ( ( ph /\ j e. Z ) -> ( ( F ` j ) ` X ) e. _V )
50 45 47 48 49 fvmptd3 
 |-  ( ( ph /\ j e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) ` X ) ) ` j ) = ( ( F ` j ) ` X ) )
51 35 36 5 4 37 50 10 climd 
 |-  ( ph -> E. n e. Z A. j e. ( ZZ>= ` n ) ( ( ( F ` j ) ` X ) e. CC /\ ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y ) )
52 nfv 
 |-  F/ j ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y )
53 nfcv 
 |-  F/_ m j
54 2 53 nffv 
 |-  F/_ m ( F ` j )
55 54 41 nffv 
 |-  F/_ m ( ( F ` j ) ` X )
56 nfcv 
 |-  F/_ m CC
57 55 56 nfel 
 |-  F/ m ( ( F ` j ) ` X ) e. CC
58 nfcv 
 |-  F/_ m abs
59 nfcv 
 |-  F/_ m -
60 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( ( F ` m ) ` x ) )
61 nfcv 
 |-  F/_ m dom ~~>
62 60 61 nfel 
 |-  F/ m ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~>
63 nfcv 
 |-  F/_ m Z
64 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
65 63 64 nfiun 
 |-  F/_ m U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
66 62 65 nfrabw 
 |-  F/_ m { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
67 7 66 nfcxfr 
 |-  F/_ m D
68 nfcv 
 |-  F/_ m ~~>
69 68 60 nffv 
 |-  F/_ m ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) )
70 67 69 nfmpt 
 |-  F/_ m ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
71 8 70 nfcxfr 
 |-  F/_ m G
72 71 41 nffv 
 |-  F/_ m ( G ` X )
73 55 59 72 nfov 
 |-  F/_ m ( ( ( F ` j ) ` X ) - ( G ` X ) )
74 58 73 nffv 
 |-  F/_ m ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) )
75 nfcv 
 |-  F/_ m <
76 nfcv 
 |-  F/_ m Y
77 74 75 76 nfbr 
 |-  F/ m ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y
78 57 77 nfan 
 |-  F/ m ( ( ( F ` j ) ` X ) e. CC /\ ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y )
79 fveq2 
 |-  ( m = j -> ( F ` m ) = ( F ` j ) )
80 79 fveq1d 
 |-  ( m = j -> ( ( F ` m ) ` X ) = ( ( F ` j ) ` X ) )
81 80 eleq1d 
 |-  ( m = j -> ( ( ( F ` m ) ` X ) e. CC <-> ( ( F ` j ) ` X ) e. CC ) )
82 80 fvoveq1d 
 |-  ( m = j -> ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) = ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) )
83 82 breq1d 
 |-  ( m = j -> ( ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y <-> ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y ) )
84 81 83 anbi12d 
 |-  ( m = j -> ( ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) <-> ( ( ( F ` j ) ` X ) e. CC /\ ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y ) ) )
85 52 78 84 cbvralw 
 |-  ( A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) <-> A. j e. ( ZZ>= ` n ) ( ( ( F ` j ) ` X ) e. CC /\ ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y ) )
86 85 rexbii 
 |-  ( E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) <-> E. n e. Z A. j e. ( ZZ>= ` n ) ( ( ( F ` j ) ` X ) e. CC /\ ( abs ` ( ( ( F ` j ) ` X ) - ( G ` X ) ) ) < Y ) )
87 51 86 sylibr 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
88 nfv 
 |-  F/ m n e. Z
89 1 88 nfan 
 |-  F/ m ( ph /\ n e. Z )
90 simpr 
 |-  ( ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) -> ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y )
91 90 a1i 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) -> ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
92 89 91 ralimdaa 
 |-  ( ( ph /\ n e. Z ) -> ( A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) -> A. m e. ( ZZ>= ` n ) ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
93 92 reximdva 
 |-  ( ph -> ( E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. CC /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) -> E. n e. Z A. m e. ( ZZ>= ` n ) ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
94 87 93 mpd 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y )
95 34 94 jca 
 |-  ( ph -> ( E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR /\ E. n e. Z A. m e. ( ZZ>= ` n ) ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
96 5 rexanuz2 
 |-  ( E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. RR /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) <-> ( E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR /\ E. n e. Z A. m e. ( ZZ>= ` n ) ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )
97 95 96 sylibr 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( ( F ` m ) ` X ) e. RR /\ ( abs ` ( ( ( F ` m ) ` X ) - ( G ` X ) ) ) < Y ) )