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

Metamath Proof Explorer

Theorem mulsubfacd

Description: Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018)

Ref Expression
Hypotheses muls1d.1 ⊢ φ → A ∈ ℂ
muls1d.2 ⊢ φ → B ∈ ℂ
Assertion mulsubfacd ⊢ φ → A ⁢ B − B = A − 1 ⁢ B

Proof

Step Hyp Ref Expression
1 muls1d.1 ⊢ φ → A ∈ ℂ
2 muls1d.2 ⊢ φ → B ∈ ℂ
3 1cnd ⊢ φ → 1 ∈ ℂ
4 1 3 2 subdird ⊢ φ → A − 1 ⁢ B = A ⁢ B − 1 ⁢ B
5 2 mullidd ⊢ φ → 1 ⁢ B = B
6 5 oveq2d ⊢ φ → A ⁢ B − 1 ⁢ B = A ⁢ B − B
7 4 6 eqtr2d ⊢ φ → A ⁢ B − B = A − 1 ⁢ B