Theorem subdi

Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by NM, 18-Nov-2004)

	Ref	Expression
Assertion	subdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
2		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
3		subcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
4	3	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 − 𝐶 ) ∈ ℂ )
5	1 2 4	adddid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐶 + ( 𝐵 − 𝐶 ) ) ) = ( ( 𝐴 · 𝐶 ) + ( 𝐴 · ( 𝐵 − 𝐶 ) ) ) )
6		pncan3	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 + ( 𝐵 − 𝐶 ) ) = 𝐵 )
7	6	ancoms	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 + ( 𝐵 − 𝐶 ) ) = 𝐵 )
8	7	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐶 + ( 𝐵 − 𝐶 ) ) = 𝐵 )
9	8	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐶 + ( 𝐵 − 𝐶 ) ) ) = ( 𝐴 · 𝐵 ) )
10	5 9	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐶 ) + ( 𝐴 · ( 𝐵 − 𝐶 ) ) ) = ( 𝐴 · 𝐵 ) )
11		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
12	11	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
13		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
14	13	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
15		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 − 𝐶 ) ∈ ℂ ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) ∈ ℂ )
16	3 15	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) ∈ ℂ )
17	16	3impb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) ∈ ℂ )
18	12 14 17	subaddd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) = ( 𝐴 · ( 𝐵 − 𝐶 ) ) ↔ ( ( 𝐴 · 𝐶 ) + ( 𝐴 · ( 𝐵 − 𝐶 ) ) ) = ( 𝐴 · 𝐵 ) ) )
19	10 18	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) = ( 𝐴 · ( 𝐵 − 𝐶 ) ) )
20	19	eqcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) )