| Step | Hyp | Ref
| Expression |
| 1 | | rlim2.1 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) |
| 2 | | rlim2.2 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 3 | | rlim2.3 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 4 | 1, 2, 3 | rlim2 15532 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 5 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ ℝ) |
| 6 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) → 𝐴 ⊆
ℝ) |
| 7 | 6 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
| 8 | | ltle 11349 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
| 9 | 5, 7, 8 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
| 10 | 9 | imim1d 82 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 11 | 10 | ralimdva 3167 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) →
(∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 12 | 2, 11 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 13 | 12 | reximdva 3168 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 14 | 13 | ralimdv 3169 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 15 | 4, 14 | sylbid 240 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 → ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 16 | | peano2re 11434 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈
ℝ) |
| 17 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 1) ∈ ℝ) |
| 18 | | ltp1 12107 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1)) |
| 19 | 18 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑦 < (𝑦 + 1)) |
| 20 | 16 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (𝑦 + 1) ∈ ℝ) |
| 21 | | ltletr 11353 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ (𝑦 + 1) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 < (𝑦 + 1) ∧ (𝑦 + 1) ≤ 𝑧) → 𝑦 < 𝑧)) |
| 22 | 5, 20, 7, 21 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝑦 < (𝑦 + 1) ∧ (𝑦 + 1) ≤ 𝑧) → 𝑦 < 𝑧)) |
| 23 | 19, 22 | mpand 695 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝑦 + 1) ≤ 𝑧 → 𝑦 < 𝑧)) |
| 24 | 23 | imim1d 82 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ((𝑦 + 1) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 25 | 24 | ralimdva 3167 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ) →
(∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑧 ∈ 𝐴 ((𝑦 + 1) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 26 | 2, 25 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑧 ∈ 𝐴 ((𝑦 + 1) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 27 | | breq1 5146 |
. . . . . . 7
⊢ (𝑤 = (𝑦 + 1) → (𝑤 ≤ 𝑧 ↔ (𝑦 + 1) ≤ 𝑧)) |
| 28 | 27 | rspceaimv 3628 |
. . . . . 6
⊢ (((𝑦 + 1) ∈ ℝ ∧
∀𝑧 ∈ 𝐴 ((𝑦 + 1) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)) |
| 29 | 17, 26, 28 | syl6an 684 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 30 | 29 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 31 | 30 | ralimdv 3169 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 32 | 1, 2, 3 | rlim2 15532 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑤 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
| 33 | 31, 32 | sylibrd 259 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)) |
| 34 | 15, 33 | impbid 212 |
1
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |