Theorem muladd11

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

	Ref	Expression
Assertion	muladd11	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\left(1+B\right)=1+A+B+AB$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		addcl	$$⊢\left(1\in ℂ\wedge A\in ℂ\right)\to 1+A\in ℂ$$
3	1 2	mpan	$$⊢A\in ℂ\to 1+A\in ℂ$$
4		adddi	$$⊢\left(1+A\in ℂ\wedge 1\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\left(1+B\right)=\left(1+A\right)\cdot 1+\left(1+A\right)B$$
5	1 4	mp3an2	$$⊢\left(1+A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\left(1+B\right)=\left(1+A\right)\cdot 1+\left(1+A\right)B$$
6	3 5	sylan	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\left(1+B\right)=\left(1+A\right)\cdot 1+\left(1+A\right)B$$
7	3	mulridd	$$⊢A\in ℂ\to \left(1+A\right)\cdot 1=1+A$$
8	7	adantr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\cdot 1=1+A$$
9		adddir	$$⊢\left(1\in ℂ\wedge A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)B=1B+AB$$
10	1 9	mp3an1	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)B=1B+AB$$
11		mullid	$$⊢B\in ℂ\to 1B=B$$
12	11	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 1B=B$$
13	12	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 1B+AB=B+AB$$
14	10 13	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)B=B+AB$$
15	8 14	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\cdot 1+\left(1+A\right)B=1+A+B+AB$$
16	6 15	eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(1+A\right)\left(1+B\right)=1+A+B+AB$$