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

Metamath Proof Explorer

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