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∈AB∈ℂ
rlim0.2 ⊢φ→A⊆ℝ
Assertion rlim0lt ⊢φ→z∈A⟼B⇝ℝ0↔∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B<x

Proof

Step Hyp Ref Expression
1 rlim0.1 ⊢φ→∀z∈AB∈ℂ
2 rlim0.2 ⊢φ→A⊆ℝ
3 0cnd ⊢φ→0∈ℂ
4 1 2 3 rlim2lt ⊢φ→z∈A⟼B⇝ℝ0↔∀x∈ℝ+∃y∈ℝ∀z∈Ay<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∈AB∈ℂ→∀z∈Ay<z→B−0<x↔y<z→B<x
10 ralbi ⊢∀z∈Ay<z→B−0<x↔y<z→B<x→∀z∈Ay<z→B−0<x↔∀z∈Ay<z→B<x
11 1 9 10 3syl ⊢φ→∀z∈Ay<z→B−0<x↔∀z∈Ay<z→B<x
12 11 rexbidv ⊢φ→∃y∈ℝ∀z∈Ay<z→B−0<x↔∃y∈ℝ∀z∈Ay<z→B<x
13 12 ralbidv ⊢φ→∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B−0<x↔∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B<x
14 4 13 bitrd ⊢φ→z∈A⟼B⇝ℝ0↔∀x∈ℝ+∃y∈ℝ∀z∈Ay<z→B<x