Step | Hyp | Ref
| Expression |
1 | | posdif 11655 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
2 | | resubcl 11472 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต โ ๐ด) โ โ) |
3 | | nnrecl 12418 |
. . . . . . 7
โข (((๐ต โ ๐ด) โ โ โง 0 < (๐ต โ ๐ด)) โ โ๐ฆ โ โ (1 / ๐ฆ) < (๐ต โ ๐ด)) |
4 | 2, 3 | sylan 581 |
. . . . . 6
โข (((๐ต โ โ โง ๐ด โ โ) โง 0 <
(๐ต โ ๐ด)) โ โ๐ฆ โ โ (1 / ๐ฆ) < (๐ต โ ๐ด)) |
5 | 4 | ex 414 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ (0 <
(๐ต โ ๐ด) โ โ๐ฆ โ โ (1 / ๐ฆ) < (๐ต โ ๐ด))) |
6 | 5 | ancoms 460 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 <
(๐ต โ ๐ด) โ โ๐ฆ โ โ (1 / ๐ฆ) < (๐ต โ ๐ด))) |
7 | 1, 6 | sylbid 239 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ โ๐ฆ โ โ (1 / ๐ฆ) < (๐ต โ ๐ด))) |
8 | | nnre 12167 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
9 | 8 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ ๐ฆ โ
โ) |
10 | | simplr 768 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ ๐ต โ
โ) |
11 | 9, 10 | remulcld 11192 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ (๐ฆ ยท ๐ต) โ โ) |
12 | | peano2rem 11475 |
. . . . . . 7
โข ((๐ฆ ยท ๐ต) โ โ โ ((๐ฆ ยท ๐ต) โ 1) โ
โ) |
13 | 11, 12 | syl 17 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ ((๐ฆ ยท ๐ต) โ 1) โ
โ) |
14 | | zbtwnre 12878 |
. . . . . 6
โข (((๐ฆ ยท ๐ต) โ 1) โ โ โ
โ!๐ง โ โค
(((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1))) |
15 | | reurex 3360 |
. . . . . 6
โข
(โ!๐ง โ
โค (((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โ โ๐ง โ โค (((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1))) |
16 | 13, 14, 15 | 3syl 18 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ
โ๐ง โ โค
(((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1))) |
17 | | znq 12884 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ฆ โ โ) โ (๐ง / ๐ฆ) โ โ) |
18 | 17 | ancoms 460 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ง โ โค) โ (๐ง / ๐ฆ) โ โ) |
19 | 18 | adantl 483 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ง / ๐ฆ) โ โ) |
20 | | an32 645 |
. . . . . . . . . 10
โข
(((((๐ฆ ยท
๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โง (1 / ๐ฆ) < (๐ต โ ๐ด)) โ ((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง (1 / ๐ฆ) < (๐ต โ ๐ด)) โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1))) |
21 | 8 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ฆ โ
โ) |
22 | | simpll 766 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ด โ
โ) |
23 | 21, 22 | remulcld 11192 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ฆ ยท ๐ด) โ โ) |
24 | 13 | adantrr 716 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ((๐ฆ ยท ๐ต) โ 1) โ
โ) |
25 | | zre 12510 |
. . . . . . . . . . . . . 14
โข (๐ง โ โค โ ๐ง โ
โ) |
26 | 25 | ad2antll 728 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ง โ
โ) |
27 | | ltletr 11254 |
. . . . . . . . . . . . 13
โข (((๐ฆ ยท ๐ด) โ โ โง ((๐ฆ ยท ๐ต) โ 1) โ โ โง ๐ง โ โ) โ (((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โง ((๐ฆ ยท ๐ต) โ 1) โค ๐ง) โ (๐ฆ ยท ๐ด) < ๐ง)) |
28 | 23, 24, 26, 27 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โง ((๐ฆ ยท ๐ต) โ 1) โค ๐ง) โ (๐ฆ ยท ๐ด) < ๐ง)) |
29 | 21 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ฆ โ
โ) |
30 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ต โ
โ) |
31 | 30 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ต โ
โ) |
32 | 22 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ๐ด โ
โ) |
33 | 29, 31, 32 | subdid 11618 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ฆ ยท (๐ต โ ๐ด)) = ((๐ฆ ยท ๐ต) โ (๐ฆ ยท ๐ด))) |
34 | 33 | breq2d 5122 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (1 <
(๐ฆ ยท (๐ต โ ๐ด)) โ 1 < ((๐ฆ ยท ๐ต) โ (๐ฆ ยท ๐ด)))) |
35 | | 1red 11163 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ 1
โ โ) |
36 | 30, 22 | resubcld 11590 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ต โ ๐ด) โ โ) |
37 | | nngt0 12191 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ โ 0 <
๐ฆ) |
38 | 37 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ 0 <
๐ฆ) |
39 | | ltdivmul 12037 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง (๐ต
โ ๐ด) โ โ
โง (๐ฆ โ โ
โง 0 < ๐ฆ)) โ ((1
/ ๐ฆ) < (๐ต โ ๐ด) โ 1 < (๐ฆ ยท (๐ต โ ๐ด)))) |
40 | 35, 36, 21, 38, 39 | syl112anc 1375 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ((1 /
๐ฆ) < (๐ต โ ๐ด) โ 1 < (๐ฆ ยท (๐ต โ ๐ด)))) |
41 | 11 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ฆ ยท ๐ต) โ โ) |
42 | | ltsub13 11643 |
. . . . . . . . . . . . . . . 16
โข (((๐ฆ ยท ๐ด) โ โ โง (๐ฆ ยท ๐ต) โ โ โง 1 โ โ)
โ ((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โ 1 < ((๐ฆ ยท ๐ต) โ (๐ฆ ยท ๐ด)))) |
43 | 23, 41, 35, 42 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โ 1 < ((๐ฆ ยท ๐ต) โ (๐ฆ ยท ๐ด)))) |
44 | 34, 40, 43 | 3bitr4rd 312 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โ (1 / ๐ฆ) < (๐ต โ ๐ด))) |
45 | 44 | anbi1d 631 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โง ((๐ฆ ยท ๐ต) โ 1) โค ๐ง) โ ((1 / ๐ฆ) < (๐ต โ ๐ด) โง ((๐ฆ ยท ๐ต) โ 1) โค ๐ง))) |
46 | 45 | biancomd 465 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((๐ฆ ยท ๐ด) < ((๐ฆ ยท ๐ต) โ 1) โง ((๐ฆ ยท ๐ต) โ 1) โค ๐ง) โ (((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง (1 / ๐ฆ) < (๐ต โ ๐ด)))) |
47 | | ltmuldiv2 12036 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐ง โ โ โง (๐ฆ โ โ โง 0 <
๐ฆ)) โ ((๐ฆ ยท ๐ด) < ๐ง โ ๐ด < (๐ง / ๐ฆ))) |
48 | 22, 26, 21, 38, 47 | syl112anc 1375 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ((๐ฆ ยท ๐ด) < ๐ง โ ๐ด < (๐ง / ๐ฆ))) |
49 | 28, 46, 48 | 3imtr3d 293 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง (1 / ๐ฆ) < (๐ต โ ๐ด)) โ ๐ด < (๐ง / ๐ฆ))) |
50 | 41 | recnd 11190 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ฆ ยท ๐ต) โ โ) |
51 | | ax-1cn 11116 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ |
52 | | npcan 11417 |
. . . . . . . . . . . . . . 15
โข (((๐ฆ ยท ๐ต) โ โ โง 1 โ โ)
โ (((๐ฆ ยท ๐ต) โ 1) + 1) = (๐ฆ ยท ๐ต)) |
53 | 50, 51, 52 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((๐ฆ ยท ๐ต) โ 1) + 1) = (๐ฆ ยท ๐ต)) |
54 | 53 | breq2d 5122 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1) โ ๐ง < (๐ฆ ยท ๐ต))) |
55 | | ltdivmul 12037 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โ โง ๐ต โ โ โง (๐ฆ โ โ โง 0 <
๐ฆ)) โ ((๐ง / ๐ฆ) < ๐ต โ ๐ง < (๐ฆ ยท ๐ต))) |
56 | 26, 30, 21, 38, 55 | syl112anc 1375 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ ((๐ง / ๐ฆ) < ๐ต โ ๐ง < (๐ฆ ยท ๐ต))) |
57 | 54, 56 | bitr4d 282 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1) โ (๐ง / ๐ฆ) < ๐ต)) |
58 | 57 | biimpd 228 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ (๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1) โ (๐ง / ๐ฆ) < ๐ต)) |
59 | 49, 58 | anim12d 610 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง (1 / ๐ฆ) < (๐ต โ ๐ด)) โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โ (๐ด < (๐ง / ๐ฆ) โง (๐ง / ๐ฆ) < ๐ต))) |
60 | 20, 59 | biimtrid 241 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โง (1 / ๐ฆ) < (๐ต โ ๐ด)) โ (๐ด < (๐ง / ๐ฆ) โง (๐ง / ๐ฆ) < ๐ต))) |
61 | | breq2 5114 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ง / ๐ฆ) โ (๐ด < ๐ฅ โ ๐ด < (๐ง / ๐ฆ))) |
62 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ง / ๐ฆ) โ (๐ฅ < ๐ต โ (๐ง / ๐ฆ) < ๐ต)) |
63 | 61, 62 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฅ = (๐ง / ๐ฆ) โ ((๐ด < ๐ฅ โง ๐ฅ < ๐ต) โ (๐ด < (๐ง / ๐ฆ) โง (๐ง / ๐ฆ) < ๐ต))) |
64 | 63 | rspcev 3584 |
. . . . . . . . 9
โข (((๐ง / ๐ฆ) โ โ โง (๐ด < (๐ง / ๐ฆ) โง (๐ง / ๐ฆ) < ๐ต)) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |
65 | 19, 60, 64 | syl6an 683 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
(((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โง (1 / ๐ฆ) < (๐ต โ ๐ด)) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))) |
66 | 65 | expd 417 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง ๐ง โ โค)) โ
((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โ ((1 / ๐ฆ) < (๐ต โ ๐ด) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)))) |
67 | 66 | expr 458 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ (๐ง โ โค โ ((((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โ ((1 / ๐ฆ) < (๐ต โ ๐ด) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))))) |
68 | 67 | rexlimdv 3151 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ
(โ๐ง โ โค
(((๐ฆ ยท ๐ต) โ 1) โค ๐ง โง ๐ง < (((๐ฆ ยท ๐ต) โ 1) + 1)) โ ((1 / ๐ฆ) < (๐ต โ ๐ด) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)))) |
69 | 16, 68 | mpd 15 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ฆ โ โ) โ ((1 /
๐ฆ) < (๐ต โ ๐ด) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))) |
70 | 69 | rexlimdva 3153 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฆ โ โ (1
/ ๐ฆ) < (๐ต โ ๐ด) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))) |
71 | 7, 70 | syld 47 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต))) |
72 | 71 | 3impia 1118 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |