Metamath Proof Explorer

Theorem rlim0lt

Description: Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

Ref Expression
Hypotheses rlim0.1 ⊢ φ → ∀ z ∈ A B ∈ ℂ
rlim0.2 ⊢ φ → A ⊆ ℝ
Assertion rlim0lt ⊢ φ → z ∈ A ⟼ B ⇝ℝ 0 ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B < x

Proof

Step Hyp Ref Expression
1 rlim0.1 ⊢ φ → ∀ z ∈ A B ∈ ℂ
2 rlim0.2 ⊢ φ → A ⊆ ℝ
3 0cnd ⊢ φ → 0 ∈ ℂ
4 1 2 3 rlim2lt ⊢ φ → z ∈ A ⟼ B ⇝ℝ 0 ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − 0 < x
5 subid1 ⊢ B ∈ ℂ → B − 0 = B
6 5 fveq2d ⊢ B ∈ ℂ → B − 0 = B
7 6 breq1d ⊢ B ∈ ℂ → B − 0 < x ↔ B < x
8 7 imbi2d ⊢ B ∈ ℂ → y < z → B − 0 < x ↔ y < z → B < x
9 8 ralimi ⊢ ∀ z ∈ A B ∈ ℂ → ∀ z ∈ A y < z → B − 0 < x ↔ y < z → B < x
10 ralbi ⊢ ∀ z ∈ A y < z → B − 0 < x ↔ y < z → B < x → ∀ z ∈ A y < z → B − 0 < x ↔ ∀ z ∈ A y < z → B < x
11 1 9 10 3syl ⊢ φ → ∀ z ∈ A y < z → B − 0 < x ↔ ∀ z ∈ A y < z → B < x
12 11 rexbidv ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ A y < z → B − 0 < x ↔ ∃ y ∈ ℝ ∀ z ∈ A y < z → B < x
13 12 ralbidv ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − 0 < x ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B < x
14 4 13 bitrd ⊢ φ → z ∈ A ⟼ B ⇝ℝ 0 ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B < x