Theorem divneg2

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

	Ref	Expression
Assertion	divneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → - ( 𝐴 / 𝐵 ) = ( 𝐴 / - 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		divneg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → - ( 𝐴 / 𝐵 ) = ( - 𝐴 / 𝐵 ) )
2		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
3		div2neg	⊢ ( ( - 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( - - 𝐴 / - 𝐵 ) = ( - 𝐴 / 𝐵 ) )
4	2 3	syl3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( - - 𝐴 / - 𝐵 ) = ( - 𝐴 / 𝐵 ) )
5		negneg	⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → - - 𝐴 = 𝐴 )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( - - 𝐴 / - 𝐵 ) = ( 𝐴 / - 𝐵 ) )
8	1 4 7	3eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → - ( 𝐴 / 𝐵 ) = ( 𝐴 / - 𝐵 ) )