This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )