Step | Hyp | Ref
| Expression |
1 | | eldif 3138 |
. . 3
โข (๐ด โ (โ โ
โ) โ (๐ด โ
โ โง ยฌ ๐ด
โ โ)) |
2 | | qre 9624 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
3 | | remulcl 7938 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
4 | 2, 3 | sylan2 286 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
5 | 4 | ad2ant2r 509 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐ด โ โ) โง
(๐ต โ โ โง
๐ต โ 0)) โ (๐ด ยท ๐ต) โ โ) |
6 | | qdivcl 9642 |
. . . . . . . . . . . . 13
โข (((๐ด ยท ๐ต) โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ด ยท ๐ต) / ๐ต) โ โ) |
7 | 6 | 3expb 1204 |
. . . . . . . . . . . 12
โข (((๐ด ยท ๐ต) โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) / ๐ต) โ โ) |
8 | 7 | expcom 116 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง ๐ต โ 0) โ ((๐ด ยท ๐ต) โ โ โ ((๐ด ยท ๐ต) / ๐ต) โ โ)) |
9 | 8 | adantl 277 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) โ โ โ ((๐ด ยท ๐ต) / ๐ต) โ โ)) |
10 | | recn 7943 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ ๐ด โ
โ) |
11 | 10 | 3ad2ant1 1018 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ๐ด โ
โ) |
12 | | qcn 9633 |
. . . . . . . . . . . . . 14
โข (๐ต โ โ โ ๐ต โ
โ) |
13 | 12 | 3ad2ant2 1019 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ๐ต โ
โ) |
14 | | simp3 999 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ๐ต โ 0) |
15 | | 0z 9263 |
. . . . . . . . . . . . . . . . 17
โข 0 โ
โค |
16 | | zq 9625 |
. . . . . . . . . . . . . . . . 17
โข (0 โ
โค โ 0 โ โ) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข 0 โ
โ |
18 | | qapne 9638 |
. . . . . . . . . . . . . . . 16
โข ((๐ต โ โ โง 0 โ
โ) โ (๐ต # 0
โ ๐ต โ
0)) |
19 | 17, 18 | mpan2 425 |
. . . . . . . . . . . . . . 15
โข (๐ต โ โ โ (๐ต # 0 โ ๐ต โ 0)) |
20 | 19 | 3ad2ant2 1019 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ต # 0 โ ๐ต โ 0)) |
21 | 14, 20 | mpbird 167 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ๐ต # 0) |
22 | 11, 13, 21 | divcanap4d 8752 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ด ยท ๐ต) / ๐ต) = ๐ด) |
23 | 22 | 3expb 1204 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) / ๐ต) = ๐ด) |
24 | 23 | eleq1d 2246 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ด ยท ๐ต) / ๐ต) โ โ โ ๐ด โ โ)) |
25 | 9, 24 | sylibd 149 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) โ โ โ ๐ด โ โ)) |
26 | 25 | con3d 631 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (ยฌ ๐ด โ โ โ ยฌ
(๐ด ยท ๐ต) โ
โ)) |
27 | 26 | ex 115 |
. . . . . . 7
โข (๐ด โ โ โ ((๐ต โ โ โง ๐ต โ 0) โ (ยฌ ๐ด โ โ โ ยฌ
(๐ด ยท ๐ต) โ
โ))) |
28 | 27 | com23 78 |
. . . . . 6
โข (๐ด โ โ โ (ยฌ
๐ด โ โ โ
((๐ต โ โ โง
๐ต โ 0) โ ยฌ
(๐ด ยท ๐ต) โ
โ))) |
29 | 28 | imp31 256 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐ด โ โ) โง
(๐ต โ โ โง
๐ต โ 0)) โ ยฌ
(๐ด ยท ๐ต) โ
โ) |
30 | 5, 29 | jca 306 |
. . . 4
โข (((๐ด โ โ โง ยฌ
๐ด โ โ) โง
(๐ต โ โ โง
๐ต โ 0)) โ ((๐ด ยท ๐ต) โ โ โง ยฌ (๐ด ยท ๐ต) โ โ)) |
31 | 30 | 3impb 1199 |
. . 3
โข (((๐ด โ โ โง ยฌ
๐ด โ โ) โง
๐ต โ โ โง
๐ต โ 0) โ ((๐ด ยท ๐ต) โ โ โง ยฌ (๐ด ยท ๐ต) โ โ)) |
32 | 1, 31 | syl3an1b 1274 |
. 2
โข ((๐ด โ (โ โ
โ) โง ๐ต โ
โ โง ๐ต โ 0)
โ ((๐ด ยท ๐ต) โ โ โง ยฌ
(๐ด ยท ๐ต) โ
โ)) |
33 | | eldif 3138 |
. 2
โข ((๐ด ยท ๐ต) โ (โ โ โ) โ
((๐ด ยท ๐ต) โ โ โง ยฌ
(๐ด ยท ๐ต) โ
โ)) |
34 | 32, 33 | sylibr 134 |
1
โข ((๐ด โ (โ โ
โ) โง ๐ต โ
โ โง ๐ต โ 0)
โ (๐ด ยท ๐ต) โ (โ โ
โ)) |