Proof of Theorem addcn2
| Step | Hyp | Ref
| Expression |
| 1 | | rphalfcl 13062 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (𝐴 / 2) ∈
ℝ+) |
| 2 | 1 | 3ad2ant1 1134 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (𝐴 / 2) ∈
ℝ+) |
| 3 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝑢 ∈
ℂ) |
| 4 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐵 ∈
ℂ) |
| 5 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝑣 ∈
ℂ) |
| 6 | 3, 4, 5 | pnpcan2d 11658 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝑢 + 𝑣) − (𝐵 + 𝑣)) = (𝑢 − 𝐵)) |
| 7 | 6 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) = (abs‘(𝑢 − 𝐵))) |
| 8 | 7 | breq1d 5153 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ↔ (abs‘(𝑢 − 𝐵)) < (𝐴 / 2))) |
| 9 | | simpl3 1194 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐶 ∈
ℂ) |
| 10 | 4, 5, 9 | pnpcand 11657 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝐵 + 𝑣) − (𝐵 + 𝐶)) = (𝑣 − 𝐶)) |
| 11 | 10 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝐵 +
𝑣) − (𝐵 + 𝐶))) = (abs‘(𝑣 − 𝐶))) |
| 12 | 11 | breq1d 5153 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘((𝐵 +
𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2) ↔ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2))) |
| 13 | 8, 12 | anbi12d 632 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 + 𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2)) ↔ ((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)))) |
| 14 | | addcl 11237 |
. . . . . 6
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 + 𝑣) ∈ ℂ) |
| 15 | 14 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝑢 + 𝑣) ∈
ℂ) |
| 16 | 4, 9 | addcld 11280 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 + 𝐶) ∈
ℂ) |
| 17 | 4, 5 | addcld 11280 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 + 𝑣) ∈
ℂ) |
| 18 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐴 ∈
ℝ+) |
| 19 | 18 | rpred 13077 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐴 ∈
ℝ) |
| 20 | | abs3lem 15377 |
. . . . 5
⊢ ((((𝑢 + 𝑣) ∈ ℂ ∧ (𝐵 + 𝐶) ∈ ℂ) ∧ ((𝐵 + 𝑣) ∈ ℂ ∧ 𝐴 ∈ ℝ)) →
(((abs‘((𝑢 + 𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 + 𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
| 21 | 15, 16, 17, 19, 20 | syl22anc 839 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘((𝑢 +
𝑣) − (𝐵 + 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 + 𝑣) − (𝐵 + 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
| 22 | 13, 21 | sylbird 260 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘(𝑢
− 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
| 23 | 22 | ralrimivva 3202 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∀𝑢 ∈
ℂ ∀𝑣 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
| 24 | | breq2 5147 |
. . . . . 6
⊢ (𝑦 = (𝐴 / 2) → ((abs‘(𝑢 − 𝐵)) < 𝑦 ↔ (abs‘(𝑢 − 𝐵)) < (𝐴 / 2))) |
| 25 | 24 | anbi1d 631 |
. . . . 5
⊢ (𝑦 = (𝐴 / 2) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧))) |
| 26 | 25 | imbi1d 341 |
. . . 4
⊢ (𝑦 = (𝐴 / 2) → ((((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
| 27 | 26 | 2ralbidv 3221 |
. . 3
⊢ (𝑦 = (𝐴 / 2) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
| 28 | | breq2 5147 |
. . . . . 6
⊢ (𝑧 = (𝐴 / 2) → ((abs‘(𝑣 − 𝐶)) < 𝑧 ↔ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2))) |
| 29 | 28 | anbi2d 630 |
. . . . 5
⊢ (𝑧 = (𝐴 / 2) → (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)))) |
| 30 | 29 | imbi1d 341 |
. . . 4
⊢ (𝑧 = (𝐴 / 2) → ((((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
| 31 | 30 | 2ralbidv 3221 |
. . 3
⊢ (𝑧 = (𝐴 / 2) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴))) |
| 32 | 27, 31 | rspc2ev 3635 |
. 2
⊢ (((𝐴 / 2) ∈ ℝ+
∧ (𝐴 / 2) ∈
ℝ+ ∧ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < (𝐴 / 2) ∧ (abs‘(𝑣 − 𝐶)) < (𝐴 / 2)) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑢 ∈ ℂ
∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |
| 33 | 2, 2, 23, 32 | syl3anc 1373 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝐵 + 𝐶))) < 𝐴)) |