Theorem rlimi

Description: Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		rlimi.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑉 )
2		rlimi.2	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
3		rlimi.3	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
4		breq2	⊢ ( 𝑥 = 𝑅 → ( ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) )
5	4	imbi2d	⊢ ( 𝑥 = 𝑅 → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) ) )
6	5	rexralbidv	⊢ ( 𝑥 = 𝑅 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) ) )
7		rlimf	⊢ ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ )
9		eqid	⊢ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑧 ∈ 𝐴 ↦ 𝐵 )
10	9	fmpt	⊢ ( ∀ 𝑧 ∈ 𝐴 𝐵 ∈ 𝑉 ↔ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑉 )
11	1 10	sylib	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑉 )
12	11	fdmd	⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
13	12	feq2d	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ ↔ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ) )
14	8 13	mpbid	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
15	9	fmpt	⊢ ( ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ ↔ ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
16	14 15	sylibr	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 𝐵 ∈ ℂ )
17		rlimss	⊢ ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
18	3 17	syl	⊢ ( 𝜑 → dom ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
19	12 18	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
20		rlimcl	⊢ ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ )
21	3 20	syl	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
22	16 19 21	rlim2	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
23	3 22	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) )
24	6 23 2	rspcdva	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑅 ) )