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=AB

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⁢AB=A⁢−BB
7 2 3 4 5 6 syl112anc ⊢A∈ℂ∧B∈ℂ∧B≠0→−B⁢AB=A⁢−BB
8 divneg ⊢B∈ℂ∧B∈ℂ∧B≠0→−BB=−BB
9 4 8 syld3an1 ⊢A∈ℂ∧B∈ℂ∧B≠0→−BB=−BB
10 divid ⊢B∈ℂ∧B≠0→BB=1
11 10 3adant1 ⊢A∈ℂ∧B∈ℂ∧B≠0→BB=1
12 11 negeqd ⊢A∈ℂ∧B∈ℂ∧B≠0→−BB=−1
13 9 12 eqtr3d ⊢A∈ℂ∧B∈ℂ∧B≠0→−BB=−1
14 13 oveq2d ⊢A∈ℂ∧B∈ℂ∧B≠0→A⁢−BB=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⁢−BB=−A
23 7 22 eqtrd ⊢A∈ℂ∧B∈ℂ∧B≠0→−B⁢AB=−A
24 negcl ⊢A∈ℂ→−A∈ℂ
25 24 3ad2ant1 ⊢A∈ℂ∧B∈ℂ∧B≠0→−A∈ℂ
26 divcl ⊢A∈ℂ∧B∈ℂ∧B≠0→AB∈ℂ
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∈ℂ∧AB∈ℂ∧−B∈ℂ∧−B≠0→−A−B=AB↔−B⁢AB=−A
32 25 26 2 30 31 syl112anc ⊢A∈ℂ∧B∈ℂ∧B≠0→−A−B=AB↔−B⁢AB=−A
33 23 32 mpbird ⊢A∈ℂ∧B∈ℂ∧B≠0→−A−B=AB