Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ ๐ด โ โ) |
2 | 1 | adantr 276 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง 1 < ๐ด) โ ๐ด โ โ) |
3 | | simp2 998 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ ๐ต โ โ) |
4 | 3 | adantr 276 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง 1 < ๐ด) โ ๐ต โ โ) |
5 | | simpr 110 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง 1 < ๐ด) โ 1 < ๐ด) |
6 | | simp3 999 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ 1 < ๐ต) |
7 | 6 | adantr 276 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง 1 < ๐ด) โ 1 < ๐ต) |
8 | | 1red 7971 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ 1 โ
โ) |
9 | 1, 8 | resubcld 8337 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ (๐ด โ 1) โ
โ) |
10 | 3, 8 | resubcld 8337 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ (๐ต โ 1) โ
โ) |
11 | 8, 3 | posdifd 8488 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ (1 < ๐ต โ 0 < (๐ต โ 1))) |
12 | 6, 11 | mpbid 147 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ 0 < (๐ต โ 1)) |
13 | 10, 12 | gt0ap0d 8585 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ (๐ต โ 1) #
0) |
14 | 9, 10, 13 | redivclapd 8791 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ ((๐ด โ 1) / (๐ต โ 1)) โ
โ) |
15 | | arch 9172 |
. . . . . . 7
โข (((๐ด โ 1) / (๐ต โ 1)) โ โ โ
โ๐ โ โ
((๐ด โ 1) / (๐ต โ 1)) < ๐) |
16 | 14, 15 | syl 14 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ โ๐ โ โ ((๐ด โ 1) / (๐ต โ 1)) < ๐) |
17 | 16 | 3expa 1203 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง 1 <
๐ต) โ โ๐ โ โ ((๐ด โ 1) / (๐ต โ 1)) < ๐) |
18 | 17 | adantrl 478 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โ โ๐ โ โ ((๐ด โ 1) / (๐ต โ 1)) < ๐) |
19 | | simplll 533 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ ๐ด โ โ) |
20 | 19 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ด โ โ) |
21 | | simpllr 534 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ ๐ต โ โ) |
22 | | 1red 7971 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ 1 โ
โ) |
23 | 21, 22 | resubcld 8337 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ (๐ต โ 1) โ โ) |
24 | | simpr 110 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ ๐ โ โ) |
25 | 24 | nnred 8931 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ ๐ โ โ) |
26 | 23, 25 | remulcld 7987 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ ((๐ต โ 1) ยท ๐) โ โ) |
27 | 26, 22 | readdcld 7986 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ (((๐ต โ 1) ยท ๐) + 1) โ โ) |
28 | 27 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (((๐ต โ 1) ยท ๐) + 1) โ โ) |
29 | 24 | nnnn0d 9228 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ ๐ โ โ0) |
30 | | reexpcl 10536 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ โ โ0)
โ (๐ตโ๐) โ
โ) |
31 | 21, 29, 30 | syl2anc 411 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ (๐ตโ๐) โ โ) |
32 | 31 | adantr 276 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (๐ตโ๐) โ โ) |
33 | | simpr 110 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ((๐ด โ 1) / (๐ต โ 1)) < ๐) |
34 | | 1red 7971 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ 1 โ
โ) |
35 | 20, 34 | resubcld 8337 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (๐ด โ 1) โ โ) |
36 | | simplr 528 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ โ โ) |
37 | 36 | nnred 8931 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ โ โ) |
38 | 21 | adantr 276 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ต โ โ) |
39 | 38, 34 | resubcld 8337 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (๐ต โ 1) โ โ) |
40 | | simplrr 536 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ 1 < ๐ต) |
41 | 40 | adantr 276 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ 1 < ๐ต) |
42 | 34, 38 | posdifd 8488 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (1 < ๐ต โ 0 < (๐ต โ 1))) |
43 | 41, 42 | mpbid 147 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ 0 < (๐ต โ 1)) |
44 | | ltdivmul 8832 |
. . . . . . . . . 10
โข (((๐ด โ 1) โ โ โง
๐ โ โ โง
((๐ต โ 1) โ
โ โง 0 < (๐ต
โ 1))) โ (((๐ด
โ 1) / (๐ต โ 1))
< ๐ โ (๐ด โ 1) < ((๐ต โ 1) ยท ๐))) |
45 | 35, 37, 39, 43, 44 | syl112anc 1242 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (((๐ด โ 1) / (๐ต โ 1)) < ๐ โ (๐ด โ 1) < ((๐ต โ 1) ยท ๐))) |
46 | 33, 45 | mpbid 147 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (๐ด โ 1) < ((๐ต โ 1) ยท ๐)) |
47 | 39, 37 | remulcld 7987 |
. . . . . . . . 9
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ((๐ต โ 1) ยท ๐) โ โ) |
48 | 20, 34, 47 | ltsubaddd 8497 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ((๐ด โ 1) < ((๐ต โ 1) ยท ๐) โ ๐ด < (((๐ต โ 1) ยท ๐) + 1))) |
49 | 46, 48 | mpbid 147 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ด < (((๐ต โ 1) ยท ๐) + 1)) |
50 | 36 | nnnn0d 9228 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ โ โ0) |
51 | | 0red 7957 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ 0 โ
โ) |
52 | | 0lt1 8083 |
. . . . . . . . . . . 12
โข 0 <
1 |
53 | | 0re 7956 |
. . . . . . . . . . . . 13
โข 0 โ
โ |
54 | | 1re 7955 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
55 | | lttr 8030 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง 1 โ โ โง ๐ต โ โ) โ ((0 < 1 โง 1
< ๐ต) โ 0 < ๐ต)) |
56 | 53, 54, 55 | mp3an12 1327 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ((0 <
1 โง 1 < ๐ต) โ 0
< ๐ต)) |
57 | 52, 56 | mpani 430 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (1 <
๐ต โ 0 < ๐ต)) |
58 | 21, 40, 57 | sylc 62 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ 0 < ๐ต) |
59 | 51, 21, 58 | ltled 8075 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ 0 โค ๐ต) |
60 | 59 | adantr 276 |
. . . . . . . 8
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ 0 โค ๐ต) |
61 | | bernneq2 10641 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ โ โ0
โง 0 โค ๐ต) โ
(((๐ต โ 1) ยท
๐) + 1) โค (๐ตโ๐)) |
62 | 38, 50, 60, 61 | syl3anc 1238 |
. . . . . . 7
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ (((๐ต โ 1) ยท ๐) + 1) โค (๐ตโ๐)) |
63 | 20, 28, 32, 49, 62 | ltletrd 8379 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (1 < ๐ด
โง 1 < ๐ต)) โง
๐ โ โ) โง
((๐ด โ 1) / (๐ต โ 1)) < ๐) โ ๐ด < (๐ตโ๐)) |
64 | 63 | ex 115 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โง ๐ โ โ) โ (((๐ด โ 1) / (๐ต โ 1)) < ๐ โ ๐ด < (๐ตโ๐))) |
65 | 64 | reximdva 2579 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โ (โ๐ โ โ ((๐ด โ 1) / (๐ต โ 1)) < ๐ โ โ๐ โ โ ๐ด < (๐ตโ๐))) |
66 | 18, 65 | mpd 13 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (1 <
๐ด โง 1 < ๐ต)) โ โ๐ โ โ ๐ด < (๐ตโ๐)) |
67 | 2, 4, 5, 7, 66 | syl22anc 1239 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง 1 < ๐ด) โ โ๐ โ โ ๐ด < (๐ตโ๐)) |
68 | | 1nn 8929 |
. . 3
โข 1 โ
โ |
69 | | simpr 110 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
70 | | simpl2 1001 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง ๐ด < ๐ต) โ ๐ต โ โ) |
71 | 70 | recnd 7985 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง ๐ด < ๐ต) โ ๐ต โ โ) |
72 | | exp1 10525 |
. . . . 5
โข (๐ต โ โ โ (๐ตโ1) = ๐ต) |
73 | 71, 72 | syl 14 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง ๐ด < ๐ต) โ (๐ตโ1) = ๐ต) |
74 | 69, 73 | breqtrrd 4031 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง ๐ด < ๐ต) โ ๐ด < (๐ตโ1)) |
75 | | oveq2 5882 |
. . . . 5
โข (๐ = 1 โ (๐ตโ๐) = (๐ตโ1)) |
76 | 75 | breq2d 4015 |
. . . 4
โข (๐ = 1 โ (๐ด < (๐ตโ๐) โ ๐ด < (๐ตโ1))) |
77 | 76 | rspcev 2841 |
. . 3
โข ((1
โ โ โง ๐ด <
(๐ตโ1)) โ
โ๐ โ โ
๐ด < (๐ตโ๐)) |
78 | 68, 74, 77 | sylancr 414 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โง ๐ด < ๐ต) โ โ๐ โ โ ๐ด < (๐ตโ๐)) |
79 | | axltwlin 8024 |
. . . . 5
โข ((1
โ โ โง ๐ต
โ โ โง ๐ด
โ โ) โ (1 < ๐ต โ (1 < ๐ด โจ ๐ด < ๐ต))) |
80 | 54, 79 | mp3an1 1324 |
. . . 4
โข ((๐ต โ โ โง ๐ด โ โ) โ (1 <
๐ต โ (1 < ๐ด โจ ๐ด < ๐ต))) |
81 | 80 | ancoms 268 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (1 <
๐ต โ (1 < ๐ด โจ ๐ด < ๐ต))) |
82 | 81 | 3impia 1200 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ (1 < ๐ด โจ ๐ด < ๐ต)) |
83 | 67, 78, 82 | mpjaodan 798 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง 1 <
๐ต) โ โ๐ โ โ ๐ด < (๐ตโ๐)) |