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

Metamath Proof Explorer

Theorem rlimclim1

Description: Forward direction of rlimclim . (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimclim1.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
rlimclim1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
rlimclim1.3 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐴 )
rlimclim1.4 ⊢ ( 𝜑 → 𝑍 ⊆ dom 𝐹 )
Assertion rlimclim1 ( 𝜑 → 𝐹 ⇝ 𝐴 )

Proof

Step Hyp Ref Expression
1 rlimclim1.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 rlimclim1.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 rlimclim1.3 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐴 )
4 rlimclim1.4 ⊢ ( 𝜑 → 𝑍 ⊆ dom 𝐹 )
5 fvex ⊢ ( 𝐹 ‘ 𝑤 ) ∈ V
6 5 rgenw ⊢ ∀ 𝑤 ∈ dom 𝐹 ( 𝐹 ‘ 𝑤 ) ∈ V
7 6 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑤 ∈ dom 𝐹 ( 𝐹 ‘ 𝑤 ) ∈ V )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
9 rlimf ⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ )
10 3 9 syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : dom 𝐹 ⟶ ℂ )
12 11 feqmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 = ( 𝑤 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑤 ) ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐹 ⇝𝑟 𝐴 )
14 12 13 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑤 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑤 ) ) ⇝𝑟 𝐴 )
15 7 8 14 rlimi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
16 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → 𝑀 ∈ ℤ )
17 flcl ⊢ ( 𝑧 ∈ ℝ → ( ⌊ ‘ 𝑧 ) ∈ ℤ )
18 17 peano2zd ⊢ ( 𝑧 ∈ ℝ → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℤ )
19 18 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℤ )
20 19 16 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ℤ )
21 16 zred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → 𝑀 ∈ ℝ )
22 19 zred ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ )
23 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) )
24 21 22 23 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) )
25 eluz2 ⊢ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) )
26 16 20 24 25 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
27 26 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ 𝑍 )
28 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ∈ ℝ )
29 18 zred ⊢ ( 𝑧 ∈ ℝ → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ )
30 28 29 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ )
31 21 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑀 ∈ ℝ )
32 30 31 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ ℝ )
33 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) → 𝑘 ∈ ℝ )
34 33 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ ℝ )
35 fllep1 ⊢ ( 𝑧 ∈ ℝ → 𝑧 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) )
36 28 35 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) )
37 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑧 ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) )
38 31 30 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( ( ⌊ ‘ 𝑧 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) )
39 28 30 32 36 38 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) )
40 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ≤ 𝑘 )
41 40 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ≤ 𝑘 )
42 28 32 34 39 41 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑧 ≤ 𝑘 )
43 breq2 ⊢ ( 𝑤 = 𝑘 → ( 𝑧 ≤ 𝑤 ↔ 𝑧 ≤ 𝑘 ) )
44 43 imbrov2fvoveq ⊢ ( 𝑤 = 𝑘 → ( ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ↔ ( 𝑧 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) ) )
45 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) )
46 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑍 ⊆ dom 𝐹 )
47 1 uztrn2 ⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ 𝑍 )
48 27 47 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ 𝑍 )
49 46 48 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ dom 𝐹 )
50 44 45 49 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( 𝑧 ≤ 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
51 42 50 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
52 51 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
53 fveq2 ⊢ ( 𝑗 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) )
54 53 raleqdv ⊢ ( 𝑗 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
55 54 rspcev ⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑧 ) + 1 ) , ( ( ⌊ ‘ 𝑧 ) + 1 ) , 𝑀 ) ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
56 27 52 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℝ ∧ ∀ 𝑤 ∈ dom 𝐹 ( 𝑧 ≤ 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − 𝐴 ) ) < 𝑦 ) ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
57 15 56 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
58 57 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
59 rlimpm ⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
60 3 59 syl ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
61 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
62 rlimcl ⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐴 ∈ ℂ )
63 3 62 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
64 4 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 )
65 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
66 64 65 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
67 1 2 60 61 63 66 clim2c ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
68 58 67 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )