Metamath Proof Explorer

Theorem muladd11r

Description: A simple product of sums expansion. (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion muladd11r ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + 1 ⁢ B + 1 = A ⁢ B + A + B + 1

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
2 1cnd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 ∈ ℂ
3 1 2 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + 1 = 1 + A
4 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
5 4 2 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ → B + 1 = 1 + B
6 3 5 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + 1 ⁢ B + 1 = 1 + A ⁢ 1 + B
7 muladd11 ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ 1 + B = 1 + A + B + A ⁢ B
8 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
9 4 8 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → B + A ⁢ B ∈ ℂ
10 2 1 9 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A + B + A ⁢ B = 1 + A + B + A ⁢ B
11 1 9 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A ⁢ B ∈ ℂ
12 2 11 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A + B + A ⁢ B = A + B + A ⁢ B + 1
13 1 4 8 addassd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A ⁢ B = A + B + A ⁢ B
14 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
15 14 8 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A ⁢ B = A ⁢ B + A + B
16 13 15 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A ⁢ B = A ⁢ B + A + B
17 16 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B + A ⁢ B + 1 = A ⁢ B + A + B + 1
18 10 12 17 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A + B + A ⁢ B = A ⁢ B + A + B + 1
19 6 7 18 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + 1 ⁢ B + 1 = A ⁢ B + A + B + 1