Step | Hyp | Ref
| Expression |
1 | | negcl 8090 |
. . 3
⊢ (𝐶 ∈ ℂ → -𝐶 ∈
ℂ) |
2 | | addcn2 11238 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ -𝐶 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑤 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴)) |
3 | 1, 2 | syl3an3 1262 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑤 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴)) |
4 | | negcl 8090 |
. . . . . . . . 9
⊢ (𝑣 ∈ ℂ → -𝑣 ∈
ℂ) |
5 | | oveq1 5844 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = -𝑣 → (𝑤 − -𝐶) = (-𝑣 − -𝐶)) |
6 | 5 | fveq2d 5485 |
. . . . . . . . . . . . 13
⊢ (𝑤 = -𝑣 → (abs‘(𝑤 − -𝐶)) = (abs‘(-𝑣 − -𝐶))) |
7 | 6 | breq1d 3987 |
. . . . . . . . . . . 12
⊢ (𝑤 = -𝑣 → ((abs‘(𝑤 − -𝐶)) < 𝑧 ↔ (abs‘(-𝑣 − -𝐶)) < 𝑧)) |
8 | 7 | anbi2d 460 |
. . . . . . . . . . 11
⊢ (𝑤 = -𝑣 → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧))) |
9 | | oveq2 5845 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = -𝑣 → (𝑢 + 𝑤) = (𝑢 + -𝑣)) |
10 | 9 | oveq1d 5852 |
. . . . . . . . . . . . 13
⊢ (𝑤 = -𝑣 → ((𝑢 + 𝑤) − (𝐵 + -𝐶)) = ((𝑢 + -𝑣) − (𝐵 + -𝐶))) |
11 | 10 | fveq2d 5485 |
. . . . . . . . . . . 12
⊢ (𝑤 = -𝑣 → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) = (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶)))) |
12 | 11 | breq1d 3987 |
. . . . . . . . . . 11
⊢ (𝑤 = -𝑣 → ((abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴 ↔ (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶))) < 𝐴)) |
13 | 8, 12 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑤 = -𝑣 → ((((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧) → (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶))) < 𝐴))) |
14 | 13 | rspcv 2822 |
. . . . . . . . 9
⊢ (-𝑣 ∈ ℂ →
(∀𝑤 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧) → (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶))) < 𝐴))) |
15 | 4, 14 | syl 14 |
. . . . . . . 8
⊢ (𝑣 ∈ ℂ →
(∀𝑤 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧) → (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶))) < 𝐴))) |
16 | 15 | adantl 275 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (∀𝑤 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧) → (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶))) < 𝐴))) |
17 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ 𝑣 ∈
ℂ) |
18 | | simpll3 1027 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ 𝐶 ∈
ℂ) |
19 | 17, 18 | neg2subd 8218 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (-𝑣 − -𝐶) = (𝐶 − 𝑣)) |
20 | 19 | fveq2d 5485 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (abs‘(-𝑣
− -𝐶)) =
(abs‘(𝐶 − 𝑣))) |
21 | 18, 17 | abssubd 11122 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (abs‘(𝐶
− 𝑣)) =
(abs‘(𝑣 − 𝐶))) |
22 | 20, 21 | eqtrd 2197 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (abs‘(-𝑣
− -𝐶)) =
(abs‘(𝑣 − 𝐶))) |
23 | 22 | breq1d 3987 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ ((abs‘(-𝑣
− -𝐶)) < 𝑧 ↔ (abs‘(𝑣 − 𝐶)) < 𝑧)) |
24 | 23 | anbi2d 460 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (((abs‘(𝑢
− 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧))) |
25 | | negsub 8138 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 + -𝑣) = (𝑢 − 𝑣)) |
26 | 25 | adantll 468 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (𝑢 + -𝑣) = (𝑢 − 𝑣)) |
27 | | simpll2 1026 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ 𝐵 ∈
ℂ) |
28 | 27, 18 | negsubd 8207 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (𝐵 + -𝐶) = (𝐵 − 𝐶)) |
29 | 26, 28 | oveq12d 5855 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ ((𝑢 + -𝑣) − (𝐵 + -𝐶)) = ((𝑢 − 𝑣) − (𝐵 − 𝐶))) |
30 | 29 | fveq2d 5485 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (abs‘((𝑢 +
-𝑣) − (𝐵 + -𝐶))) = (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶)))) |
31 | 30 | breq1d 3987 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ ((abs‘((𝑢 +
-𝑣) − (𝐵 + -𝐶))) < 𝐴 ↔ (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴)) |
32 | 24, 31 | imbi12d 233 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ ((((abs‘(𝑢
− 𝐵)) < 𝑦 ∧ (abs‘(-𝑣 − -𝐶)) < 𝑧) → (abs‘((𝑢 + -𝑣) − (𝐵 + -𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))) |
33 | 16, 32 | sylibd 148 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
∧ 𝑣 ∈ ℂ)
→ (∀𝑤 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))) |
34 | 33 | ralrimdva 2544 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ 𝑢 ∈ ℂ)
→ (∀𝑤 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))) |
35 | 34 | ralimdva 2531 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (∀𝑢 ∈
ℂ ∀𝑤 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))) |
36 | 35 | reximdv 2565 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (∃𝑧 ∈
ℝ+ ∀𝑢 ∈ ℂ ∀𝑤 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))) |
37 | 36 | reximdv 2565 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑤 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑤 − -𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑤) − (𝐵 + -𝐶))) < 𝐴) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑢 ∈ ℂ
∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴))) |
38 | 3, 37 | mpd 13 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 − 𝑣) − (𝐵 − 𝐶))) < 𝐴)) |