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

Metamath Proof Explorer

Theorem climrlim2

Description: Produce a real limit from an integer limit, where the real function is only dependent on the integer part of x . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses climrlim2.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climrlim2.2 ⊢ ( 𝑛 = ( ⌊ ‘ 𝑥 ) → 𝐵 = 𝐶 )
climrlim2.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
climrlim2.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climrlim2.5 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 )
climrlim2.6 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
climrlim2.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ≤ 𝑥 )
Assertion climrlim2 ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )

Proof

Step Hyp Ref Expression
1 climrlim2.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climrlim2.2 ⊢ ( 𝑛 = ( ⌊ ‘ 𝑥 ) → 𝐵 = 𝐶 )
3 climrlim2.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 climrlim2.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 climrlim2.5 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 )
6 climrlim2.6 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
7 climrlim2.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ≤ 𝑥 )
8 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
9 8 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
10 9 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → 𝑗 ∈ ℤ )
11 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
12 11 flcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
13 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
14 13 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
15 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → 𝑗 ≤ 𝑥 )
16 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
17 16 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
18 flge ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ≤ 𝑥 ↔ 𝑗 ≤ ( ⌊ ‘ 𝑥 ) ) )
19 17 10 18 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( 𝑗 ≤ 𝑥 ↔ 𝑗 ≤ ( ⌊ ‘ 𝑥 ) ) )
20 15 19 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → 𝑗 ≤ ( ⌊ ‘ 𝑥 ) )
21 eluz2 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑗 ) ↔ ( 𝑗 ∈ ℤ ∧ ( ⌊ ‘ 𝑥 ) ∈ ℤ ∧ 𝑗 ≤ ( ⌊ ‘ 𝑥 ) ) )
22 10 14 20 21 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
23 simpr ⊢ ( ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 )
24 23 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 )
25 fveq2 ⊢ ( 𝑘 = ( ⌊ ‘ 𝑥 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
26 25 fvoveq1d ⊢ ( 𝑘 = ( ⌊ ‘ 𝑥 ) → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) = ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝐷 ) ) )
27 26 breq1d ⊢ ( 𝑘 = ( ⌊ ‘ 𝑥 ) → ( ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ↔ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝐷 ) ) < 𝑦 ) )
28 27 rspcv ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝐷 ) ) < 𝑦 ) )
29 22 24 28 syl2im ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝐷 ) ) < 𝑦 ) )
30 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑛 ∈ 𝑍 ↦ 𝐵 )
31 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
32 flge ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ≤ 𝑥 ↔ 𝑀 ≤ ( ⌊ ‘ 𝑥 ) ) )
33 11 31 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑀 ≤ 𝑥 ↔ 𝑀 ≤ ( ⌊ ‘ 𝑥 ) ) )
34 7 33 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ≤ ( ⌊ ‘ 𝑥 ) )
35 eluz2 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( ⌊ ‘ 𝑥 ) ∈ ℤ ∧ 𝑀 ≤ ( ⌊ ‘ 𝑥 ) ) )
36 31 12 34 35 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
37 36 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⌊ ‘ 𝑥 ) ∈ 𝑍 )
38 2 eleq1d ⊢ ( 𝑛 = ( ⌊ ‘ 𝑥 ) → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
39 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 𝐵 ∈ ℂ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝑍 𝐵 ∈ ℂ )
41 38 40 37 rspcdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
42 30 2 37 41 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) = 𝐶 )
43 42 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) = 𝐶 )
44 43 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) = 𝐶 )
45 44 fvoveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝐷 ) ) = ( abs ‘ ( 𝐶 − 𝐷 ) ) )
46 45 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝐷 ) ) < 𝑦 ↔ ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) )
47 29 46 sylibd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) )
48 47 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑗 ≤ 𝑥 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
49 48 com23 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
50 49 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
51 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℝ )
52 51 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ )
53 52 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ℝ )
54 50 53 jctild ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ( 𝑗 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) ) )
55 54 expimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) ) → ( 𝑗 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) ) )
56 55 reximdv2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
57 56 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
58 57 adantld ⊢ ( 𝜑 → ( ( 𝐷 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
59 climrel ⊢ Rel ⇝
60 59 brrelex1i ⊢ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ V )
61 5 60 syl ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ V )
62 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) )
63 1 4 61 62 clim2 ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 ↔ ( 𝐷 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) − 𝐷 ) ) < 𝑦 ) ) ) )
64 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ ℂ )
65 climcl ⊢ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 → 𝐷 ∈ ℂ )
66 5 65 syl ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
67 64 3 66 rlim2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐷 ) ) < 𝑦 ) ) )
68 58 63 67 3imtr4d ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐷 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 ) )
69 5 68 mpd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐷 )