Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ โ) |
2 | 1 | recnd 11242 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ โ) |
3 | | gt0ne0 11679 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ 0) |
4 | 2, 3 | recne0d 11984 |
. . . . 5
โข ((๐ด โ โ โง 0 <
๐ด) โ (1 / ๐ด) โ 0) |
5 | 4 | necomd 2997 |
. . . 4
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 โ (1 / ๐ด)) |
6 | 5 | neneqd 2946 |
. . 3
โข ((๐ด โ โ โง 0 <
๐ด) โ ยฌ 0 = (1 /
๐ด)) |
7 | | 0lt1 11736 |
. . . . 5
โข 0 <
1 |
8 | | 0re 11216 |
. . . . . 6
โข 0 โ
โ |
9 | | 1re 11214 |
. . . . . 6
โข 1 โ
โ |
10 | 8, 9 | ltnsymi 11333 |
. . . . 5
โข (0 < 1
โ ยฌ 1 < 0) |
11 | 7, 10 | ax-mp 5 |
. . . 4
โข ยฌ 1
< 0 |
12 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ ๐ด โ
โ) |
13 | 3 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ ๐ด โ 0) |
14 | 12, 13 | rereccld 12041 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (1 / ๐ด) โ
โ) |
15 | 14 | renegcld 11641 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ -(1 / ๐ด) โ
โ) |
16 | | simpr 486 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (1 / ๐ด) < 0) |
17 | 1, 3 | rereccld 12041 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง 0 <
๐ด) โ (1 / ๐ด) โ
โ) |
18 | 17 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (1 / ๐ด) โ
โ) |
19 | 18 | lt0neg1d 11783 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ ((1 / ๐ด) < 0 โ 0 < -(1 /
๐ด))) |
20 | 16, 19 | mpbid 231 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ 0 < -(1 /
๐ด)) |
21 | | simplr 768 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ 0 < ๐ด) |
22 | 15, 12, 20, 21 | mulgt0d 11369 |
. . . . . . 7
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ 0 < (-(1 /
๐ด) ยท ๐ด)) |
23 | 2 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ ๐ด โ
โ) |
24 | 23, 13 | reccld 11983 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (1 / ๐ด) โ
โ) |
25 | 24, 23 | mulneg1d 11667 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (-(1 / ๐ด) ยท ๐ด) = -((1 / ๐ด) ยท ๐ด)) |
26 | 23, 13 | recid2d 11986 |
. . . . . . . . 9
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ ((1 / ๐ด) ยท ๐ด) = 1) |
27 | 26 | negeqd 11454 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ -((1 / ๐ด) ยท ๐ด) = -1) |
28 | 25, 27 | eqtrd 2773 |
. . . . . . 7
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (-(1 / ๐ด) ยท ๐ด) = -1) |
29 | 22, 28 | breqtrd 5175 |
. . . . . 6
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ 0 <
-1) |
30 | | 1red 11215 |
. . . . . . 7
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ 1 โ
โ) |
31 | 30 | lt0neg1d 11783 |
. . . . . 6
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ (1 < 0
โ 0 < -1)) |
32 | 29, 31 | mpbird 257 |
. . . . 5
โข (((๐ด โ โ โง 0 <
๐ด) โง (1 / ๐ด) < 0) โ 1 <
0) |
33 | 32 | ex 414 |
. . . 4
โข ((๐ด โ โ โง 0 <
๐ด) โ ((1 / ๐ด) < 0 โ 1 <
0)) |
34 | 11, 33 | mtoi 198 |
. . 3
โข ((๐ด โ โ โง 0 <
๐ด) โ ยฌ (1 / ๐ด) < 0) |
35 | | ioran 983 |
. . 3
โข (ยฌ (0
= (1 / ๐ด) โจ (1 / ๐ด) < 0) โ (ยฌ 0 = (1 /
๐ด) โง ยฌ (1 / ๐ด) < 0)) |
36 | 6, 34, 35 | sylanbrc 584 |
. 2
โข ((๐ด โ โ โง 0 <
๐ด) โ ยฌ (0 = (1 /
๐ด) โจ (1 / ๐ด) < 0)) |
37 | | axlttri 11285 |
. . 3
โข ((0
โ โ โง (1 / ๐ด) โ โ) โ (0 < (1 / ๐ด) โ ยฌ (0 = (1 / ๐ด) โจ (1 / ๐ด) < 0))) |
38 | 8, 17, 37 | sylancr 588 |
. 2
โข ((๐ด โ โ โง 0 <
๐ด) โ (0 < (1 /
๐ด) โ ยฌ (0 = (1 /
๐ด) โจ (1 / ๐ด) < 0))) |
39 | 36, 38 | mpbird 257 |
1
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 < (1 / ๐ด)) |