Metamath Proof Explorer

Theorem div2neg

Description: Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 1 3ad2ant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B ∈ ℂ
3 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
4 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
5 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ≠ 0
6 div12 ⊢ − B ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B ⁢ A B = A ⁢ − B B
7 2 3 4 5 6 syl112anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B ⁢ A B = A ⁢ − B B
8 divneg ⊢ B ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B B = − B B
9 4 8 syld3an1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B B = − B B
10 divid ⊢ B ∈ ℂ ∧ B ≠ 0 → B B = 1
11 10 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B B = 1
12 11 negeqd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B B = − 1
13 9 12 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B B = − 1
14 13 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ − B B = A ⁢ -1
15 ax-1cn ⊢ 1 ∈ ℂ
16 15 negcli ⊢ − 1 ∈ ℂ
17 mulcom ⊢ A ∈ ℂ ∧ − 1 ∈ ℂ → A ⁢ -1 = -1 ⁢ A
18 16 17 mpan2 ⊢ A ∈ ℂ → A ⁢ -1 = -1 ⁢ A
19 mulm1 ⊢ A ∈ ℂ → -1 ⁢ A = − A
20 18 19 eqtrd ⊢ A ∈ ℂ → A ⁢ -1 = − A
21 20 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ -1 = − A
22 14 21 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ − B B = − A
23 7 22 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B ⁢ A B = − A
24 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
25 24 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A ∈ ℂ
26 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
27 negeq0 ⊢ B ∈ ℂ → B = 0 ↔ − B = 0
28 27 necon3bid ⊢ B ∈ ℂ → B ≠ 0 ↔ − B ≠ 0
29 28 biimpa ⊢ B ∈ ℂ ∧ B ≠ 0 → − B ≠ 0
30 29 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − B ≠ 0
31 divmul ⊢ − A ∈ ℂ ∧ A B ∈ ℂ ∧ − B ∈ ℂ ∧ − B ≠ 0 → − A − B = A B ↔ − B ⁢ A B = − A
32 25 26 2 30 31 syl112anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A − B = A B ↔ − B ⁢ A B = − A
33 23 32 mpbird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → − A − B = A B