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