Step | Hyp | Ref
| Expression |
1 | | rlim2.1 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) |
2 | | rlim2.2 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | | rlim2.3 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
4 | 1, 2, 3 | rlim2 14075 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑤 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
5 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ) |
6 | | rlim3.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 𝐷 ∈ ℝ) |
8 | 5, 7 | ifcld 4081 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ ℝ) |
9 | | max1 11890 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℝ ∧ 𝑤 ∈ ℝ) → 𝐷 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷)) |
10 | 6, 9 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → 𝐷 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷)) |
11 | | elicopnf 12140 |
. . . . . . . 8
⊢ (𝐷 ∈ ℝ → (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ (𝐷[,)+∞) ↔ (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ ℝ ∧ 𝐷 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷)))) |
12 | 7, 11 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ (𝐷[,)+∞) ↔ (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ ℝ ∧ 𝐷 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷)))) |
13 | 8, 10, 12 | mpbir2and 959 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ (𝐷[,)+∞)) |
14 | 2, 6 | jca 553 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ)) |
15 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝐷 ∈ ℝ) |
16 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑤 ∈ ℝ) |
17 | | max2 11892 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ ℝ ∧ 𝑤 ∈ ℝ) → 𝑤 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷)) |
18 | 15, 16, 17 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑤 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷)) |
19 | 16, 15 | ifcld 4081 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ ℝ) |
20 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) → 𝐴 ⊆
ℝ) |
21 | 20 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
22 | | letr 10010 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ ∧ if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑤 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∧ if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧) → 𝑤 ≤ 𝑧)) |
23 | 16, 19, 21, 22 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝑤 ≤ if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∧ if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧) → 𝑤 ≤ 𝑧)) |
24 | 18, 23 | mpand 707 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → 𝑤 ≤ 𝑧)) |
25 | 24 | imim1d 80 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) → ((𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
26 | 25 | ralimdva 2945 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐷 ∈ ℝ) ∧ 𝑤 ∈ ℝ) →
(∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑧 ∈ 𝐴 (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
27 | 14, 26 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑧 ∈ 𝐴 (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
28 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑦 = if(𝐷 ≤ 𝑤, 𝑤, 𝐷) → (𝑦 ≤ 𝑧 ↔ if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧)) |
29 | 28 | imbi1d 330 |
. . . . . . . 8
⊢ (𝑦 = if(𝐷 ≤ 𝑤, 𝑤, 𝐷) → ((𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) ↔ (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
30 | 29 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑦 = if(𝐷 ≤ 𝑤, 𝑤, 𝐷) → (∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
31 | 30 | rspcev 3282 |
. . . . . 6
⊢
((if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ∈ (𝐷[,)+∞) ∧ ∀𝑧 ∈ 𝐴 (if(𝐷 ≤ 𝑤, 𝑤, 𝐷) ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)) → ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)) |
32 | 13, 27, 31 | syl6an 566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
33 | 32 | rexlimdva 3013 |
. . . 4
⊢ (𝜑 → (∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
34 | 33 | ralimdv 2946 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑤 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑤 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
35 | 4, 34 | sylbid 229 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 → ∀𝑥 ∈ ℝ+
∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
36 | | pnfxr 9971 |
. . . . . 6
⊢ +∞
∈ ℝ* |
37 | | icossre 12125 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐷[,)+∞) ⊆
ℝ) |
38 | 6, 36, 37 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (𝐷[,)+∞) ⊆
ℝ) |
39 | | ssrexv 3630 |
. . . . 5
⊢ ((𝐷[,)+∞) ⊆ ℝ
→ (∃𝑦 ∈
(𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ (𝜑 → (∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
41 | 40 | ralimdv 2946 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
42 | 1, 2, 3 | rlim2 14075 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
43 | 41, 42 | sylibrd 248 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥) → (𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶)) |
44 | 35, 43 | impbid 201 |
1
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |