Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Multiplication
mulneg12
Next ⟩
mul2neg
Metamath Proof Explorer
Ascii
Unicode
Theorem
mulneg12
Description:
Swap the negative sign in a product.
(Contributed by
NM
, 30-Jul-2004)
Ref
Expression
Assertion
mulneg12
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
−
A
⁢
B
=
A
⁢
−
B
Proof
Step
Hyp
Ref
Expression
1
mulneg1
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
−
A
⁢
B
=
−
A
⁢
B
2
mulneg2
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
A
⁢
−
B
=
−
A
⁢
B
3
1
2
eqtr4d
⊢
A
∈
ℂ
∧
B
∈
ℂ
→
−
A
⁢
B
=
A
⁢
−
B