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

Metamath Proof Explorer

Theorem rlimi2

Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rlimi.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑉 )
rlimi.2 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
rlimi.3 ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
rlimi.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
Assertion rlimi2 ( 𝜑 → ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rlimi.1 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑉 )
2 rlimi.2 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
3 rlimi.3 ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
4 rlimi.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 1 2 3 rlimi ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) )
6 eqid ⊢ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑧 ∈ 𝐴 ↦ 𝐵 )
7 6 fnmpt ⊢ ( ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
8 fndm ⊢ ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
9 1 7 8 3syl ⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
10 rlimss ⊢ ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
11 3 10 syl ⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
12 9 11 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
13 rexico ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ ) → ( ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) ) )
14 12 4 13 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) ) )
15 5 14 mpbird ⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝐷 [,) +∞ ) ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) )