# Metamath Proof Explorer

## Theorem divneg2

Description: Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014)

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

### Proof

Step Hyp Ref Expression
1 divneg ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{A}}{{B}}=\frac{-{A}}{{B}}$
2 negcl ${⊢}{A}\in ℂ\to -{A}\in ℂ$
3 div2neg ${⊢}\left(-{A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-\left(-{A}\right)}{-{B}}=\frac{-{A}}{{B}}$
4 2 3 syl3an1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-\left(-{A}\right)}{-{B}}=\frac{-{A}}{{B}}$
5 negneg ${⊢}{A}\in ℂ\to -\left(-{A}\right)={A}$
6 5 3ad2ant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\left(-{A}\right)={A}$
7 6 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{-\left(-{A}\right)}{-{B}}=\frac{{A}}{-{B}}$
8 1 4 7 3eqtr2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to -\frac{{A}}{{B}}=\frac{{A}}{-{B}}$