Metamath Proof Explorer


Theorem div2neg

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

Ref Expression
Assertion div2neg ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( - ๐ด / - ๐ต ) = ( ๐ด / ๐ต ) )

Proof

Step Hyp Ref Expression
1 negcl โŠข ( ๐ต โˆˆ โ„‚ โ†’ - ๐ต โˆˆ โ„‚ )
2 1 3ad2ant2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ๐ต โˆˆ โ„‚ )
3 simp1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ๐ด โˆˆ โ„‚ )
4 simp2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ๐ต โˆˆ โ„‚ )
5 simp3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ๐ต โ‰  0 )
6 div12 โŠข ( ( - ๐ต โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) ) โ†’ ( - ๐ต ยท ( ๐ด / ๐ต ) ) = ( ๐ด ยท ( - ๐ต / ๐ต ) ) )
7 2 3 4 5 6 syl112anc โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( - ๐ต ยท ( ๐ด / ๐ต ) ) = ( ๐ด ยท ( - ๐ต / ๐ต ) ) )
8 divneg โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ( ๐ต / ๐ต ) = ( - ๐ต / ๐ต ) )
9 4 8 syld3an1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ( ๐ต / ๐ต ) = ( - ๐ต / ๐ต ) )
10 divid โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ๐ต / ๐ต ) = 1 )
11 10 3adant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ๐ต / ๐ต ) = 1 )
12 11 negeqd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ( ๐ต / ๐ต ) = - 1 )
13 9 12 eqtr3d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( - ๐ต / ๐ต ) = - 1 )
14 13 oveq2d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ๐ด ยท ( - ๐ต / ๐ต ) ) = ( ๐ด ยท - 1 ) )
15 ax-1cn โŠข 1 โˆˆ โ„‚
16 15 negcli โŠข - 1 โˆˆ โ„‚
17 mulcom โŠข ( ( ๐ด โˆˆ โ„‚ โˆง - 1 โˆˆ โ„‚ ) โ†’ ( ๐ด ยท - 1 ) = ( - 1 ยท ๐ด ) )
18 16 17 mpan2 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยท - 1 ) = ( - 1 ยท ๐ด ) )
19 mulm1 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( - 1 ยท ๐ด ) = - ๐ด )
20 18 19 eqtrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยท - 1 ) = - ๐ด )
21 20 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ๐ด ยท - 1 ) = - ๐ด )
22 14 21 eqtrd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ๐ด ยท ( - ๐ต / ๐ต ) ) = - ๐ด )
23 7 22 eqtrd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( - ๐ต ยท ( ๐ด / ๐ต ) ) = - ๐ด )
24 negcl โŠข ( ๐ด โˆˆ โ„‚ โ†’ - ๐ด โˆˆ โ„‚ )
25 24 3ad2ant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ๐ด โˆˆ โ„‚ )
26 divcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ๐ด / ๐ต ) โˆˆ โ„‚ )
27 negeq0 โŠข ( ๐ต โˆˆ โ„‚ โ†’ ( ๐ต = 0 โ†” - ๐ต = 0 ) )
28 27 necon3bid โŠข ( ๐ต โˆˆ โ„‚ โ†’ ( ๐ต โ‰  0 โ†” - ๐ต โ‰  0 ) )
29 28 biimpa โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ๐ต โ‰  0 )
30 29 3adant1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ - ๐ต โ‰  0 )
31 divmul โŠข ( ( - ๐ด โˆˆ โ„‚ โˆง ( ๐ด / ๐ต ) โˆˆ โ„‚ โˆง ( - ๐ต โˆˆ โ„‚ โˆง - ๐ต โ‰  0 ) ) โ†’ ( ( - ๐ด / - ๐ต ) = ( ๐ด / ๐ต ) โ†” ( - ๐ต ยท ( ๐ด / ๐ต ) ) = - ๐ด ) )
32 25 26 2 30 31 syl112anc โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( ( - ๐ด / - ๐ต ) = ( ๐ด / ๐ต ) โ†” ( - ๐ต ยท ( ๐ด / ๐ต ) ) = - ๐ด ) )
33 23 32 mpbird โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0 ) โ†’ ( - ๐ด / - ๐ต ) = ( ๐ด / ๐ต ) )