Metamath Proof Explorer

Theorem rlim3

Description: Restrict the range of the domain bound to reals greater than some D e. RR . (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlim2.1 ⊢ φ → ∀ z ∈ A B ∈ ℂ
rlim2.2 ⊢ φ → A ⊆ ℝ
rlim2.3 ⊢ φ → C ∈ ℂ
rlim3.4 ⊢ φ → D ∈ ℝ
Assertion rlim3 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ D +∞ ∀ 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 rlim3.4 ⊢ φ → D ∈ ℝ
5 1 2 3 rlim2 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x
6 simpr ⊢ φ ∧ w ∈ ℝ → w ∈ ℝ
7 4 adantr ⊢ φ ∧ w ∈ ℝ → D ∈ ℝ
8 6 7 ifcld ⊢ φ ∧ w ∈ ℝ → if D ≤ w w D ∈ ℝ
9 max1 ⊢ D ∈ ℝ ∧ w ∈ ℝ → D ≤ if D ≤ w w D
10 4 9 sylan ⊢ φ ∧ w ∈ ℝ → D ≤ if D ≤ w w D
11 elicopnf ⊢ D ∈ ℝ → if D ≤ w w D ∈ D +∞ ↔ if D ≤ w w D ∈ ℝ ∧ D ≤ if D ≤ w w D
12 7 11 syl ⊢ φ ∧ w ∈ ℝ → if D ≤ w w D ∈ D +∞ ↔ if D ≤ w w D ∈ ℝ ∧ D ≤ if D ≤ w w D
13 8 10 12 mpbir2and ⊢ φ ∧ w ∈ ℝ → if D ≤ w w D ∈ D +∞
14 2 4 jca ⊢ φ → A ⊆ ℝ ∧ D ∈ ℝ
15 max2 ⊢ D ∈ ℝ ∧ w ∈ ℝ → w ≤ if D ≤ w w D
16 15 ad4ant23 ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → w ≤ if D ≤ w w D
17 simplr ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → w ∈ ℝ
18 simpllr ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → D ∈ ℝ
19 17 18 ifcld ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → if D ≤ w w D ∈ ℝ
20 simpll ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ → A ⊆ ℝ
21 20 sselda ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → z ∈ ℝ
22 letr ⊢ w ∈ ℝ ∧ if D ≤ w w D ∈ ℝ ∧ z ∈ ℝ → w ≤ if D ≤ w w D ∧ if D ≤ w w D ≤ z → w ≤ z
23 17 19 21 22 syl3anc ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → w ≤ if D ≤ w w D ∧ if D ≤ w w D ≤ z → w ≤ z
24 16 23 mpand ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → if D ≤ w w D ≤ z → w ≤ z
25 24 imim1d ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ ∧ z ∈ A → w ≤ z → B − C < x → if D ≤ w w D ≤ z → B − C < x
26 25 ralimdva ⊢ A ⊆ ℝ ∧ D ∈ ℝ ∧ w ∈ ℝ → ∀ z ∈ A w ≤ z → B − C < x → ∀ z ∈ A if D ≤ w w D ≤ z → B − C < x
27 14 26 sylan ⊢ φ ∧ w ∈ ℝ → ∀ z ∈ A w ≤ z → B − C < x → ∀ z ∈ A if D ≤ w w D ≤ z → B − C < x
28 breq1 ⊢ y = if D ≤ w w D → y ≤ z ↔ if D ≤ w w D ≤ z
29 28 rspceaimv ⊢ if D ≤ w w D ∈ D +∞ ∧ ∀ z ∈ A if D ≤ w w D ≤ z → B − C < x → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x
30 13 27 29 syl6an ⊢ φ ∧ w ∈ ℝ → ∀ z ∈ A w ≤ z → B − C < x → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x
31 30 rexlimdva ⊢ φ → ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x
32 31 ralimdv ⊢ φ → ∀ x ∈ ℝ + ∃ w ∈ ℝ ∀ z ∈ A w ≤ z → B − C < x → ∀ x ∈ ℝ + ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x
33 5 32 sylbid ⊢ φ → z ∈ A ⟼ B ⇝ℝ C → ∀ x ∈ ℝ + ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x
34 pnfxr ⊢ +∞ ∈ ℝ *
35 icossre ⊢ D ∈ ℝ ∧ +∞ ∈ ℝ * → D +∞ ⊆ ℝ
36 4 34 35 sylancl ⊢ φ → D +∞ ⊆ ℝ
37 ssrexv ⊢ D +∞ ⊆ ℝ → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x → ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
38 36 37 syl ⊢ φ → ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x → ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
39 38 ralimdv ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x → ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
40 1 2 3 rlim2 ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ ℝ ∀ z ∈ A y ≤ z → B − C < x
41 39 40 sylibrd ⊢ φ → ∀ x ∈ ℝ + ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x → z ∈ A ⟼ B ⇝ℝ C
42 33 41 impbid ⊢ φ → z ∈ A ⟼ B ⇝ℝ C ↔ ∀ x ∈ ℝ + ∃ y ∈ D +∞ ∀ z ∈ A y ≤ z → B − C < x