Step | Hyp | Ref
| Expression |
1 | | simprrl 780 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ท โ
โ) |
2 | | simprll 778 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ถ โ
โ) |
3 | | simprlr 779 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ถ โ 0) |
4 | | divcl 11824 |
. . . . . . 7
โข ((๐ท โ โ โง ๐ถ โ โ โง ๐ถ โ 0) โ (๐ท / ๐ถ) โ โ) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . . . . 6
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ท / ๐ถ) โ โ) |
6 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ด โ
โ) |
7 | | simplrl 776 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ต โ
โ) |
8 | | simplrr 777 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ต โ 0) |
9 | | divcl 11824 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) |
10 | 6, 7, 8, 9 | syl3anc 1372 |
. . . . . 6
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ด / ๐ต) โ โ) |
11 | 5, 10 | mulcomd 11181 |
. . . . 5
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ท / ๐ถ) ยท (๐ด / ๐ต)) = ((๐ด / ๐ต) ยท (๐ท / ๐ถ))) |
12 | | simplr 768 |
. . . . . 6
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ต โ โ โง ๐ต โ 0)) |
13 | | simprl 770 |
. . . . . 6
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ถ โ โ โง ๐ถ โ 0)) |
14 | | divmuldiv 11860 |
. . . . . 6
โข (((๐ด โ โ โง ๐ท โ โ) โง ((๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0))) โ ((๐ด / ๐ต) ยท (๐ท / ๐ถ)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) |
15 | 6, 1, 12, 13, 14 | syl22anc 838 |
. . . . 5
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ต) ยท (๐ท / ๐ถ)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) |
16 | 11, 15 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ท / ๐ถ) ยท (๐ด / ๐ต)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) |
17 | 16 | oveq2d 7374 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ / ๐ท) ยท ((๐ท / ๐ถ) ยท (๐ด / ๐ต))) = ((๐ถ / ๐ท) ยท ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)))) |
18 | | simprr 772 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ท โ โ โง ๐ท โ 0)) |
19 | | divmuldiv 11860 |
. . . . . . 7
โข (((๐ถ โ โ โง ๐ท โ โ) โง ((๐ท โ โ โง ๐ท โ 0) โง (๐ถ โ โ โง ๐ถ โ 0))) โ ((๐ถ / ๐ท) ยท (๐ท / ๐ถ)) = ((๐ถ ยท ๐ท) / (๐ท ยท ๐ถ))) |
20 | 2, 1, 18, 13, 19 | syl22anc 838 |
. . . . . 6
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ / ๐ท) ยท (๐ท / ๐ถ)) = ((๐ถ ยท ๐ท) / (๐ท ยท ๐ถ))) |
21 | 2, 1 | mulcomd 11181 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ถ ยท ๐ท) = (๐ท ยท ๐ถ)) |
22 | 21 | oveq1d 7373 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ ยท ๐ท) / (๐ท ยท ๐ถ)) = ((๐ท ยท ๐ถ) / (๐ท ยท ๐ถ))) |
23 | 1, 2 | mulcld 11180 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ท ยท ๐ถ) โ โ) |
24 | | simprrr 781 |
. . . . . . . . 9
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ๐ท โ 0) |
25 | 1, 2, 24, 3 | mulne0d 11812 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ท ยท ๐ถ) โ 0) |
26 | | divid 11847 |
. . . . . . . 8
โข (((๐ท ยท ๐ถ) โ โ โง (๐ท ยท ๐ถ) โ 0) โ ((๐ท ยท ๐ถ) / (๐ท ยท ๐ถ)) = 1) |
27 | 23, 25, 26 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ท ยท ๐ถ) / (๐ท ยท ๐ถ)) = 1) |
28 | 22, 27 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ ยท ๐ท) / (๐ท ยท ๐ถ)) = 1) |
29 | 20, 28 | eqtrd 2773 |
. . . . 5
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ / ๐ท) ยท (๐ท / ๐ถ)) = 1) |
30 | 29 | oveq1d 7373 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (((๐ถ / ๐ท) ยท (๐ท / ๐ถ)) ยท (๐ด / ๐ต)) = (1 ยท (๐ด / ๐ต))) |
31 | | divcl 11824 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ท โ โ โง ๐ท โ 0) โ (๐ถ / ๐ท) โ โ) |
32 | 2, 1, 24, 31 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ถ / ๐ท) โ โ) |
33 | 32, 5, 10 | mulassd 11183 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (((๐ถ / ๐ท) ยท (๐ท / ๐ถ)) ยท (๐ด / ๐ต)) = ((๐ถ / ๐ท) ยท ((๐ท / ๐ถ) ยท (๐ด / ๐ต)))) |
34 | 10 | mulid2d 11178 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (1 ยท
(๐ด / ๐ต)) = (๐ด / ๐ต)) |
35 | 30, 33, 34 | 3eqtr3d 2781 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ / ๐ท) ยท ((๐ท / ๐ถ) ยท (๐ด / ๐ต))) = (๐ด / ๐ต)) |
36 | 17, 35 | eqtr3d 2775 |
. 2
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ถ / ๐ท) ยท ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) = (๐ด / ๐ต)) |
37 | 6, 1 | mulcld 11180 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ด ยท ๐ท) โ โ) |
38 | 7, 2 | mulcld 11180 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ต ยท ๐ถ) โ โ) |
39 | | mulne0 11802 |
. . . . 5
โข (((๐ต โ โ โง ๐ต โ 0) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ต ยท ๐ถ) โ 0) |
40 | 39 | ad2ant2lr 747 |
. . . 4
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ต ยท ๐ถ) โ 0) |
41 | | divcl 11824 |
. . . 4
โข (((๐ด ยท ๐ท) โ โ โง (๐ต ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ 0) โ ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)) โ โ) |
42 | 37, 38, 40, 41 | syl3anc 1372 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)) โ โ) |
43 | | divne0 11830 |
. . . 4
โข (((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0)) โ (๐ถ / ๐ท) โ 0) |
44 | 43 | adantl 483 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (๐ถ / ๐ท) โ 0) |
45 | | divmul 11821 |
. . 3
โข (((๐ด / ๐ต) โ โ โง ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)) โ โ โง ((๐ถ / ๐ท) โ โ โง (๐ถ / ๐ท) โ 0)) โ (((๐ด / ๐ต) / (๐ถ / ๐ท)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)) โ ((๐ถ / ๐ท) ยท ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) = (๐ด / ๐ต))) |
46 | 10, 42, 32, 44, 45 | syl112anc 1375 |
. 2
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ (((๐ด / ๐ต) / (๐ถ / ๐ท)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ)) โ ((๐ถ / ๐ท) ยท ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) = (๐ด / ๐ต))) |
47 | 36, 46 | mpbird 257 |
1
โข (((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โง ((๐ถ โ โ โง ๐ถ โ 0) โง (๐ท โ โ โง ๐ท โ 0))) โ ((๐ด / ๐ต) / (๐ถ / ๐ท)) = ((๐ด ยท ๐ท) / (๐ต ยท ๐ถ))) |