Proof of Theorem addsubeq4
Step | Hyp | Ref
| Expression |
1 | | eqcom 2039 |
. . 3
⊢ ((𝐶 − A) = (B −
𝐷) ↔ (B − 𝐷) = (𝐶 − A)) |
2 | | subcl 7007 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧
A ∈
ℂ) → (𝐶 −
A) ∈
ℂ) |
3 | 2 | ancoms 255 |
. . . . 5
⊢
((A ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐶 − A) ∈
ℂ) |
4 | | subadd 7011 |
. . . . . . 7
⊢
((B ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ (𝐶 − A) ∈ ℂ)
→ ((B − 𝐷) = (𝐶 − A) ↔ (𝐷 + (𝐶 − A)) = B)) |
5 | 4 | 3expa 1103 |
. . . . . 6
⊢
(((B ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧
(𝐶 − A) ∈ ℂ)
→ ((B − 𝐷) = (𝐶 − A) ↔ (𝐷 + (𝐶 − A)) = B)) |
6 | 5 | ancoms 255 |
. . . . 5
⊢ (((𝐶 − A) ∈ ℂ ∧ (B ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((B − 𝐷) = (𝐶 − A) ↔ (𝐷 + (𝐶 − A)) = B)) |
7 | 3, 6 | sylan 267 |
. . . 4
⊢
(((A ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧
(B ∈
ℂ ∧ 𝐷 ∈
ℂ)) → ((B − 𝐷) = (𝐶 − A) ↔ (𝐷 + (𝐶 − A)) = B)) |
8 | 7 | an4s 522 |
. . 3
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 ∈ ℂ
∧ 𝐷 ∈
ℂ)) → ((B − 𝐷) = (𝐶 − A) ↔ (𝐷 + (𝐶 − A)) = B)) |
9 | 1, 8 | syl5bb 181 |
. 2
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 ∈ ℂ
∧ 𝐷 ∈
ℂ)) → ((𝐶
− A) = (B − 𝐷) ↔ (𝐷 + (𝐶 − A)) = B)) |
10 | | addcom 6947 |
. . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐶 + 𝐷) = (𝐷 + 𝐶)) |
11 | 10 | adantl 262 |
. . . . . 6
⊢
((A ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (𝐶 + 𝐷) = (𝐷 + 𝐶)) |
12 | 11 | oveq1d 5470 |
. . . . 5
⊢
((A ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐶 + 𝐷) − A) = ((𝐷 + 𝐶) − A)) |
13 | | addsubass 7018 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧
A ∈
ℂ) → ((𝐷 + 𝐶) − A) = (𝐷 + (𝐶 − A))) |
14 | 13 | 3com12 1107 |
. . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧
A ∈
ℂ) → ((𝐷 + 𝐶) − A) = (𝐷 + (𝐶 − A))) |
15 | 14 | 3expa 1103 |
. . . . . 6
⊢ (((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧
A ∈
ℂ) → ((𝐷 + 𝐶) − A) = (𝐷 + (𝐶 − A))) |
16 | 15 | ancoms 255 |
. . . . 5
⊢
((A ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐷 + 𝐶) − A) = (𝐷 + (𝐶 − A))) |
17 | 12, 16 | eqtrd 2069 |
. . . 4
⊢
((A ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐶 + 𝐷) − A) = (𝐷 + (𝐶 − A))) |
18 | 17 | adantlr 446 |
. . 3
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 ∈ ℂ
∧ 𝐷 ∈
ℂ)) → ((𝐶 +
𝐷) − A) = (𝐷 + (𝐶 − A))) |
19 | 18 | eqeq1d 2045 |
. 2
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 ∈ ℂ
∧ 𝐷 ∈
ℂ)) → (((𝐶 +
𝐷) − A) = B ↔
(𝐷 + (𝐶 − A)) = B)) |
20 | | addcl 6804 |
. . 3
⊢ ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐶 + 𝐷) ∈
ℂ) |
21 | | subadd 7011 |
. . . . 5
⊢ (((𝐶 + 𝐷) ∈
ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ) → (((𝐶 + 𝐷) − A) = B ↔
(A + B)
= (𝐶 + 𝐷))) |
22 | 21 | 3expb 1104 |
. . . 4
⊢ (((𝐶 + 𝐷) ∈
ℂ ∧ (A ∈ ℂ ∧ B ∈ ℂ)) → (((𝐶 + 𝐷) − A) = B ↔
(A + B)
= (𝐶 + 𝐷))) |
23 | 22 | ancoms 255 |
. . 3
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 + 𝐷) ∈
ℂ) → (((𝐶 +
𝐷) − A) = B ↔
(A + B)
= (𝐶 + 𝐷))) |
24 | 20, 23 | sylan2 270 |
. 2
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 ∈ ℂ
∧ 𝐷 ∈
ℂ)) → (((𝐶 +
𝐷) − A) = B ↔
(A + B)
= (𝐶 + 𝐷))) |
25 | 9, 19, 24 | 3bitr2rd 206 |
1
⊢
(((A ∈ ℂ ∧
B ∈
ℂ) ∧ (𝐶 ∈ ℂ
∧ 𝐷 ∈
ℂ)) → ((A + B) = (𝐶 + 𝐷) ↔ (𝐶 − A) = (B −
𝐷))) |