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 bilani 
 |-  ( ( ph /\ i e. Z ) -> i e. ( ZZ>= ` M ) )
59 uzss 
 |-  ( i e. ( ZZ>= ` M ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
60 58 59 syl 
 |-  ( ( ph /\ i e. Z ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
61 nfcv 
 |-  F/_ k ( i + 1 )
62 4 61 nffv 
 |-  F/_ k ( I ` ( i + 1 ) )
63 nfcv 
 |-  F/_ k ZZ>=
64 nfcv 
 |-  F/_ k +
65 nfcv 
 |-  F/_ k 1
66 46 64 65 nfov 
 |-  F/_ k ( ( I ` i ) + 1 )
67 63 66 nffv 
 |-  F/_ k ( ZZ>= ` ( ( I ` i ) + 1 ) )
68 62 67 nfel 
 |-  F/ k ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) )
69 43 68 nfim 
 |-  F/ k ( ( ph /\ i e. Z ) -> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) )
70 fvoveq1 
 |-  ( k = i -> ( I ` ( k + 1 ) ) = ( I ` ( i + 1 ) ) )
71 fveq2 
 |-  ( k = i -> ( I ` k ) = ( I ` i ) )
72 71 fvoveq1d 
 |-  ( k = i -> ( ZZ>= ` ( ( I ` k ) + 1 ) ) = ( ZZ>= ` ( ( I ` i ) + 1 ) ) )
73 70 72 eleq12d 
 |-  ( k = i -> ( ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) <-> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) ) )
74 51 73 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 ) ) ) ) )
75 69 74 11 chvarfv 
 |-  ( ( ph /\ i e. Z ) -> ( I ` ( i + 1 ) ) e. ( ZZ>= ` ( ( I ` i ) + 1 ) ) )
76 5 6 10 75 climsuselem1 
 |-  ( ( ph /\ i e. Z ) -> ( I ` i ) e. ( ZZ>= ` i ) )
77 60 76 sseldd 
 |-  ( ( ph /\ i e. Z ) -> ( I ` i ) e. ( ZZ>= ` M ) )
78 77 5 eleqtrrdi 
 |-  ( ( ph /\ i e. Z ) -> ( I ` i ) e. Z )
79 78 ex 
 |-  ( ph -> ( i e. Z -> ( I ` i ) e. Z ) )
80 79 imdistani 
 |-  ( ( ph /\ i e. Z ) -> ( ph /\ ( I ` i ) e. Z ) )
81 42 nfci 
 |-  F/_ k Z
82 46 81 nfel 
 |-  F/ k ( I ` i ) e. Z
83 1 82 nfan 
 |-  F/ k ( ph /\ ( I ` i ) e. Z )
84 47 nfel1 
 |-  F/ k ( F ` ( I ` i ) ) e. CC
85 83 84 nfim 
 |-  F/ k ( ( ph /\ ( I ` i ) e. Z ) -> ( F ` ( I ` i ) ) e. CC )
86 eleq1 
 |-  ( k = ( I ` i ) -> ( k e. Z <-> ( I ` i ) e. Z ) )
87 86 anbi2d 
 |-  ( k = ( I ` i ) -> ( ( ph /\ k e. Z ) <-> ( ph /\ ( I ` i ) e. Z ) ) )
88 fveq2 
 |-  ( k = ( I ` i ) -> ( F ` k ) = ( F ` ( I ` i ) ) )
89 88 eleq1d 
 |-  ( k = ( I ` i ) -> ( ( F ` k ) e. CC <-> ( F ` ( I ` i ) ) e. CC ) )
90 87 89 imbi12d 
 |-  ( k = ( I ` i ) -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) <-> ( ( ph /\ ( I ` i ) e. Z ) -> ( F ` ( I ` i ) ) e. CC ) ) )
91 46 85 90 8 vtoclgf 
 |-  ( ( I ` i ) e. Z -> ( ( ph /\ ( I ` i ) e. Z ) -> ( F ` ( I ` i ) ) e. CC ) )
92 78 80 91 sylc 
 |-  ( ( ph /\ i e. Z ) -> ( F ` ( I ` i ) ) e. CC )
93 56 92 eqeltrd 
 |-  ( ( ph /\ i e. Z ) -> ( G ` i ) e. CC )
94 23 41 93 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 )
95 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 ) ) )
96 95 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 ) ) )
97 fveq2 
 |-  ( i = h -> ( F ` i ) = ( F ` h ) )
98 97 eleq1d 
 |-  ( i = h -> ( ( F ` i ) e. CC <-> ( F ` h ) e. CC ) )
99 97 fvoveq1d 
 |-  ( i = h -> ( abs ` ( ( F ` i ) - A ) ) = ( abs ` ( ( F ` h ) - A ) ) )
100 99 breq1d 
 |-  ( i = h -> ( ( abs ` ( ( F ` i ) - A ) ) < x <-> ( abs ` ( ( F ` h ) - A ) ) < x ) )
101 98 100 anbi12d 
 |-  ( i = h -> ( ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) <-> ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) ) )
102 101 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 ) )
103 102 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 ) )
104 103 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 ) )
105 zre 
 |-  ( j e. ZZ -> j e. RR )
106 105 3ad2ant2 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j e. RR )
107 simp3 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ( ZZ>= ` if ( M <_ j , j , M ) ) )
108 eluzelz 
 |-  ( i e. ( ZZ>= ` if ( M <_ j , j , M ) ) -> i e. ZZ )
109 zre 
 |-  ( i e. ZZ -> i e. RR )
