Theorem divneg

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

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

Proof

Step	Hyp	Ref	Expression
1		reccl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ ℂ )
2		mulneg1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 / 𝐵 ) ∈ ℂ ) → ( - 𝐴 · ( 1 / 𝐵 ) ) = - ( 𝐴 · ( 1 / 𝐵 ) ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( - 𝐴 · ( 1 / 𝐵 ) ) = - ( 𝐴 · ( 1 / 𝐵 ) ) )
4	3	3impb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( - 𝐴 · ( 1 / 𝐵 ) ) = - ( 𝐴 · ( 1 / 𝐵 ) ) )
5		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
6		divrec	⊢ ( ( - 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( - 𝐴 / 𝐵 ) = ( - 𝐴 · ( 1 / 𝐵 ) ) )
7	5 6	syl3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( - 𝐴 / 𝐵 ) = ( - 𝐴 · ( 1 / 𝐵 ) ) )
8		divrec	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
9	8	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → - ( 𝐴 / 𝐵 ) = - ( 𝐴 · ( 1 / 𝐵 ) ) )
10	4 7 9	3eqtr4rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → - ( 𝐴 / 𝐵 ) = ( - 𝐴 / 𝐵 ) )