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}$$