Metamath Proof Explorer

Theorem divneg

Description: Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004)

Ref Expression
Assertion divneg ⊢A∈ℂ∧B∈ℂ∧B≠0→−AB=−AB

Proof

Step Hyp Ref Expression
1 reccl ⊢B∈ℂ∧B≠0→1B∈ℂ
2 mulneg1 ⊢A∈ℂ∧1B∈ℂ→−A⁢1B=−A⁢1B
3 1 2 sylan2 ⊢A∈ℂ∧B∈ℂ∧B≠0→−A⁢1B=−A⁢1B
4 3 3impb ⊢A∈ℂ∧B∈ℂ∧B≠0→−A⁢1B=−A⁢1B
5 negcl ⊢A∈ℂ→−A∈ℂ
6 divrec ⊢−A∈ℂ∧B∈ℂ∧B≠0→−AB=−A⁢1B
7 5 6 syl3an1 ⊢A∈ℂ∧B∈ℂ∧B≠0→−AB=−A⁢1B
8 divrec ⊢A∈ℂ∧B∈ℂ∧B≠0→AB=A⁢1B
9 8 negeqd ⊢A∈ℂ∧B∈ℂ∧B≠0→−AB=−A⁢1B
10 4 7 9 3eqtr4rd ⊢A∈ℂ∧B∈ℂ∧B≠0→−AB=−AB