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