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 ffvelrnda ( ( 𝜑𝑘 ∈ dom 𝐹 ) → ( 𝐹𝑘 ) ∈ ℂ )
66 64 65 syldan ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
67 1 2 60 61 63 66 clim2c ( 𝜑 → ( 𝐹𝐴 ↔ ∀ 𝑦 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑦 ) )
68 58 67 mpbird ( 𝜑𝐹𝐴 )