Step | Hyp | Ref
| Expression |
1 | | negcl 8170 |
. . . 4
โข (๐ต โ โ โ -๐ต โ
โ) |
2 | | divadddivap 8697 |
. . . 4
โข (((๐ด โ โ โง -๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) + (-๐ต / ๐ท)) = (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |
3 | 1, 2 | sylanl2 403 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) + (-๐ต / ๐ท)) = (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |
4 | | simplr 528 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ๐ต โ โ) |
5 | | simprrl 539 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ๐ท โ โ) |
6 | | simprrr 540 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ๐ท # 0) |
7 | | divnegap 8676 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ -(๐ต / ๐ท) = (-๐ต / ๐ท)) |
8 | 4, 5, 6, 7 | syl3anc 1248 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ -(๐ต / ๐ท) = (-๐ต / ๐ท)) |
9 | 8 | oveq2d 5904 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) + -(๐ต / ๐ท)) = ((๐ด / ๐ถ) + (-๐ต / ๐ท))) |
10 | | simpll 527 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ๐ด โ โ) |
11 | | simprll 537 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ๐ถ โ โ) |
12 | | simprlr 538 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ๐ถ # 0) |
13 | | divclap 8648 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ โง ๐ถ # 0) โ (๐ด / ๐ถ) โ โ) |
14 | 10, 11, 12, 13 | syl3anc 1248 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (๐ด / ๐ถ) โ โ) |
15 | | divclap 8648 |
. . . . . 6
โข ((๐ต โ โ โง ๐ท โ โ โง ๐ท # 0) โ (๐ต / ๐ท) โ โ) |
16 | 4, 5, 6, 15 | syl3anc 1248 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (๐ต / ๐ท) โ โ) |
17 | 14, 16 | negsubd 8287 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) + -(๐ต / ๐ท)) = ((๐ด / ๐ถ) โ (๐ต / ๐ท))) |
18 | 9, 17 | eqtr3d 2222 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) + (-๐ต / ๐ท)) = ((๐ด / ๐ถ) โ (๐ต / ๐ท))) |
19 | 3, 18 | eqtr3d 2222 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท)) = ((๐ด / ๐ถ) โ (๐ต / ๐ท))) |
20 | 4, 11 | mulneg1d 8381 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (-๐ต ยท ๐ถ) = -(๐ต ยท ๐ถ)) |
21 | 20 | oveq2d 5904 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) + -(๐ต ยท ๐ถ))) |
22 | 10, 5 | mulcld 7991 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (๐ด ยท ๐ท) โ โ) |
23 | 4, 11 | mulcld 7991 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (๐ต ยท ๐ถ) โ โ) |
24 | 22, 23 | negsubd 8287 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด ยท ๐ท) + -(๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))) |
25 | 21, 24 | eqtrd 2220 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) = ((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ))) |
26 | 25 | oveq1d 5903 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ (((๐ด ยท ๐ท) + (-๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท)) = (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |
27 | 19, 26 | eqtr3d 2222 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง ((๐ถ โ โ โง ๐ถ # 0) โง (๐ท โ โ โง ๐ท # 0))) โ ((๐ด / ๐ถ) โ (๐ต / ๐ท)) = (((๐ด ยท ๐ท) โ (๐ต ยท ๐ถ)) / (๐ถ ยท ๐ท))) |