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 ⊢ Ⅎ 𝑘 𝜑
climsuse.3 ⊢ Ⅎ 𝑘 𝐹
climsuse.2 ⊢ Ⅎ 𝑘 𝐺
climsuse.4 ⊢ Ⅎ 𝑘 𝐼
climsuse.5 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climsuse.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climsuse.7 ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
climsuse.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
climsuse.9 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climsuse.10 ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑀 ) ∈ 𝑍 )
climsuse.11 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐼 ‘ ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝑘 ) + 1 ) ) )
climsuse.12 ⊢ ( 𝜑 → 𝐺 ∈ 𝑌 )
climsuse.13 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐼 ‘ 𝑘 ) ) )
Assertion climsuse ( 𝜑 → 𝐺 ⇝ 𝐴 )

Proof

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