This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climsuse

Description: A subsequence G of a converging sequence F , converges to the same limit. I is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climsuse.1 
|- F/ k ph
climsuse.3 
|- F/_ k F
climsuse.2 
|- F/_ k G
climsuse.4 
|- F/_ k I
climsuse.5 
|- Z = ( ZZ>= ` M )
climsuse.6 
|- ( ph -> M e. ZZ )
climsuse.7 
|- ( ph -> F e. X )
climsuse.8 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climsuse.9 
|- ( ph -> F ~~> A )
climsuse.10 
|- ( ph -> ( I ` M ) e. Z )
climsuse.11 
|- ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )
climsuse.12 
|- ( ph -> G e. Y )
climsuse.13 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( F ` ( I ` k ) ) )
Assertion climsuse 
|- ( ph -> G ~~> A )

Proof

Step Hyp Ref Expression
1 climsuse.1 
 |-  F/ k ph
2 climsuse.3 
 |-  F/_ k F
3 climsuse.2 
 |-  F/_ k G
4 climsuse.4 
 |-  F/_ k I
5 climsuse.5 
 |-  Z = ( ZZ>= ` M )
6 climsuse.6 
 |-  ( ph -> M e. ZZ )
7 climsuse.7 
 |-  ( ph -> F e. X )
8 climsuse.8 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
9 climsuse.9 
 |-  ( ph -> F ~~> A )
10 climsuse.10 
 |-  ( ph -> ( I ` M ) e. Z )
11 climsuse.11 
 |-  ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )
12 climsuse.12 
 |-  ( ph -> G e. Y )
13 climsuse.13 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( F ` ( I ` k ) ) )
14 climcl 
 |-  ( F ~~> A -> A e. CC )
15 9 14 syl 
 |-  ( ph -> A e. CC )
16 nfv 
 |-  F/ x ph
17 simpllr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ M <_ j ) -> j e. ZZ )
18 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ -. M <_ j ) -> M e. ZZ )
19 17 18 ifclda 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) -> if ( M <_ j , j , M ) e. ZZ )
20 nfv 
 |-  F/ i ( ( ph /\ x e. RR+ ) /\ j e. ZZ )
21 nfra1 
 |-  F/ i A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x )
22 20 21 nfan 
 |-  F/ i ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) )
23 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ph )
24 simpllr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j e. ZZ )
25 23 24 jca 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( ph /\ j e. ZZ ) )
26 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ( ZZ>= ` if ( M <_ j , j , M ) ) )
27 simpr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ M <_ j ) -> M <_ j )
28 6 anim1i 
 |-  ( ( ph /\ j e. ZZ ) -> ( M e. ZZ /\ j e. ZZ ) )
29 28 adantr 
 |-  ( ( ( ph /\ j e. ZZ ) /\ M <_ j ) -> ( M e. ZZ /\ j e. ZZ ) )
30 eluz 
 |-  ( ( M e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` M ) <-> M <_ j ) )
