Step | Hyp | Ref
| Expression |
1 | | remulcl 7941 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ โ) โ (๐ด ยท ๐ด) โ โ) |
2 | 1 | anidms 397 |
. . . 4
โข (๐ด โ โ โ (๐ด ยท ๐ด) โ โ) |
3 | | 0re 7959 |
. . . 4
โข 0 โ
โ |
4 | | ltnsym2 8050 |
. . . 4
โข (((๐ด ยท ๐ด) โ โ โง 0 โ โ)
โ ยฌ ((๐ด ยท
๐ด) < 0 โง 0 <
(๐ด ยท ๐ด))) |
5 | 2, 3, 4 | sylancl 413 |
. . 3
โข (๐ด โ โ โ ยฌ
((๐ด ยท ๐ด) < 0 โง 0 < (๐ด ยท ๐ด))) |
6 | | orc 712 |
. . . . . 6
โข ((๐ด ยท ๐ด) < 0 โ ((๐ด ยท ๐ด) < 0 โจ 0 < (๐ด ยท ๐ด))) |
7 | | reaplt 8547 |
. . . . . . 7
โข (((๐ด ยท ๐ด) โ โ โง 0 โ โ)
โ ((๐ด ยท ๐ด) # 0 โ ((๐ด ยท ๐ด) < 0 โจ 0 < (๐ด ยท ๐ด)))) |
8 | 2, 3, 7 | sylancl 413 |
. . . . . 6
โข (๐ด โ โ โ ((๐ด ยท ๐ด) # 0 โ ((๐ด ยท ๐ด) < 0 โจ 0 < (๐ด ยท ๐ด)))) |
9 | 6, 8 | imbitrrid 156 |
. . . . 5
โข (๐ด โ โ โ ((๐ด ยท ๐ด) < 0 โ (๐ด ยท ๐ด) # 0)) |
10 | | recn 7946 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
11 | | mulap0r 8574 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ด โ โ โง (๐ด ยท ๐ด) # 0) โ (๐ด # 0 โง ๐ด # 0)) |
12 | 10, 11 | syl3an1 1271 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ โ โง (๐ด ยท ๐ด) # 0) โ (๐ด # 0 โง ๐ด # 0)) |
13 | 10, 12 | syl3an2 1272 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ โ โง (๐ด ยท ๐ด) # 0) โ (๐ด # 0 โง ๐ด # 0)) |
14 | 13 | simpld 112 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ โ โง (๐ด ยท ๐ด) # 0) โ ๐ด # 0) |
15 | 14 | 3expia 1205 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ โ) โ ((๐ด ยท ๐ด) # 0 โ ๐ด # 0)) |
16 | 15 | anidms 397 |
. . . . 5
โข (๐ด โ โ โ ((๐ด ยท ๐ด) # 0 โ ๐ด # 0)) |
17 | | apsqgt0 8560 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด # 0) โ 0 < (๐ด ยท ๐ด)) |
18 | 17 | ex 115 |
. . . . 5
โข (๐ด โ โ โ (๐ด # 0 โ 0 < (๐ด ยท ๐ด))) |
19 | 9, 16, 18 | 3syld 57 |
. . . 4
โข (๐ด โ โ โ ((๐ด ยท ๐ด) < 0 โ 0 < (๐ด ยท ๐ด))) |
20 | 19 | ancld 325 |
. . 3
โข (๐ด โ โ โ ((๐ด ยท ๐ด) < 0 โ ((๐ด ยท ๐ด) < 0 โง 0 < (๐ด ยท ๐ด)))) |
21 | 5, 20 | mtod 663 |
. 2
โข (๐ด โ โ โ ยฌ
(๐ด ยท ๐ด) < 0) |
22 | | lenlt 8035 |
. . 3
โข ((0
โ โ โง (๐ด
ยท ๐ด) โ โ)
โ (0 โค (๐ด ยท
๐ด) โ ยฌ (๐ด ยท ๐ด) < 0)) |
23 | 3, 2, 22 | sylancr 414 |
. 2
โข (๐ด โ โ โ (0 โค
(๐ด ยท ๐ด) โ ยฌ (๐ด ยท ๐ด) < 0)) |
24 | 21, 23 | mpbird 167 |
1
โข (๐ด โ โ โ 0 โค
(๐ด ยท ๐ด)) |