Metamath Proof Explorer

Theorem climxlim2lem

Description: In this lemma for climxlim2 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climxlim2lem.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climxlim2lem.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climxlim2lem.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
climxlim2lem.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
climxlim2lem.5 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
Assertion climxlim2lem ( 𝜑 → 𝐹 ~~>* 𝐴 )

Proof

Step Hyp Ref Expression
1 climxlim2lem.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 climxlim2lem.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climxlim2lem.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 climxlim2lem.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
5 climxlim2lem.5 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ⇝ 𝐴 )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑀 ∈ ℤ )
8 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
9 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
10 7 2 8 9 xlimclim2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
11 6 10 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 ~~>* 𝐴 )
12 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
13 12 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) )
14 13 adantllr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) )
15 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
16 15 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
17 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) → ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
18 eleq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑦 ∈ ℂ ↔ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
19 neeq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑦 ≠ 𝐴 ↔ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) )
20 18 19 anbi12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) ) )
21 fvoveq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( abs ‘ ( 𝑦 − 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
22 21 breq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ↔ 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
23 20 22 imbi12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑘 ) → ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) )
24 23 rspcva ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
25 16 17 24 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
26 25 adantr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
27 14 26 mpd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
28 27 ex ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
29 28 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
30 29 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
31 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
32 5 31 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
33 32 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℂ )
34 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ¬ 𝐴 ∈ ℝ )
35 prfi ⊢ { +∞ , -∞ } ∈ Fin
36 35 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → { +∞ , -∞ } ∈ Fin )
37 df-xr ⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )
38 33 34 36 37 cnrefiisp ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℝ* ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 𝐴 ) → 𝑥 ≤ ( abs ‘ ( 𝑦 − 𝐴 ) ) ) )
39 30 38 reximddv3 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
40 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ ℝ+ )
41 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
42 40 41 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
43 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
44 42 43 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 )
45 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥
46 44 45 nfan ⊢ Ⅎ 𝑘 ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
47 simpll ⊢ ( ( ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
48 2 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
49 48 adantll ⊢ ( ( ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
50 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
51 47 49 50 syl2anc ⊢ ( ( ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
52 neqne ⊢ ( ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 → ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 )
53 51 52 impel ⊢ ( ( ( ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
54 53 ad5ant2345 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
55 54 adantllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
56 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
57 56 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
58 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : 𝑍 ⟶ ℂ )
59 48 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
60 58 59 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
61 60 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
62 32 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐴 ∈ ℂ )
63 61 62 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℂ )
64 63 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
65 64 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
67 66 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ+ )
68 67 rpred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
69 65 68 ltnled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ¬ 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) )
70 57 69 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ¬ 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
71 70 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ¬ 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
72 71 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ¬ 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
73 55 72 condan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
74 46 73 ralrimia ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
75 nfcv ⊢ Ⅎ 𝑘 𝐹
76 75 1 2 4 climuz ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
77 5 76 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
78 77 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
79 78 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
81 74 80 reximddv3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
82 81 adantllr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ≠ 𝐴 → 𝑥 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
83 39 82 rexlimddv2 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
84 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 )
85 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴
86 84 85 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
87 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝐹 : 𝑍 ⟶ ℝ* )
88 simplr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝑗 ∈ 𝑍 )
89 2 uzid3 ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
90 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
91 90 eqeq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) = 𝐴 ↔ ( 𝐹 ‘ 𝑗 ) = 𝐴 ) )
92 91 rspcva ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
93 89 92 sylan ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
94 93 3adant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
95 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
96 95 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
97 94 96 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝐴 ∈ ℝ* )
98 97 ad4ant134 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝐴 ∈ ℝ* )
99 rspa ⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
100 99 adantll ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
101 86 75 2 87 88 98 100 xlimconst2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 ) → 𝐹 ~~>* 𝐴 )
102 83 101 rexlimddv2 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ ) → 𝐹 ~~>* 𝐴 )
103 11 102 pm2.61dan ⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 )