Proof of Theorem addcomd
| Step | Hyp | Ref
| Expression |
| 1 | | 1cnd 11256 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
| 2 | 1, 1 | addcld 11280 |
. . . . . . 7
⊢ (𝜑 → (1 + 1) ∈
ℂ) |
| 3 | | muld.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 4 | | addcomd.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 5 | 2, 3, 4 | adddid 11285 |
. . . . . 6
⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵))) |
| 6 | 3, 4 | addcld 11280 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
| 7 | | 1p1times 11432 |
. . . . . . 7
⊢ ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) ·
(𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
| 8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
| 9 | | 1p1times 11432 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((1 + 1)
· 𝐴) = (𝐴 + 𝐴)) |
| 10 | 3, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴)) |
| 11 | | 1p1times 11432 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ → ((1 + 1)
· 𝐵) = (𝐵 + 𝐵)) |
| 12 | 4, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵)) |
| 13 | 10, 12 | oveq12d 7449 |
. . . . . 6
⊢ (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵))) |
| 14 | 5, 8, 13 | 3eqtr3rd 2786 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
| 15 | 3, 3 | addcld 11280 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℂ) |
| 16 | 15, 4, 4 | addassd 11283 |
. . . . 5
⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵))) |
| 17 | 6, 3, 4 | addassd 11283 |
. . . . 5
⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵))) |
| 18 | 14, 16, 17 | 3eqtr4d 2787 |
. . . 4
⊢ (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵)) |
| 19 | 15, 4 | addcld 11280 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ) |
| 20 | 6, 3 | addcld 11280 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ) |
| 21 | | addcan2 11446 |
. . . . 5
⊢ ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))) |
| 22 | 19, 20, 4, 21 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))) |
| 23 | 18, 22 | mpbid 232 |
. . 3
⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)) |
| 24 | 3, 3, 4 | addassd 11283 |
. . 3
⊢ (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵))) |
| 25 | 3, 4, 3 | addassd 11283 |
. . 3
⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴))) |
| 26 | 23, 24, 25 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴))) |
| 27 | 4, 3 | addcld 11280 |
. . 3
⊢ (𝜑 → (𝐵 + 𝐴) ∈ ℂ) |
| 28 | | addcan 11445 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
| 29 | 3, 6, 27, 28 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
| 30 | 26, 29 | mpbid 232 |
1
⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |