Proof of Theorem addcn2
Step | Hyp | Ref
| Expression |
1 | | rphalfcl 12613 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (𝐴 / 2) ∈
ℝ+) |
2 | 1 | 3ad2ant1 1135 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (𝐴 / 2) ∈
ℝ+) |
3 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝑢 ∈
ℂ) |
4 | | simpl2 1194 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐵 ∈
ℂ) |
5 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝑣 ∈
ℂ) |
6 | 3, 4, 5 | pnpcan2d 11227 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝑢 + 𝑣) − (𝐵 + 𝑣)) = (𝑢 − 𝐵)) |
7 | 6 | fveq2d 6721 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) = (abs‘(𝑢 − 𝐵))) |
8 | 7 | breq1d 5063 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ↔ (abs‘(𝑢 − 𝐵)) < (𝐴 / 2))) |
9 | | simpl3 1195 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐶 ∈
ℂ) |
10 | 4, 5, 9 | pnpcand 11226 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝐵 + 𝑣) − (𝐵 + 𝐶)) = (𝑣 − 𝐶)) |
11 | 10 | fveq2d 6721 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝐵 +
𝑣) − (𝐵 + 𝐶))) = (abs‘(𝑣 − 𝐶))) |
12 | 11 | breq1d 5063 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘((𝐵 +
𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2) ↔ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2))) |
13 | 8, 12 | anbi12d 634 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 + 𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2)) ↔ ((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)))) |
14 | | addcl 10811 |
. . . . . 6
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 + 𝑣) ∈ ℂ) |
15 | 14 | adantl 485 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝑢 + 𝑣) ∈
ℂ) |
16 | 4, 9 | addcld 10852 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 + 𝐶) ∈
ℂ) |
17 | 4, 5 | addcld 10852 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 + 𝑣) ∈
ℂ) |
18 | | simpl1 1193 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐴 ∈
ℝ+) |
19 | 18 | rpred 12628 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐴 ∈
ℝ) |
20 | | abs3lem 14902 |
. . . . 5
⊢ ((((𝑢 + 𝑣) ∈ ℂ ∧ (𝐵 + 𝐶) ∈ ℂ) ∧ ((𝐵 + 𝑣) ∈ ℂ ∧ 𝐴 ∈ ℝ)) →
(((abs‘((𝑢 + 𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 + 𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
21 | 15, 16, 17, 19, 20 | syl22anc 839 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 + 𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
22 | 13, 21 | sylbird 263 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘(𝑢
− 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
23 | 22 | ralrimivva 3112 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∀𝑢 ∈
ℂ ∀𝑣 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
24 | | breq2 5057 |
. . . . . 6
⊢ (𝑦 = (𝐴 / 2) → ((abs‘(𝑢 − 𝐵)) < 𝑦 ↔ (abs‘(𝑢 − 𝐵)) < (𝐴 / 2))) |
25 | 24 | anbi1d 633 |
. . . . 5
⊢ (𝑦 = (𝐴 / 2) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧))) |
26 | 25 | imbi1d 345 |
. . . 4
⊢ (𝑦 = (𝐴 / 2) → ((((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
27 | 26 | 2ralbidv 3120 |
. . 3
⊢ (𝑦 = (𝐴 / 2) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
28 | | breq2 5057 |
. . . . . 6
⊢ (𝑧 = (𝐴 / 2) → ((abs‘(𝑣 − 𝐶)) < 𝑧 ↔ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2))) |
29 | 28 | anbi2d 632 |
. . . . 5
⊢ (𝑧 = (𝐴 / 2) → (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)))) |
30 | 29 | imbi1d 345 |
. . . 4
⊢ (𝑧 = (𝐴 / 2) → ((((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
31 | 30 | 2ralbidv 3120 |
. . 3
⊢ (𝑧 = (𝐴 / 2) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
32 | 27, 31 | rspc2ev 3549 |
. 2
⊢ (((𝐴 / 2) ∈ ℝ+
∧ (𝐴 / 2) ∈
ℝ+ ∧ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑢 ∈ ℂ
∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
33 | 2, 2, 23, 32 | syl3anc 1373 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |