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

Metamath Proof Explorer

Theorem muls1d

Description: Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 muls1d.1 ⊢ φ → A ∈ ℂ
2 muls1d.2 ⊢ φ → B ∈ ℂ
3 1cnd ⊢ φ → 1 ∈ ℂ
4 1 2 3 subdid ⊢ φ → A ⁢ B − 1 = A ⁢ B − A ⋅ 1
5 1 mulridd ⊢ φ → A ⋅ 1 = A
6 5 oveq2d ⊢ φ → A ⁢ B − A ⋅ 1 = A ⁢ B − A
7 4 6 eqtrd ⊢ φ → A ⁢ B − 1 = A ⁢ B − A