Step | Hyp | Ref
| Expression |
1 | | negcl 11406 |
. . . 4
โข (๐ต โ โ โ -๐ต โ
โ) |
2 | | divadddiv 11875 |
. . . 4
โข (((๐ด โ โ โง -๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) + (-๐ต / ๐ท)) = (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |
3 | 1, 2 | sylanl2 680 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) + (-๐ต / ๐ท)) = (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |
4 | | simplr 768 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ต โ
โ) |
5 | | simprrl 780 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ท โ
โ) |
6 | | simprrr 781 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ท โ 0) |
7 | | divneg 11852 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท โ 0) โ -(๐ต / ๐ท) = (-๐ต / ๐ท)) |
8 | 4, 5, 6, 7 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ -(๐ต / ๐ท) = (-๐ต / ๐ท)) |
9 | 8 | oveq2d 7374 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) + -(๐ต / ๐ท)) = ((๐ด / ๐ถ) + (-๐ต / ๐ท))) |
10 | | simpll 766 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ด โ
โ) |
11 | | simprll 778 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ถ โ
โ) |
12 | | simprlr 779 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ถ โ 0) |
13 | | divcl 11824 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ โ 0) โ (๐ด / ๐ถ) โ โ) |
14 | 10, 11, 12, 13 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ด / ๐ถ) โ โ) |
15 | | divcl 11824 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท โ 0) โ (๐ต / ๐ท) โ โ) |
16 | 4, 5, 6, 15 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ต / ๐ท) โ โ) |
17 | 14, 16 | negsubd 11523 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) + -(๐ต / ๐ท)) = ((๐ด / ๐ถ) โ (๐ต / ๐ท))) |
18 | 9, 17 | eqtr3d 2775 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) + (-๐ต / ๐ท)) = ((๐ด / ๐ถ) โ (๐ต / ๐ท))) |
19 | 3, 18 | eqtr3d 2775 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท)) = ((๐ด / ๐ถ) โ (๐ต / ๐ท))) |
20 | 4, 11 | mulneg1d 11613 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (-๐ต ยท ๐ถ) = -(๐ต ยท ๐ถ)) |
21 | 20 | oveq2d 7374 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) + -(๐ต ยท ๐ถ))) |
22 | 10, 5 | mulcld 11180 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ด ยท ๐ท) โ โ) |
23 | 4, 11 | mulcld 11180 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ต ยท ๐ถ) โ โ) |
24 | 22, 23 | negsubd 11523 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด ยท ๐ท) + -(๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))) |
25 | 21, 24 | eqtrd 2773 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))) |
26 | 25 | oveq1d 7373 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท)) = (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |
27 | 19, 26 | eqtr3d 2775 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ถ) โ (๐ต / ๐ท)) = (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |