Step | Hyp | Ref
| Expression |
1 | | remulcl 7938 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
2 | 1 | ad2ant2r 509 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
3 | | 0re 7956 |
. . . 4
โข 0 โ
โ |
4 | | ltnsym2 8047 |
. . . 4
โข (((๐ด ยท ๐ต) โ โ โง 0 โ โ)
โ ยฌ ((๐ด ยท
๐ต) < 0 โง 0 <
(๐ด ยท ๐ต))) |
5 | 2, 3, 4 | sylancl 413 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ยฌ ((๐ด ยท ๐ต) < 0 โง 0 < (๐ด ยท ๐ต))) |
6 | | orc 712 |
. . . . . 6
โข ((๐ด ยท ๐ต) < 0 โ ((๐ด ยท ๐ต) < 0 โจ 0 < (๐ด ยท ๐ต))) |
7 | | reaplt 8544 |
. . . . . . 7
โข (((๐ด ยท ๐ต) โ โ โง 0 โ โ)
โ ((๐ด ยท ๐ต) # 0 โ ((๐ด ยท ๐ต) < 0 โจ 0 < (๐ด ยท ๐ต)))) |
8 | 2, 3, 7 | sylancl 413 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ต) # 0 โ ((๐ด ยท ๐ต) < 0 โจ 0 < (๐ด ยท ๐ต)))) |
9 | 6, 8 | imbitrrid 156 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ต) < 0 โ (๐ด ยท ๐ต) # 0)) |
10 | | simplll 533 |
. . . . . . 7
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ ๐ด โ โ) |
11 | | simplrl 535 |
. . . . . . 7
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ ๐ต โ โ) |
12 | | recn 7943 |
. . . . . . . . . . . . . 14
โข (๐ต โ โ โ ๐ต โ
โ) |
13 | | recn 7943 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ ๐ด โ
โ) |
14 | | mulap0r 8571 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด ยท ๐ต) # 0) โ (๐ด # 0 โง ๐ต # 0)) |
15 | 13, 14 | syl3an1 1271 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด ยท ๐ต) # 0) โ (๐ด # 0 โง ๐ต # 0)) |
16 | 12, 15 | syl3an2 1272 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด ยท ๐ต) # 0) โ (๐ด # 0 โง ๐ต # 0)) |
17 | 16 | 3expia 1205 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) # 0 โ (๐ด # 0 โง ๐ต # 0))) |
18 | 17 | ad2ant2r 509 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ต) # 0 โ (๐ด # 0 โง ๐ต # 0))) |
19 | 18 | imp 124 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (๐ด # 0 โง ๐ต # 0)) |
20 | 19 | simpld 112 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ ๐ด # 0) |
21 | | reaplt 8544 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 โ
โ) โ (๐ด # 0
โ (๐ด < 0 โจ 0
< ๐ด))) |
22 | 3, 21 | mpan2 425 |
. . . . . . . . . 10
โข (๐ด โ โ โ (๐ด # 0 โ (๐ด < 0 โจ 0 < ๐ด))) |
23 | 22 | ad3antrrr 492 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (๐ด # 0 โ (๐ด < 0 โจ 0 < ๐ด))) |
24 | 20, 23 | mpbid 147 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (๐ด < 0 โจ 0 < ๐ด)) |
25 | | lenlt 8032 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐ด
โ โ) โ (0 โค ๐ด โ ยฌ ๐ด < 0)) |
26 | 3, 25 | mpan 424 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (0 โค
๐ด โ ยฌ ๐ด < 0)) |
27 | 26 | biimpa 296 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 โค
๐ด) โ ยฌ ๐ด < 0) |
28 | 27 | ad2antrr 488 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ ยฌ ๐ด < 0) |
29 | | biorf 744 |
. . . . . . . . 9
โข (ยฌ
๐ด < 0 โ (0 <
๐ด โ (๐ด < 0 โจ 0 < ๐ด))) |
30 | 28, 29 | syl 14 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (0 < ๐ด โ (๐ด < 0 โจ 0 < ๐ด))) |
31 | 24, 30 | mpbird 167 |
. . . . . . 7
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ 0 < ๐ด) |
32 | 19 | simprd 114 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ ๐ต # 0) |
33 | | reaplt 8544 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง 0 โ
โ) โ (๐ต # 0
โ (๐ต < 0 โจ 0
< ๐ต))) |
34 | 3, 33 | mpan2 425 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (๐ต # 0 โ (๐ต < 0 โจ 0 < ๐ต))) |
35 | 34 | ad2antrl 490 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต # 0 โ (๐ต < 0 โจ 0 < ๐ต))) |
36 | 35 | adantr 276 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (๐ต # 0 โ (๐ต < 0 โจ 0 < ๐ต))) |
37 | 32, 36 | mpbid 147 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (๐ต < 0 โจ 0 < ๐ต)) |
38 | | lenlt 8032 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐ต
โ โ) โ (0 โค ๐ต โ ยฌ ๐ต < 0)) |
39 | 3, 38 | mpan 424 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (0 โค
๐ต โ ยฌ ๐ต < 0)) |
40 | 39 | biimpa 296 |
. . . . . . . . . 10
โข ((๐ต โ โ โง 0 โค
๐ต) โ ยฌ ๐ต < 0) |
41 | 40 | ad2antlr 489 |
. . . . . . . . 9
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ ยฌ ๐ต < 0) |
42 | | biorf 744 |
. . . . . . . . 9
โข (ยฌ
๐ต < 0 โ (0 <
๐ต โ (๐ต < 0 โจ 0 < ๐ต))) |
43 | 41, 42 | syl 14 |
. . . . . . . 8
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ (0 < ๐ต โ (๐ต < 0 โจ 0 < ๐ต))) |
44 | 37, 43 | mpbird 167 |
. . . . . . 7
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ 0 < ๐ต) |
45 | 10, 11, 31, 44 | mulgt0d 8079 |
. . . . . 6
โข ((((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โง (๐ด ยท ๐ต) # 0) โ 0 < (๐ด ยท ๐ต)) |
46 | 45 | ex 115 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ต) # 0 โ 0 < (๐ด ยท ๐ต))) |
47 | 9, 46 | syld 45 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ต) < 0 โ 0 < (๐ด ยท ๐ต))) |
48 | 47 | ancld 325 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ต) < 0 โ ((๐ด ยท ๐ต) < 0 โง 0 < (๐ด ยท ๐ต)))) |
49 | 5, 48 | mtod 663 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ยฌ (๐ด ยท ๐ต) < 0) |
50 | | lenlt 8032 |
. . 3
โข ((0
โ โ โง (๐ด
ยท ๐ต) โ โ)
โ (0 โค (๐ด ยท
๐ต) โ ยฌ (๐ด ยท ๐ต) < 0)) |
51 | 3, 2, 50 | sylancr 414 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (0 โค (๐ด ยท ๐ต) โ ยฌ (๐ด ยท ๐ต) < 0)) |
52 | 49, 51 | mpbird 167 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |