Metamath Proof Explorer

Theorem rlim2lt

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

Ref Expression
Hypotheses rlim2.1 ⊢ φ → ∀ z ∈ A B ∈ ℂ
rlim2.2 ⊢ φ → A ⊆ ℝ
rlim2.3 ⊢ φ → C ∈ ℂ
Assertion rlim2lt ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x

Proof

Step Hyp Ref Expression
1 rlim2.1 ⊢ φ → ∀ z ∈ A B ∈ ℂ
2 rlim2.2 ⊢ φ → A ⊆ ℝ
3 rlim2.3 ⊢ φ → C ∈ ℂ
4 1 2 3 rlim2 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
5 simplr ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y ∈ ℝ
6 simpl ⊢ A ⊆ ℝ ∧ y ∈ ℝ → A ⊆ ℝ
7 6 sselda ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → z ∈ ℝ
8 ltle ⊢ y ∈ ℝ ∧ z ∈ ℝ → y < z → y ≤ z
9 5 7 8 syl2anc ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y < z → y ≤ z
10 9 imim1d ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y ≤ z → B − C < x → y < z → B − C < x
11 10 ralimdva ⊢ A ⊆ ℝ ∧ y ∈ ℝ → ∀ z ∈ A y ≤ z → B − C < x → ∀ z ∈ A y < z → B − C < x
12 2 11 sylan ⊢ φ ∧ y ∈ ℝ → ∀ z ∈ A y ≤ z → B − C < x → ∀ z ∈ A y < z → B − C < x
13 12 reximdva ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x → ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x
14 13 ralimdv ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x
15 4 14 sylbid ⊢ φ → z ∈ A ⟼ B ⇝ℝ C → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x
16 peano2re ⊢ y ∈ ℝ → y + 1 ∈ ℝ
17 16 adantl ⊢ φ ∧ y ∈ ℝ → y + 1 ∈ ℝ
18 ltp1 ⊢ y ∈ ℝ → y < y + 1
19 18 ad2antlr ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y < y + 1
20 16 ad2antlr ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y + 1 ∈ ℝ
21 ltletr ⊢ y ∈ ℝ ∧ y + 1 ∈ ℝ ∧ z ∈ ℝ → y < y + 1 ∧ y + 1 ≤ z → y < z
22 5 20 7 21 syl3anc ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y < y + 1 ∧ y + 1 ≤ z → y < z
23 19 22 mpand ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y + 1 ≤ z → y < z
24 23 imim1d ⊢ A ⊆ ℝ ∧ y ∈ ℝ ∧ z ∈ A → y < z → B − C < x → y + 1 ≤ z → B − C < x
25 24 ralimdva ⊢ A ⊆ ℝ ∧ y ∈ ℝ → ∀ z ∈ A y < z → B − C < x → ∀ z ∈ A y + 1 ≤ z → B − C < x
26 2 25 sylan ⊢ φ ∧ y ∈ ℝ → ∀ z ∈ A y < z → B − C < x → ∀ z ∈ A y + 1 ≤ z → B − C < x
27 breq1 ⊢ w = y + 1 → w ≤ z ↔ y + 1 ≤ z
28 27 rspceaimv ⊢ y + 1 ∈ ℝ ∧ ∀ z ∈ A y + 1 ≤ z → B − C < x → ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x
29 17 26 28 syl6an ⊢ φ ∧ y ∈ ℝ → ∀ z ∈ A y < z → B − C < x → ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x
30 29 rexlimdva ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x → ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x
31 30 ralimdv ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x → ∀ x ∈ ℝ + ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x
32 1 2 3 rlim2 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x
33 31 32 sylibrd ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x → z ∈ A ⟼ B ⇝ℝ C
34 15 33 impbid ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y < z → B − C < x