# Metamath Proof Explorer

## Theorem divneg

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

Ref Expression
Assertion divneg ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{A}}{{B}}=\frac{-{A}}{{B}}$

### Proof

Step Hyp Ref Expression
1 reccl ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to \frac{1}{{B}}\in ℂ$
2 mulneg1 ${⊢}\left({A}\in ℂ\wedge \frac{1}{{B}}\in ℂ\right)\to \left(-{A}\right)\left(\frac{1}{{B}}\right)=-{A}\left(\frac{1}{{B}}\right)$
3 1 2 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(-{A}\right)\left(\frac{1}{{B}}\right)=-{A}\left(\frac{1}{{B}}\right)$
4 3 3impb ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(-{A}\right)\left(\frac{1}{{B}}\right)=-{A}\left(\frac{1}{{B}}\right)$
5 negcl ${⊢}{A}\in ℂ\to -{A}\in ℂ$
6 divrec ${⊢}\left(-{A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-{A}}{{B}}=\left(-{A}\right)\left(\frac{1}{{B}}\right)$
7 5 6 syl3an1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-{A}}{{B}}=\left(-{A}\right)\left(\frac{1}{{B}}\right)$
8 divrec ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}={A}\left(\frac{1}{{B}}\right)$
9 8 negeqd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{A}}{{B}}=-{A}\left(\frac{1}{{B}}\right)$
10 4 7 9 3eqtr4rd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{A}}{{B}}=\frac{-{A}}{{B}}$