Step | Hyp | Ref
| Expression |
1 | | simpllr 534 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ ๐ต โ โ) |
2 | 1 | renegcld 8339 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ -๐ต โ โ) |
3 | | simplll 533 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ ๐ด โ โ) |
4 | 3 | renegcld 8339 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ -๐ด โ โ) |
5 | | simplr 528 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ ๐ต โ โ) |
6 | 5 | lt0neg1d 8474 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (๐ต < 0 โ 0 < -๐ต)) |
7 | 6 | biimpa 296 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ 0 < -๐ต) |
8 | | simprr 531 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 < (๐ด ยท ๐ต)) |
9 | | simpll 527 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ ๐ด โ โ) |
10 | 9 | recnd 7988 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ ๐ด โ โ) |
11 | 5 | recnd 7988 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ ๐ต โ โ) |
12 | 10, 11 | mul2negd 8372 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (-๐ด ยท -๐ต) = (๐ด ยท ๐ต)) |
13 | 8, 12 | breqtrrd 4033 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 < (-๐ด ยท -๐ต)) |
14 | 10 | negcld 8257 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ -๐ด โ โ) |
15 | 11 | negcld 8257 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ -๐ต โ โ) |
16 | 14, 15 | mulcomd 7981 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (-๐ด ยท -๐ต) = (-๐ต ยท -๐ด)) |
17 | 13, 16 | breqtrd 4031 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 < (-๐ต ยท -๐ด)) |
18 | 17 | adantr 276 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ 0 < (-๐ต ยท -๐ด)) |
19 | | prodgt0gt0 8810 |
. . . . . 6
โข (((-๐ต โ โ โง -๐ด โ โ) โง (0 <
-๐ต โง 0 < (-๐ต ยท -๐ด))) โ 0 < -๐ด) |
20 | 2, 4, 7, 18, 19 | syl22anc 1239 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ 0 < -๐ด) |
21 | 3 | lt0neg1d 8474 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ (๐ด < 0 โ 0 < -๐ด)) |
22 | 20, 21 | mpbird 167 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ ๐ด < 0) |
23 | | simplrl 535 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ 0 โค ๐ด) |
24 | | 0red 7960 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ 0 โ
โ) |
25 | 24, 3 | lenltd 8077 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ (0 โค ๐ด โ ยฌ ๐ด < 0)) |
26 | 23, 25 | mpbid 147 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โง ๐ต < 0) โ ยฌ ๐ด < 0) |
27 | 22, 26 | pm2.65da 661 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ ยฌ ๐ต < 0) |
28 | | 0red 7960 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 โ
โ) |
29 | 28, 5 | lenltd 8077 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (0 โค ๐ต โ ยฌ ๐ต < 0)) |
30 | 27, 29 | mpbird 167 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 โค ๐ต) |
31 | 9, 5 | remulcld 7990 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (๐ด ยท ๐ต) โ โ) |
32 | 31, 8 | gt0ap0d 8588 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (๐ด ยท ๐ต) # 0) |
33 | 10, 11, 32 | mulap0bbd 8619 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ ๐ต # 0) |
34 | | 0cnd 7952 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 โ
โ) |
35 | | apsym 8565 |
. . . 4
โข ((๐ต โ โ โง 0 โ
โ) โ (๐ต # 0
โ 0 # ๐ต)) |
36 | 11, 34, 35 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (๐ต # 0 โ 0 # ๐ต)) |
37 | 33, 36 | mpbid 147 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 # ๐ต) |
38 | | ltleap 8591 |
. . 3
โข ((0
โ โ โง ๐ต
โ โ) โ (0 < ๐ต โ (0 โค ๐ต โง 0 # ๐ต))) |
39 | 28, 5, 38 | syl2anc 411 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ (0 < ๐ต โ (0 โค ๐ต โง 0 # ๐ต))) |
40 | 30, 37, 39 | mpbir2and 944 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 < (๐ด ยท ๐ต))) โ 0 < ๐ต) |