This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divneg2

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

Ref Expression
Assertion divneg2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = A − B

Proof

Step Hyp Ref Expression
1 divneg ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = − A B
2 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
3 div2neg ⊢ − A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − − A − B = − A B
4 2 3 syl3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − − A − B = − A B
5 negneg ⊢ A ∈ ℂ → − − A = A
6 5 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − − A = A
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − − A − B = A − B
8 1 4 7 3eqtr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = A − B