Step | Hyp | Ref
| Expression |
1 | | elunitrn 13444 |
. . . . . . . 8
โข (๐ด โ (0[,]1) โ ๐ด โ
โ) |
2 | 1 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ ๐ด โ
โ) |
3 | | elunitrn 13444 |
. . . . . . . 8
โข (๐ต โ (0[,]1) โ ๐ต โ
โ) |
4 | 3 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ ๐ต โ
โ) |
5 | | simp3 1139 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ ๐ต โ 0) |
6 | 2, 4, 5 | redivcld 12042 |
. . . . . 6
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) |
7 | 6 | adantr 482 |
. . . . 5
โข (((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โง ๐ด โค ๐ต) โ (๐ด / ๐ต) โ โ) |
8 | | elunitge0 32879 |
. . . . . . . 8
โข (๐ด โ (0[,]1) โ 0 โค
๐ด) |
9 | 8 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ 0 โค ๐ด) |
10 | | elunitge0 32879 |
. . . . . . . . . 10
โข (๐ต โ (0[,]1) โ 0 โค
๐ต) |
11 | 10 | adantr 482 |
. . . . . . . . 9
โข ((๐ต โ (0[,]1) โง ๐ต โ 0) โ 0 โค ๐ต) |
12 | | 0re 11216 |
. . . . . . . . . . . . 13
โข 0 โ
โ |
13 | | ltlen 11315 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง ๐ต
โ โ) โ (0 < ๐ต โ (0 โค ๐ต โง ๐ต โ 0))) |
14 | 12, 3, 13 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ต โ (0[,]1) โ (0 <
๐ต โ (0 โค ๐ต โง ๐ต โ 0))) |
15 | 14 | biimpar 479 |
. . . . . . . . . . 11
โข ((๐ต โ (0[,]1) โง (0 โค
๐ต โง ๐ต โ 0)) โ 0 < ๐ต) |
16 | 15 | 3impb 1116 |
. . . . . . . . . 10
โข ((๐ต โ (0[,]1) โง 0 โค
๐ต โง ๐ต โ 0) โ 0 < ๐ต) |
17 | 16 | 3com23 1127 |
. . . . . . . . 9
โข ((๐ต โ (0[,]1) โง ๐ต โ 0 โง 0 โค ๐ต) โ 0 < ๐ต) |
18 | 11, 17 | mpd3an3 1463 |
. . . . . . . 8
โข ((๐ต โ (0[,]1) โง ๐ต โ 0) โ 0 < ๐ต) |
19 | 18 | 3adant1 1131 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ 0 < ๐ต) |
20 | | divge0 12083 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
21 | 2, 9, 4, 19, 20 | syl22anc 838 |
. . . . . 6
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ 0 โค (๐ด / ๐ต)) |
22 | 21 | adantr 482 |
. . . . 5
โข (((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โง ๐ด โค ๐ต) โ 0 โค (๐ด / ๐ต)) |
23 | | 1red 11215 |
. . . . . . . 8
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ 1 โ
โ) |
24 | | ledivmul 12090 |
. . . . . . . 8
โข ((๐ด โ โ โง 1 โ
โ โง (๐ต โ
โ โง 0 < ๐ต))
โ ((๐ด / ๐ต) โค 1 โ ๐ด โค (๐ต ยท 1))) |
25 | 2, 23, 4, 19, 24 | syl112anc 1375 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ ((๐ด / ๐ต) โค 1 โ ๐ด โค (๐ต ยท 1))) |
26 | | ax-1rid 11180 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต ยท 1) = ๐ต) |
27 | 26 | breq2d 5161 |
. . . . . . . 8
โข (๐ต โ โ โ (๐ด โค (๐ต ยท 1) โ ๐ด โค ๐ต)) |
28 | 4, 27 | syl 17 |
. . . . . . 7
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (๐ด โค (๐ต ยท 1) โ ๐ด โค ๐ต)) |
29 | 25, 28 | bitr2d 280 |
. . . . . 6
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (๐ด โค ๐ต โ (๐ด / ๐ต) โค 1)) |
30 | 29 | biimpa 478 |
. . . . 5
โข (((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โง ๐ด โค ๐ต) โ (๐ด / ๐ต) โค 1) |
31 | 7, 22, 30 | 3jca 1129 |
. . . 4
โข (((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โง ๐ด โค ๐ต) โ ((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1)) |
32 | 31 | ex 414 |
. . 3
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (๐ด โค ๐ต โ ((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1))) |
33 | | simp3 1139 |
. . . 4
โข (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1) โ (๐ด / ๐ต) โค 1) |
34 | 33, 29 | imbitrrid 245 |
. . 3
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1) โ ๐ด โค ๐ต)) |
35 | 32, 34 | impbid 211 |
. 2
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (๐ด โค ๐ต โ ((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1))) |
36 | | elicc01 13443 |
. 2
โข ((๐ด / ๐ต) โ (0[,]1) โ ((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1)) |
37 | 35, 36 | bitr4di 289 |
1
โข ((๐ด โ (0[,]1) โง ๐ต โ (0[,]1) โง ๐ต โ 0) โ (๐ด โค ๐ต โ (๐ด / ๐ต) โ (0[,]1))) |