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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 𝐶 ) ) )