Proof of Theorem muladd11r
Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
2 | | 1cnd 7936 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 1 ∈
ℂ) |
3 | 1, 2 | addcomd 8070 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 1) = (1 + 𝐴)) |
4 | | simpr 109 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
5 | 4, 2 | addcomd 8070 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + 1) = (1 + 𝐵)) |
6 | 3, 5 | oveq12d 5871 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = ((1 + 𝐴) · (1 + 𝐵))) |
7 | | muladd11 8052 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 +
𝐴) · (1 + 𝐵)) = ((1 + 𝐴) + (𝐵 + (𝐴 · 𝐵)))) |
8 | | mulcl 7901 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
9 | 4, 8 | addcld 7939 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 + (𝐴 · 𝐵)) ∈ ℂ) |
10 | 2, 1, 9 | addassd 7942 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 +
𝐴) + (𝐵 + (𝐴 · 𝐵))) = (1 + (𝐴 + (𝐵 + (𝐴 · 𝐵))))) |
11 | 1, 9 | addcld 7939 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 + (𝐴 · 𝐵))) ∈ ℂ) |
12 | 2, 11 | addcomd 8070 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (1 +
(𝐴 + (𝐵 + (𝐴 · 𝐵)))) = ((𝐴 + (𝐵 + (𝐴 · 𝐵))) + 1)) |
13 | 1, 4, 8 | addassd 7942 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐴 · 𝐵)) = (𝐴 + (𝐵 + (𝐴 · 𝐵)))) |
14 | | addcl 7899 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
15 | 14, 8 | addcomd 8070 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) + (𝐴 · 𝐵)) = ((𝐴 · 𝐵) + (𝐴 + 𝐵))) |
16 | 13, 15 | eqtr3d 2205 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 + (𝐴 · 𝐵))) = ((𝐴 · 𝐵) + (𝐴 + 𝐵))) |
17 | 16 | oveq1d 5868 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (𝐵 + (𝐴 · 𝐵))) + 1) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) |
18 | 10, 12, 17 | 3eqtrd 2207 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 +
𝐴) + (𝐵 + (𝐴 · 𝐵))) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) |
19 | 6, 7, 18 | 3eqtrd 2207 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) |