Step | Hyp | Ref
| Expression |
1 | | addcn.2 |
. 2
⊢ + :(ℂ
× ℂ)⟶ℂ |
2 | | addcn.3 |
. . . . 5
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) |
3 | 2 | 3coml 1192 |
. . . 4
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) |
4 | | rpmincl 11137 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ 𝑧 ∈
ℝ+) → inf({𝑦, 𝑧}, ℝ, < ) ∈
ℝ+) |
5 | 4 | adantl 275 |
. . . . . 6
⊢ (((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) → inf({𝑦, 𝑧}, ℝ, < ) ∈
ℝ+) |
6 | | simpll1 1021 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑏 ∈ ℂ) |
7 | | simprl 521 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑢 ∈ ℂ) |
8 | | eqid 2157 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
9 | 8 | cnmetdval 12929 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝑏(abs ∘ − )𝑢) = (abs‘(𝑏 − 𝑢))) |
10 | | abssub 11001 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℂ ∧ 𝑢 ∈ ℂ) →
(abs‘(𝑏 − 𝑢)) = (abs‘(𝑢 − 𝑏))) |
11 | 9, 10 | eqtrd 2190 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝑏(abs ∘ − )𝑢) = (abs‘(𝑢 − 𝑏))) |
12 | 6, 7, 11 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑏(abs ∘ − )𝑢) = (abs‘(𝑢 − 𝑏))) |
13 | 12 | breq1d 3975 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ↔ (abs‘(𝑢 − 𝑏)) < inf({𝑦, 𝑧}, ℝ, < ))) |
14 | 7, 6 | subcld 8186 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑢 − 𝑏) ∈ ℂ) |
15 | 14 | abscld 11081 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘(𝑢 − 𝑏)) ∈ ℝ) |
16 | | simplrl 525 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑦 ∈ ℝ+) |
17 | 16 | rpred 9603 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑦 ∈ ℝ) |
18 | | simplrr 526 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑧 ∈ ℝ+) |
19 | 18 | rpred 9603 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑧 ∈ ℝ) |
20 | | ltmininf 11134 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝑢
− 𝑏)) ∈ ℝ
∧ 𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ)
→ ((abs‘(𝑢
− 𝑏)) < inf({𝑦, 𝑧}, ℝ, < ) ↔ ((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑢 − 𝑏)) < 𝑧))) |
21 | 15, 17, 19, 20 | syl3anc 1220 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑢 − 𝑏)) < inf({𝑦, 𝑧}, ℝ, < ) ↔ ((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑢 − 𝑏)) < 𝑧))) |
22 | 13, 21 | bitrd 187 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ↔ ((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑢 − 𝑏)) < 𝑧))) |
23 | | simpl 108 |
. . . . . . . . . 10
⊢
(((abs‘(𝑢
− 𝑏)) < 𝑦 ∧ (abs‘(𝑢 − 𝑏)) < 𝑧) → (abs‘(𝑢 − 𝑏)) < 𝑦) |
24 | 22, 23 | syl6bi 162 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) → (abs‘(𝑢 − 𝑏)) < 𝑦)) |
25 | | simpll2 1022 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑐 ∈ ℂ) |
26 | | simprr 522 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑣 ∈ ℂ) |
27 | 8 | cnmetdval 12929 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑐(abs ∘ − )𝑣) = (abs‘(𝑐 − 𝑣))) |
28 | | abssub 11001 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ ℂ ∧ 𝑣 ∈ ℂ) →
(abs‘(𝑐 − 𝑣)) = (abs‘(𝑣 − 𝑐))) |
29 | 27, 28 | eqtrd 2190 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑐(abs ∘ − )𝑣) = (abs‘(𝑣 − 𝑐))) |
30 | 25, 26, 29 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑐(abs ∘ − )𝑣) = (abs‘(𝑣 − 𝑐))) |
31 | 30 | breq1d 3975 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < ) ↔ (abs‘(𝑣 − 𝑐)) < inf({𝑦, 𝑧}, ℝ, < ))) |
32 | 26, 25 | subcld 8186 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑣 − 𝑐) ∈ ℂ) |
33 | 32 | abscld 11081 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘(𝑣 − 𝑐)) ∈ ℝ) |
34 | | ltmininf 11134 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝑣
− 𝑐)) ∈ ℝ
∧ 𝑦 ∈ ℝ
∧ 𝑧 ∈ ℝ)
→ ((abs‘(𝑣
− 𝑐)) < inf({𝑦, 𝑧}, ℝ, < ) ↔ ((abs‘(𝑣 − 𝑐)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧))) |
35 | 33, 17, 19, 34 | syl3anc 1220 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑣 − 𝑐)) < inf({𝑦, 𝑧}, ℝ, < ) ↔ ((abs‘(𝑣 − 𝑐)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧))) |
36 | 31, 35 | bitrd 187 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < ) ↔ ((abs‘(𝑣 − 𝑐)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧))) |
37 | | simpr 109 |
. . . . . . . . . 10
⊢
(((abs‘(𝑣
− 𝑐)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘(𝑣 − 𝑐)) < 𝑧) |
38 | 36, 37 | syl6bi 162 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < ) → (abs‘(𝑣 − 𝑐)) < 𝑧)) |
39 | 24, 38 | anim12d 333 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )) → ((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧))) |
40 | 1 | fovcl 5926 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑏 + 𝑐) ∈ ℂ) |
41 | 6, 25, 40 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑏 + 𝑐) ∈ ℂ) |
42 | 1 | fovcl 5926 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 + 𝑣) ∈ ℂ) |
43 | 42 | adantl 275 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑢 + 𝑣) ∈ ℂ) |
44 | 8 | cnmetdval 12929 |
. . . . . . . . . . . 12
⊢ (((𝑏 + 𝑐) ∈ ℂ ∧ (𝑢 + 𝑣) ∈ ℂ) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) = (abs‘((𝑏 + 𝑐) − (𝑢 + 𝑣)))) |
45 | | abssub 11001 |
. . . . . . . . . . . 12
⊢ (((𝑏 + 𝑐) ∈ ℂ ∧ (𝑢 + 𝑣) ∈ ℂ) → (abs‘((𝑏 + 𝑐) − (𝑢 + 𝑣))) = (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐)))) |
46 | 44, 45 | eqtrd 2190 |
. . . . . . . . . . 11
⊢ (((𝑏 + 𝑐) ∈ ℂ ∧ (𝑢 + 𝑣) ∈ ℂ) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) = (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐)))) |
47 | 41, 43, 46 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) = (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐)))) |
48 | 47 | breq1d 3975 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎 ↔ (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) |
49 | 48 | biimprd 157 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎 → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎)) |
50 | 39, 49 | imim12d 74 |
. . . . . . 7
⊢ ((((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎) → (((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
51 | 50 | ralimdvva 2526 |
. . . . . 6
⊢ (((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎) → ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
52 | | breq2 3969 |
. . . . . . . . . 10
⊢ (𝑥 = inf({𝑦, 𝑧}, ℝ, < ) → ((𝑏(abs ∘ − )𝑢) < 𝑥 ↔ (𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ))) |
53 | | breq2 3969 |
. . . . . . . . . 10
⊢ (𝑥 = inf({𝑦, 𝑧}, ℝ, < ) → ((𝑐(abs ∘ − )𝑣) < 𝑥 ↔ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < ))) |
54 | 52, 53 | anbi12d 465 |
. . . . . . . . 9
⊢ (𝑥 = inf({𝑦, 𝑧}, ℝ, < ) → (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) ↔ ((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )))) |
55 | 54 | imbi1d 230 |
. . . . . . . 8
⊢ (𝑥 = inf({𝑦, 𝑧}, ℝ, < ) → ((((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎) ↔ (((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
56 | 55 | 2ralbidv 2481 |
. . . . . . 7
⊢ (𝑥 = inf({𝑦, 𝑧}, ℝ, < ) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
57 | 56 | rspcev 2816 |
. . . . . 6
⊢
((inf({𝑦, 𝑧}, ℝ, < ) ∈
ℝ+ ∧ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < inf({𝑦, 𝑧}, ℝ, < ) ∧ (𝑐(abs ∘ − )𝑣) < inf({𝑦, 𝑧}, ℝ, < )) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎)) → ∃𝑥 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎)) |
58 | 5, 51, 57 | syl6an 1414 |
. . . . 5
⊢ (((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
∧ (𝑦 ∈
ℝ+ ∧ 𝑧
∈ ℝ+)) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎) → ∃𝑥 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
59 | 58 | rexlimdvva 2582 |
. . . 4
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
→ (∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎) → ∃𝑥 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
60 | 3, 59 | mpd 13 |
. . 3
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ∧ 𝑎 ∈ ℝ+)
→ ∃𝑥 ∈
ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎)) |
61 | 60 | rgen3 2544 |
. 2
⊢
∀𝑏 ∈
ℂ ∀𝑐 ∈
ℂ ∀𝑎 ∈
ℝ+ ∃𝑥 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((𝑏(abs ∘ − )𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎) |
62 | | cnxmet 12931 |
. . 3
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
63 | | addcncntop.j |
. . . 4
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
64 | 63, 63, 63 | txmetcn 12919 |
. . 3
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (abs ∘ −
) ∈ (∞Met‘ℂ) ∧ (abs ∘ − ) ∈
(∞Met‘ℂ)) → ( + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ↔ ( + :(ℂ ×
ℂ)⟶ℂ ∧ ∀𝑏 ∈ ℂ ∀𝑐 ∈ ℂ ∀𝑎 ∈ ℝ+ ∃𝑥 ∈ ℝ+
∀𝑢 ∈ ℂ
∀𝑣 ∈ ℂ
(((𝑏(abs ∘ −
)𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎)))) |
65 | 62, 62, 62, 64 | mp3an 1319 |
. 2
⊢ ( + ∈
((𝐽 ×t
𝐽) Cn 𝐽) ↔ ( + :(ℂ ×
ℂ)⟶ℂ ∧ ∀𝑏 ∈ ℂ ∀𝑐 ∈ ℂ ∀𝑎 ∈ ℝ+ ∃𝑥 ∈ ℝ+
∀𝑢 ∈ ℂ
∀𝑣 ∈ ℂ
(((𝑏(abs ∘ −
)𝑢) < 𝑥 ∧ (𝑐(abs ∘ − )𝑣) < 𝑥) → ((𝑏 + 𝑐)(abs ∘ − )(𝑢 + 𝑣)) < 𝑎))) |
66 | 1, 61, 65 | mpbir2an 927 |
1
⊢ + ∈
((𝐽 ×t
𝐽) Cn 𝐽) |