Theorem muladd11r

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

	Ref	Expression
Assertion	muladd11r	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 1 ) · ( 𝐵 + 1 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 𝐴 + 𝐵 ) ) + 1 ) )

Proof

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