Step | Hyp | Ref
| Expression |
1 | | nnmulcl 12241 |
. . 3
โข (((๐ต / ๐ด) โ โ โง (๐ถ / ๐ต) โ โ) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) โ โ) |
2 | | nncn 12225 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
3 | 2 | 3ad2ant2 1133 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
4 | | simp3 1137 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
5 | | nncn 12225 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
6 | | nnne0 12251 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ 0) |
7 | 5, 6 | jca 511 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด โ โ โง ๐ด โ 0)) |
8 | 7 | 3ad2ant1 1132 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โ โ โง ๐ด โ 0)) |
9 | | nnne0 12251 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ 0) |
10 | 2, 9 | jca 511 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต โ โ โง ๐ต โ 0)) |
11 | 10 | 3ad2ant2 1133 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต โ โ โง ๐ต โ 0)) |
12 | | divmul24 11923 |
. . . . . 6
โข (((๐ต โ โ โง ๐ถ โ โ) โง ((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0))) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) = ((๐ต / ๐ต) ยท (๐ถ / ๐ด))) |
13 | 3, 4, 8, 11, 12 | syl22anc 836 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) = ((๐ต / ๐ต) ยท (๐ถ / ๐ด))) |
14 | 2, 9 | dividd 11993 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต / ๐ต) = 1) |
15 | 14 | oveq1d 7427 |
. . . . . 6
โข (๐ต โ โ โ ((๐ต / ๐ต) ยท (๐ถ / ๐ด)) = (1 ยท (๐ถ / ๐ด))) |
16 | 15 | 3ad2ant2 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต / ๐ต) ยท (๐ถ / ๐ด)) = (1 ยท (๐ถ / ๐ด))) |
17 | | divcl 11883 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ด โ 0) โ (๐ถ / ๐ด) โ โ) |
18 | 17 | 3expb 1119 |
. . . . . . . . 9
โข ((๐ถ โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ด) โ โ) |
19 | 7, 18 | sylan2 592 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ด โ โ) โ (๐ถ / ๐ด) โ โ) |
20 | 19 | ancoms 458 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ถ / ๐ด) โ โ) |
21 | 20 | mullidd 11237 |
. . . . . 6
โข ((๐ด โ โ โง ๐ถ โ โ) โ (1
ยท (๐ถ / ๐ด)) = (๐ถ / ๐ด)) |
22 | 21 | 3adant2 1130 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (1
ยท (๐ถ / ๐ด)) = (๐ถ / ๐ด)) |
23 | 13, 16, 22 | 3eqtrd 2775 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต / ๐ด) ยท (๐ถ / ๐ต)) = (๐ถ / ๐ด)) |
24 | 23 | eleq1d 2817 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ต / ๐ด) ยท (๐ถ / ๐ต)) โ โ โ (๐ถ / ๐ด) โ โ)) |
25 | 1, 24 | imbitrid 243 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ต / ๐ด) โ โ โง (๐ถ / ๐ต) โ โ) โ (๐ถ / ๐ด) โ โ)) |
26 | 25 | imp 406 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ((๐ต / ๐ด) โ โ โง (๐ถ / ๐ต) โ โ)) โ (๐ถ / ๐ด) โ โ) |