Step | Hyp | Ref
| Expression |
1 | | 0lt1 11682 |
. . 3
โข 0 <
1 |
2 | 1 | a1i 11 |
. 2
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ 0 <
1) |
3 | | simpr 486 |
. . . 4
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ ยฌ (1 /
๐ด) < 0) |
4 | | 0red 11163 |
. . . . 5
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ 0 โ
โ) |
5 | | 1red 11161 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
6 | | reclt0d.1 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
7 | | reclt0d.2 |
. . . . . . . 8
โข (๐ โ ๐ด < 0) |
8 | 7 | lt0ne0d 11725 |
. . . . . . 7
โข (๐ โ ๐ด โ 0) |
9 | 5, 6, 8 | redivcld 11988 |
. . . . . 6
โข (๐ โ (1 / ๐ด) โ โ) |
10 | 9 | adantr 482 |
. . . . 5
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ (1 / ๐ด) โ
โ) |
11 | 4, 10 | lenltd 11306 |
. . . 4
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ (0 โค (1 /
๐ด) โ ยฌ (1 / ๐ด) < 0)) |
12 | 3, 11 | mpbird 257 |
. . 3
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ 0 โค (1 /
๐ด)) |
13 | 6 | recnd 11188 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
14 | 13, 8 | recidd 11931 |
. . . . . . 7
โข (๐ โ (๐ด ยท (1 / ๐ด)) = 1) |
15 | 14 | eqcomd 2739 |
. . . . . 6
โข (๐ โ 1 = (๐ด ยท (1 / ๐ด))) |
16 | 15 | adantr 482 |
. . . . 5
โข ((๐ โง 0 โค (1 / ๐ด)) โ 1 = (๐ด ยท (1 / ๐ด))) |
17 | | 0red 11163 |
. . . . . . . . . 10
โข (๐ โ 0 โ
โ) |
18 | 6, 17, 7 | ltled 11308 |
. . . . . . . . 9
โข (๐ โ ๐ด โค 0) |
19 | 18 | adantr 482 |
. . . . . . . 8
โข ((๐ โง 0 โค (1 / ๐ด)) โ ๐ด โค 0) |
20 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง 0 โค (1 / ๐ด)) โ 0 โค (1 / ๐ด)) |
21 | 19, 20 | jca 513 |
. . . . . . 7
โข ((๐ โง 0 โค (1 / ๐ด)) โ (๐ด โค 0 โง 0 โค (1 / ๐ด))) |
22 | 21 | orcd 872 |
. . . . . 6
โข ((๐ โง 0 โค (1 / ๐ด)) โ ((๐ด โค 0 โง 0 โค (1 / ๐ด)) โจ (0 โค ๐ด โง (1 / ๐ด) โค 0))) |
23 | | mulle0b 12031 |
. . . . . . . 8
โข ((๐ด โ โ โง (1 / ๐ด) โ โ) โ ((๐ด ยท (1 / ๐ด)) โค 0 โ ((๐ด โค 0 โง 0 โค (1 / ๐ด)) โจ (0 โค ๐ด โง (1 / ๐ด) โค 0)))) |
24 | 6, 9, 23 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ด ยท (1 / ๐ด)) โค 0 โ ((๐ด โค 0 โง 0 โค (1 / ๐ด)) โจ (0 โค ๐ด โง (1 / ๐ด) โค 0)))) |
25 | 24 | adantr 482 |
. . . . . 6
โข ((๐ โง 0 โค (1 / ๐ด)) โ ((๐ด ยท (1 / ๐ด)) โค 0 โ ((๐ด โค 0 โง 0 โค (1 / ๐ด)) โจ (0 โค ๐ด โง (1 / ๐ด) โค 0)))) |
26 | 22, 25 | mpbird 257 |
. . . . 5
โข ((๐ โง 0 โค (1 / ๐ด)) โ (๐ด ยท (1 / ๐ด)) โค 0) |
27 | 16, 26 | eqbrtrd 5128 |
. . . 4
โข ((๐ โง 0 โค (1 / ๐ด)) โ 1 โค
0) |
28 | 5 | adantr 482 |
. . . . 5
โข ((๐ โง 0 โค (1 / ๐ด)) โ 1 โ
โ) |
29 | | 0red 11163 |
. . . . 5
โข ((๐ โง 0 โค (1 / ๐ด)) โ 0 โ
โ) |
30 | 28, 29 | lenltd 11306 |
. . . 4
โข ((๐ โง 0 โค (1 / ๐ด)) โ (1 โค 0 โ ยฌ
0 < 1)) |
31 | 27, 30 | mpbid 231 |
. . 3
โข ((๐ โง 0 โค (1 / ๐ด)) โ ยฌ 0 <
1) |
32 | 12, 31 | syldan 592 |
. 2
โข ((๐ โง ยฌ (1 / ๐ด) < 0) โ ยฌ 0 <
1) |
33 | 2, 32 | condan 817 |
1
โข (๐ โ (1 / ๐ด) < 0) |