31 29 30 syl 
 |-  ( ( ( ph /\ j e. ZZ ) /\ M <_ j ) -> ( j e. ( ZZ>= ` M ) <-> M <_ j ) )
32 27 31 mpbird 
 |-  ( ( ( ph /\ j e. ZZ ) /\ M <_ j ) -> j e. ( ZZ>= ` M ) )
33 simpll 
 |-  ( ( ( ph /\ j e. ZZ ) /\ -. M <_ j ) -> ph )
34 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
35 33 6 34 3syl 
 |-  ( ( ( ph /\ j e. ZZ ) /\ -. M <_ j ) -> M e. ( ZZ>= ` M ) )
36 32 35 ifclda 
 |-  ( ( ph /\ j e. ZZ ) -> if ( M <_ j , j , M ) e. ( ZZ>= ` M ) )
37 uzss 
 |-  ( if ( M <_ j , j , M ) e. ( ZZ>= ` M ) -> ( ZZ>= ` if ( M <_ j , j , M ) ) C_ ( ZZ>= ` M ) )
38 36 37 syl 
 |-  ( ( ph /\ j e. ZZ ) -> ( ZZ>= ` if ( M <_ j , j , M ) ) C_ ( ZZ>= ` M ) )
39 38 5 sseqtrrdi 
 |-  ( ( ph /\ j e. ZZ ) -> ( ZZ>= ` if ( M <_ j , j , M ) ) C_ Z )
40 39 sseld 
 |-  ( ( ph /\ j e. ZZ ) -> ( i e. ( ZZ>= ` if ( M <_ j , j , M ) ) -> i e. Z ) )
41 25 26 40 sylc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. Z )
42 nfv 
 |-  F/ k i e. Z
43 1 42 nfan 
 |-  F/ k ( ph /\ i e. Z )
44 nfcv 
 |-  F/_ k i
45 3 44 nffv 
 |-  F/_ k ( G ` i )
46 4 44 nffv 
 |-  F/_ k ( I ` i )
47 2 46 nffv 
 |-  F/_ k ( F ` ( I ` i ) )
48 45 47 nfeq 
 |-  F/ k ( G ` i ) = ( F ` ( I ` i ) )
49 43 48 nfim 
 |-  F/ k ( ( ph /\ i e. Z ) -> ( G ` i ) = ( F ` ( I ` i ) ) )
50 eleq1 
 |-  ( k = i -> ( k e. Z <-> i e. Z ) )
51 50 anbi2d 
 |-  ( k = i -> ( ( ph /\ k e. Z ) <-> ( ph /\ i e. Z ) ) )
52 fveq2 
 |-  ( k = i -> ( G ` k ) = ( G ` i ) )
53 2fveq3 
 |-  ( k = i -> ( F ` ( I ` k ) ) = ( F ` ( I ` i ) ) )
54 52 53 eqeq12d 
 |-  ( k = i -> ( ( G ` k ) = ( F ` ( I ` k ) ) <-> ( G ` i ) = ( F ` ( I ` i ) ) ) )
55 51 54 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. Z ) -> ( G ` k ) = ( F ` ( I ` k ) ) ) <-> ( ( ph /\ i e. Z ) -> ( G ` i ) = ( F ` ( I ` i ) ) ) ) )
56 49 55 13 chvarfv 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) = ( F ` ( I ` i ) ) )
57 5 eleq2i 
 |-  ( i e. Z <-> i e. ( ZZ>= ` M ) )
58 57 biimpi 
 |-  ( i e. Z -> i e. ( ZZ>= ` M ) )
59 58 adantl 
 |-  ( ( ph /\ i e. Z ) -> i e. ( ZZ>= ` M ) )
60 uzss 
 |-  ( i e. ( ZZ>= ` M ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
61 59 60 syl 
 |-  ( ( ph /\ i e. Z ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
62 nfcv 
 |-  F/_ k ( i + 1 )
63 4 62 nffv 
 |-  F/_ k ( I ` ( i + 1 ) )
64 nfcv 
 |-  F/_ k ZZ>=
65 nfcv 
 |-  F/_ k +
66 nfcv 
 |-  F/_ k 1
67 46 65 66 nfov 
 |-  F/_ k ( ( I ` i ) + 1 )
68 64 67 nffv 
 |-  F/_ k ( ZZ>= ` ( ( I ` i ) + 1 ) )
69 63 68 nfel 
 |-  F/ k ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) )
70 43 69 nfim 
 |-  F/ k ( ( ph /\ i e. Z ) -> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) )
71 fvoveq1 
 |-  ( k = i -> ( I ` ( k + 1 ) ) = ( I ` ( i + 1 ) ) )
72 fveq2 
 |-  ( k = i -> ( I ` k ) = ( I ` i ) )
73 72 fvoveq1d 
 |-  ( k = i -> ( ZZ>= ` ( ( I ` k ) + 1 ) ) = ( ZZ>= ` ( ( I ` i ) + 1 ) ) )
74 71 73 eleq12d 
 |-  ( k = i -> ( ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) <-> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) ) )
75 51 74 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) ) <-> ( ( ph /\ i e. Z ) -> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) ) ) )
76 70 75 11 chvarfv 
 |-  ( ( ph /\ i e. Z ) -> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) )
77 5 6 10 76 climsuselem1 
 |-  ( ( ph /\ i e. Z ) -> ( I ` i ) e. ( ZZ>= ` i ) )
78 61 77 sseldd 
 |-  ( ( ph /\ i e. Z ) -> ( I ` i ) e. ( ZZ>= ` M ) )
79 78 5 eleqtrrdi 
 |-  ( ( ph /\ i e. Z ) -> ( I ` i ) e. Z )
80 79 ex 
 |-  ( ph -> ( i e. Z -> ( I ` i ) e. Z ) )
81 80 imdistani 
 |-  ( ( ph /\ i e. Z ) -> ( ph /\ ( I ` i ) e. Z ) )
82 42 nfci 
 |-  F/_ k Z
83 46 82 nfel 
 |-  F/ k ( I ` i ) e. Z
84 1 83 nfan 
 |-  F/ k ( ph /\ ( I ` i ) e. Z )
85 47 nfel1 
 |-  F/ k ( F ` ( I ` i ) ) e. CC
86 84 85 nfim 
 |-  F/ k ( ( ph /\ ( I ` i ) e. Z ) -> ( F ` ( I ` i ) ) e. CC )
87 eleq1 
 |-  ( k = ( I ` i ) -> ( k e. Z <-> ( I ` i ) e. Z ) )
88 87 anbi2d 
 |-  ( k = ( I ` i ) -> ( ( ph /\ k e. Z ) <-> ( ph /\ ( I ` i ) e. Z ) ) )
89 fveq2 
 |-  ( k = ( I ` i ) -> ( F ` k ) = ( F ` ( I ` i ) ) )
90 89 eleq1d 
 |-  ( k = ( I ` i ) -> ( ( F ` k ) e. CC <-> ( F ` ( I ` i ) ) e. CC ) )
91 88 90 imbi12d 
 |-  ( k = ( I ` i ) -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) <-> ( ( ph /\ ( I ` i ) e. Z ) -> ( F ` ( I ` i ) ) e. CC ) ) )
92 46 86 91 8 vtoclgf 
 |-  ( ( I ` i ) e. Z -> ( ( ph /\ ( I ` i ) e. Z ) -> ( F ` ( I ` i ) ) e. CC ) )
93 79 81 92 sylc 
 |-  ( ( ph /\ i e. Z ) -> ( F ` ( I ` i ) ) e. CC )
94 56 93 eqeltrd 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) e. CC )
95 23 41 94 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( G ` i ) e. CC )
96 23 41 56 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( G ` i ) = ( F ` ( I ` i ) ) )
97 96 fvoveq1d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( abs ` ( ( G ` i ) - A ) ) = ( abs ` ( ( F ` ( I ` i ) ) - A ) ) )
98 fveq2 
 |-  ( i = h -> ( F ` i ) = ( F ` h ) )
99 98 eleq1d 
 |-  ( i = h -> ( ( F ` i ) e. CC <-> ( F ` h ) e. CC ) )
100 98 fvoveq1d 
 |-  ( i = h -> ( abs ` ( ( F ` i ) - A ) ) = ( abs ` ( ( F ` h ) - A ) ) )
101 100 breq1d 
 |-  ( i = h -> ( ( abs ` ( ( F ` i ) - A ) ) < x <-> ( abs ` ( ( F ` h ) - A ) ) < x ) )
102 99 101 anbi12d 
 |-  ( i = h -> ( ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) <-> ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) ) )
103 102 cbvralvw 
 |-  ( A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) <-> A. h e. ( ZZ>= ` j ) ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) )
104 103 biimpi 
 |-  ( A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) -> A. h e. ( ZZ>= ` j ) ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) )
105 104 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> A. h e. ( ZZ>= ` j ) ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) )
106 zre 
 |-  ( j e. ZZ -> j e. RR )
107 106 3ad2ant2 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j e. RR )
108 simp3 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ( ZZ>= ` if ( M <_ j , j , M ) ) )
109 eluzelz 
 |-  ( i e. ( ZZ>= ` if ( M <_ j , j , M ) ) -> i e. ZZ )
110 zre 
 |-  ( i e. ZZ -> i e. RR )
111 108 109 110 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. RR )
112 simp1 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ph )
113 6 zred 
 |-  ( ph -> M e. RR )
114 112 113 syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M e. RR )
115 simpl2 
 |-  ( ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) /\ M <_ j ) -> j e. ZZ )
116 115 zred 
 |-  ( ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) /\ M <_ j ) -> j e. RR )
117 114 adantr 
 |-  ( ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) /\ -. M <_ j ) -> M e. RR )
118 116 117 ifclda 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> if ( M <_ j , j , M ) e. RR )
119 max1 
 |-  ( ( M e. RR /\ j e. RR ) -> M <_ if ( M <_ j , j , M ) )
120 114 107 119 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M <_ if ( M <_ j , j , M ) )
121 eluzle 
 |-  ( i e. ( ZZ>= ` if ( M <_ j , j , M ) ) -> if ( M <_ j , j , M ) <_ i )
122 121 3ad2ant3 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> if ( M <_ j , j , M ) <_ i )
123 114 118 111 120 122 letrd 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M <_ i )
124 112 6 syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M e. ZZ )
125 109 3ad2ant3 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ZZ )
126 eluz 
 |-  ( ( M e. ZZ /\ i e. ZZ ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
127 124 125 126 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
128 123 127 mpbird 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ( ZZ>= ` M ) )
129 128 5 eleqtrrdi 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. Z )
130 112 129 jca 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( ph /\ i e. Z ) )
131 eluzelre 
 |-  ( ( I ` i ) e. ( ZZ>= ` M ) -> ( I ` i ) e. RR )
132 130 78 131 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. RR )
133 max2 
 |-  ( ( M e. RR /\ j e. RR ) -> j <_ if ( M <_ j , j , M ) )
134 114 107 133 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j <_ if ( M <_ j , j , M ) )
135 107 118 111 134 122 letrd 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j <_ i )
136 eluzle 
 |-  ( ( I ` i ) e. ( ZZ>= ` i ) -> i <_ ( I ` i ) )
137 130 77 136 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i <_ ( I ` i ) )
138 107 111 132 135 137 letrd 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j <_ ( I ` i ) )
139 simp2 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j e. ZZ )
140 eluzelz 
 |-  ( ( I ` i ) e. ( ZZ>= ` i ) -> ( I ` i ) e. ZZ )
141 130 77 140 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. ZZ )
142 eluz 
 |-  ( ( j e. ZZ /\ ( I ` i ) e. ZZ ) -> ( ( I ` i ) e. ( ZZ>= ` j ) <-> j <_ ( I ` i ) ) )
143 139 141 142 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( ( I ` i ) e. ( ZZ>= ` j ) <-> j <_ ( I ` i ) ) )
144 138 143 mpbird 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. ( ZZ>= ` j ) )
145 23 24 26 144 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. ( ZZ>= ` j ) )
146 fveq2 
 |-  ( h = ( I ` i ) -> ( F ` h ) = ( F ` ( I ` i ) ) )
147 146 eleq1d 
 |-  ( h = ( I ` i ) -> ( ( F ` h ) e. CC <-> ( F ` ( I ` i ) ) e. CC ) )
148 146 fvoveq1d 
 |-  ( h = ( I ` i ) -> ( abs ` ( ( F ` h ) - A ) ) = ( abs ` ( ( F ` ( I ` i ) ) - A ) ) )
149 148 breq1d 
 |-  ( h = ( I ` i ) -> ( ( abs ` ( ( F ` h ) - A ) ) < x <-> ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x ) )
150 147 149 anbi12d 
 |-  ( h = ( I ` i ) -> ( ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) <-> ( ( F ` ( I ` i ) ) e. CC /\ ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x ) ) )
151 150 rspccva 
 |-  ( ( A. h e. ( ZZ>= ` j ) ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) /\ ( I ` i ) e. ( ZZ>= ` j ) ) -> ( ( F ` ( I ` i ) ) e. CC /\ ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x ) )
152 151 simprd 
 |-  ( ( A. h e. ( ZZ>= ` j ) ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) /\ ( I ` i ) e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x )
153 105 145 152 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x )
154 97 153 eqbrtrd 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( abs ` ( ( G ` i ) - A ) ) < x )
155 95 154 jca 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
156 155 ex 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) -> ( i e. ( ZZ>= ` if ( M <_ j , j , M ) ) -> ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) ) )
157 22 156 ralrimi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) -> A. i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
158 fveq2 
 |-  ( l = if ( M <_ j , j , M ) -> ( ZZ>= ` l ) = ( ZZ>= ` if ( M <_ j , j , M ) ) )
159 158 raleqdv 
 |-  ( l = if ( M <_ j , j , M ) -> ( A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) <-> A. i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) ) )
160 159 rspcev 
 |-  ( ( if ( M <_ j , j , M ) e. ZZ /\ A. i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) ) -> E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
161 19 157 160 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ZZ ) /\ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) -> E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
162 eqidd 
 |-  ( ( ph /\ i e. ZZ ) -> ( F ` i ) = ( F ` i ) )
163 7 162 clim 
 |-  ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) ) )
164 9 163 mpbid 
 |-  ( ph -> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) ) )
165 164 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. ZZ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) )
166 165 r19.21bi 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. ZZ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) )
167 161 166 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
168 167 ex 
 |-  ( ph -> ( x e. RR+ -> E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) ) )
169 16 168 ralrimi 
 |-  ( ph -> A. x e. RR+ E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
170 eqidd 
 |-  ( ( ph /\ i e. ZZ ) -> ( G ` i ) = ( G ` i ) )
171 12 170 clim 
 |-  ( ph -> ( G ~~> A <-> ( A e. CC /\ A. x e. RR+ E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) ) ) )
172 15 169 171 mpbir2and 
 |-  ( ph -> G ~~> A )