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

Metamath Proof Explorer

Theorem muladd11

Description: A simple product of sums expansion. (Contributed by NM, 21-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 addcl ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → 1 + A ∈ ℂ
3 1 2 mpan ⊢ A ∈ ℂ → 1 + A ∈ ℂ
4 adddi ⊢ 1 + A ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ 1 + B = 1 + A ⋅ 1 + 1 + A ⁢ B
5 1 4 mp3an2 ⊢ 1 + A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ 1 + B = 1 + A ⋅ 1 + 1 + A ⁢ B
6 3 5 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ 1 + B = 1 + A ⋅ 1 + 1 + A ⁢ B
7 3 mulridd ⊢ A ∈ ℂ → 1 + A ⋅ 1 = 1 + A
8 7 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⋅ 1 = 1 + A
9 adddir ⊢ 1 ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ B = 1 ⁢ B + A ⁢ B
10 1 9 mp3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ B = 1 ⁢ B + A ⁢ B
11 mullid ⊢ B ∈ ℂ → 1 ⁢ B = B
12 11 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 ⁢ B = B
13 12 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 ⁢ B + A ⁢ B = B + A ⁢ B
14 10 13 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ B = B + A ⁢ B
15 8 14 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⋅ 1 + 1 + A ⁢ B = 1 + A + B + A ⁢ B
16 6 15 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 1 + A ⁢ 1 + B = 1 + A + B + A ⁢ B