Step | Hyp | Ref
| Expression |
1 | | rlim2.1 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) |
2 | | eqid 2610 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 ↦ 𝐵) = (𝑧 ∈ 𝐴 ↦ 𝐵) |
3 | 2 | fmpt 6289 |
. . . 4
⊢
(∀𝑧 ∈
𝐴 𝐵 ∈ ℂ ↔ (𝑧 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
4 | 1, 3 | sylib 207 |
. . 3
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
5 | | rlim2.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
6 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) = ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤)) |
7 | 4, 5, 6 | rlim 14074 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥)))) |
8 | | rlim2.3 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
9 | 8 | biantrurd 528 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥)))) |
10 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑧 𝑦 ≤ 𝑤 |
11 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑧abs |
12 | | nffvmpt1 6111 |
. . . . . . . . . 10
⊢
Ⅎ𝑧((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) |
13 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑧
− |
14 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑧𝐶 |
15 | 12, 13, 14 | nfov 6575 |
. . . . . . . . 9
⊢
Ⅎ𝑧(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶) |
16 | 11, 15 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑧(abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) |
17 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑧
< |
18 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑧𝑥 |
19 | 16, 17, 18 | nfbr 4629 |
. . . . . . 7
⊢
Ⅎ𝑧(abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥 |
20 | 10, 19 | nfim 1813 |
. . . . . 6
⊢
Ⅎ𝑧(𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) |
21 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑤(𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) |
22 | | breq2 4587 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (𝑦 ≤ 𝑤 ↔ 𝑦 ≤ 𝑧)) |
23 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) = ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
24 | 23 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶) = (((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) |
25 | 24 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) = (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶))) |
26 | 25 | breq1d 4593 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥 ↔ (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥)) |
27 | 22, 26 | imbi12d 333 |
. . . . . 6
⊢ (𝑤 = 𝑧 → ((𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥))) |
28 | 20, 21, 27 | cbvral 3143 |
. . . . 5
⊢
(∀𝑤 ∈
𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥)) |
29 | 2 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) = 𝐵) |
30 | 29 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶) = (𝐵 − 𝐶)) |
31 | 30 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) = (abs‘(𝐵 − 𝐶))) |
32 | 31 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥 ↔ (abs‘(𝐵 − 𝐶)) < 𝑥)) |
33 | 32 | imbi2d 329 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
34 | 33 | ralimiaa 2935 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 𝐵 ∈ ℂ → ∀𝑧 ∈ 𝐴 ((𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
35 | | ralbi 3050 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 ((𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)) → (∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
36 | 1, 34, 35 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
37 | 28, 36 | syl5bb 271 |
. . . 4
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
38 | 37 | rexbidv 3034 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
39 | 38 | ralbidv 2969 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
40 | 7, 9, 39 | 3bitr2d 295 |
1
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |