Metamath Proof Explorer

Theorem divneg

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

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

Proof

Step Hyp Ref Expression
1 reccl ⊢ B ∈ ℂ ∧ B ≠ 0 → 1 B ∈ ℂ
2 mulneg1 ⊢ A ∈ ℂ ∧ 1 B ∈ ℂ → − A ⁢ 1 B = − A ⁢ 1 B
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A ⁢ 1 B = − A ⁢ 1 B
4 3 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A ⁢ 1 B = − A ⁢ 1 B
5 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
6 divrec ⊢ − A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = − A ⁢ 1 B
7 5 6 syl3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = − A ⁢ 1 B
8 divrec ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B
9 8 negeqd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = − A ⁢ 1 B
10 4 7 9 3eqtr4rd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A B = − A B