Step | Hyp | Ref
| Expression |
1 | | nnmulcl 8940 |
. . 3
โข (((๐ต / ๐ด) โ โ โง (๐ถ / ๐ต) โ โ) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) โ โ) |
2 | | nncn 8927 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
3 | 2 | 3ad2ant2 1019 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
4 | | simp3 999 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
5 | | nncn 8927 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
6 | | nnap0 8948 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด # 0) |
7 | 5, 6 | jca 306 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด โ โ โง ๐ด # 0)) |
8 | 7 | 3ad2ant1 1018 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โ โ โง ๐ด # 0)) |
9 | | nnap0 8948 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต # 0) |
10 | 2, 9 | jca 306 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต โ โ โง ๐ต # 0)) |
11 | 10 | 3ad2ant2 1019 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต โ โ โง ๐ต # 0)) |
12 | | divmul24ap 8673 |
. . . . . 6
โข (((๐ต โ โ โง ๐ถ โ โ) โง ((๐ด โ โ โง ๐ด # 0) โง (๐ต โ โ โง ๐ต # 0))) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) = ((๐ต / ๐ต) ยท (๐ถ / ๐ด))) |
13 | 3, 4, 8, 11, 12 | syl22anc 1239 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) = ((๐ต / ๐ต) ยท (๐ถ / ๐ด))) |
14 | 2, 9 | dividapd 8743 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต / ๐ต) = 1) |
15 | 14 | oveq1d 5890 |
. . . . . 6
โข (๐ต โ โ โ ((๐ต / ๐ต) ยท (๐ถ / ๐ด)) = (1 ยท (๐ถ / ๐ด))) |
16 | 15 | 3ad2ant2 1019 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต / ๐ต) ยท (๐ถ / ๐ด)) = (1 ยท (๐ถ / ๐ด))) |
17 | | divclap 8635 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ด # 0) โ (๐ถ / ๐ด) โ โ) |
18 | 17 | 3expb 1204 |
. . . . . . . . 9
โข ((๐ถ โ โ โง (๐ด โ โ โง ๐ด # 0)) โ (๐ถ / ๐ด) โ โ) |
19 | 7, 18 | sylan2 286 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ด โ โ) โ (๐ถ / ๐ด) โ โ) |
20 | 19 | ancoms 268 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ถ / ๐ด) โ โ) |
21 | 20 | mulid2d 7976 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (1
ยท (๐ถ / ๐ด)) = (๐ถ / ๐ด)) |
22 | 21 | 3adant2 1016 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (1
ยท (๐ถ / ๐ด)) = (๐ถ / ๐ด)) |
23 | 13, 16, 22 | 3eqtrd 2214 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) = (๐ถ / ๐ด)) |
24 | 23 | eleq1d 2246 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ต / ๐ด) ยท (๐ถ / ๐ต)) โ โ โ (๐ถ / ๐ด) โ โ)) |
25 | 1, 24 | imbitrid 154 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ต / ๐ด) โ โ โง (๐ถ / ๐ต) โ โ) โ (๐ถ / ๐ด) โ โ)) |
26 | 25 | imp 124 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ต / ๐ด) โ โ โง (๐ถ / ๐ต) โ โ)) โ (๐ถ / ๐ด) โ โ) |