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 ) โ ( - ๐ด / - ๐ต ) = ( ๐ด / ๐ต ) ) |