110 107 108 109 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. RR )
111 simp1 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ph )
112 6 zred 
 |-  ( ph -> M e. RR )
113 111 112 syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M e. RR )
114 simpl2 
 |-  ( ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) /\ M <_ j ) -> j e. ZZ )
115 114 zred 
 |-  ( ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) /\ M <_ j ) -> j e. RR )
116 113 adantr 
 |-  ( ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) /\ -. M <_ j ) -> M e. RR )
117 115 116 ifclda 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> if ( M <_ j , j , M ) e. RR )
118 max1 
 |-  ( ( M e. RR /\ j e. RR ) -> M <_ if ( M <_ j , j , M ) )
119 113 106 118 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M <_ if ( M <_ j , j , M ) )
120 eluzle 
 |-  ( i e. ( ZZ>= ` if ( M <_ j , j , M ) ) -> if ( M <_ j , j , M ) <_ i )
121 120 3ad2ant3 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> if ( M <_ j , j , M ) <_ i )
122 113 117 110 119 121 letrd 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M <_ i )
123 111 6 syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> M e. ZZ )
124 108 3ad2ant3 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ZZ )
125 eluz 
 |-  ( ( M e. ZZ /\ i e. ZZ ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
126 123 124 125 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( i e. ( ZZ>= ` M ) <-> M <_ i ) )
127 122 126 mpbird 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. ( ZZ>= ` M ) )
128 127 5 eleqtrrdi 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i e. Z )
129 111 128 jca 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( ph /\ i e. Z ) )
130 eluzelre 
 |-  ( ( I ` i ) e. ( ZZ>= ` M ) -> ( I ` i ) e. RR )
131 129 77 130 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. RR )
132 max2 
 |-  ( ( M e. RR /\ j e. RR ) -> j <_ if ( M <_ j , j , M ) )
133 113 106 132 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j <_ if ( M <_ j , j , M ) )
134 106 117 110 133 121 letrd 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j <_ i )
135 eluzle 
 |-  ( ( I ` i ) e. ( ZZ>= ` i ) -> i <_ ( I ` i ) )
136 129 76 135 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> i <_ ( I ` i ) )
137 106 110 131 134 136 letrd 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j <_ ( I ` i ) )
138 simp2 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> j e. ZZ )
139 eluzelz 
 |-  ( ( I ` i ) e. ( ZZ>= ` i ) -> ( I ` i ) e. ZZ )
140 129 76 139 3syl 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. ZZ )
141 eluz 
 |-  ( ( j e. ZZ /\ ( I ` i ) e. ZZ ) -> ( ( I ` i ) e. ( ZZ>= ` j ) <-> j <_ ( I ` i ) ) )
142 138 140 141 syl2anc 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( ( I ` i ) e. ( ZZ>= ` j ) <-> j <_ ( I ` i ) ) )
143 137 142 mpbird 
 |-  ( ( ph /\ j e. ZZ /\ i e. ( ZZ>= ` if ( M <_ j , j , M ) ) ) -> ( I ` i ) e. ( ZZ>= ` j ) )
144 23 24 26 143 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 ) )
145 fveq2 
 |-  ( h = ( I ` i ) -> ( F ` h ) = ( F ` ( I ` i ) ) )
146 145 eleq1d 
 |-  ( h = ( I ` i ) -> ( ( F ` h ) e. CC <-> ( F ` ( I ` i ) ) e. CC ) )
147 145 fvoveq1d 
 |-  ( h = ( I ` i ) -> ( abs ` ( ( F ` h ) - A ) ) = ( abs ` ( ( F ` ( I ` i ) ) - A ) ) )
148 147 breq1d 
 |-  ( h = ( I ` i ) -> ( ( abs ` ( ( F ` h ) - A ) ) < x <-> ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x ) )
149 146 148 anbi12d 
 |-  ( h = ( I ` i ) -> ( ( ( F ` h ) e. CC /\ ( abs ` ( ( F ` h ) - A ) ) < x ) <-> ( ( F ` ( I ` i ) ) e. CC /\ ( abs ` ( ( F ` ( I ` i ) ) - A ) ) < x ) ) )
150 149 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 ) )
151 150 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 )
152 104 144 151 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 )
153 96 152 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 )
154 94 153 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 ) )
155 154 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 ) ) )
156 22 155 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 ) )
157 fveq2 
 |-  ( l = if ( M <_ j , j , M ) -> ( ZZ>= ` l ) = ( ZZ>= ` if ( M <_ j , j , M ) ) )
158 157 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 ) ) )
159 158 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 ) )
160 19 156 159 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 ) )
161 eqidd 
 |-  ( ( ph /\ i e. ZZ ) -> ( F ` i ) = ( F ` i ) )
162 7 161 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 ) ) ) )
163 9 162 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 ) ) )
164 163 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. ZZ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) )
165 164 r19.21bi 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. ZZ A. i e. ( ZZ>= ` j ) ( ( F ` i ) e. CC /\ ( abs ` ( ( F ` i ) - A ) ) < x ) )
166 160 165 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
167 166 ex 
 |-  ( ph -> ( x e. RR+ -> E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) ) )
168 16 167 ralrimi 
 |-  ( ph -> A. x e. RR+ E. l e. ZZ A. i e. ( ZZ>= ` l ) ( ( G ` i ) e. CC /\ ( abs ` ( ( G ` i ) - A ) ) < x ) )
169 eqidd 
 |-  ( ( ph /\ i e. ZZ ) -> ( G ` i ) = ( G ` i ) )
170 12 169 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 ) ) ) )
171 15 168 170 mpbir2and 
 |-  ( ph -> G ~~> A )