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 ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) )