Step | Hyp | Ref
| Expression |
1 | | simpl2 1001 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ต โ โ) |
2 | | simpl3 1002 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ e โค ๐ด) |
3 | | simpr 110 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
4 | | ere 11680 |
. . . . . . . . . . 11
โข e โ
โ |
5 | | simpl1 1000 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ โ) |
6 | | lelttr 8048 |
. . . . . . . . . . 11
โข ((e
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((e โค ๐ด โง ๐ด < ๐ต) โ e < ๐ต)) |
7 | 4, 5, 1, 6 | mp3an2i 1342 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((e โค ๐ด โง ๐ด < ๐ต) โ e < ๐ต)) |
8 | 2, 3, 7 | mp2and 433 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ e < ๐ต) |
9 | | epos 11790 |
. . . . . . . . . 10
โข 0 <
e |
10 | | 0re 7959 |
. . . . . . . . . . 11
โข 0 โ
โ |
11 | | lttr 8033 |
. . . . . . . . . . 11
โข ((0
โ โ โง e โ โ โง ๐ต โ โ) โ ((0 < e โง e
< ๐ต) โ 0 < ๐ต)) |
12 | 10, 4, 1, 11 | mp3an12i 1341 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((0 < e โง e < ๐ต) โ 0 < ๐ต)) |
13 | 9, 12 | mpani 430 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (e < ๐ต โ 0 < ๐ต)) |
14 | 8, 13 | mpd 13 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 0 < ๐ต) |
15 | 1, 14 | elrpd 9695 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ต โ
โ+) |
16 | | ltletr 8049 |
. . . . . . . . . . 11
โข ((0
โ โ โง e โ โ โง ๐ด โ โ) โ ((0 < e โง e
โค ๐ด) โ 0 < ๐ด)) |
17 | 10, 4, 5, 16 | mp3an12i 1341 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((0 < e โง e โค ๐ด) โ 0 < ๐ด)) |
18 | 9, 17 | mpani 430 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (e โค ๐ด โ 0 < ๐ด)) |
19 | 2, 18 | mpd 13 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 0 < ๐ด) |
20 | 5, 19 | elrpd 9695 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ
โ+) |
21 | 15, 20 | rpdivcld 9716 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต / ๐ด) โ
โ+) |
22 | | relogcl 14322 |
. . . . . 6
โข ((๐ต / ๐ด) โ โ+ โ
(logโ(๐ต / ๐ด)) โ
โ) |
23 | 21, 22 | syl 14 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) โ โ) |
24 | 1, 20 | rerpdivcld 9730 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต / ๐ด) โ โ) |
25 | | 1re 7958 |
. . . . . 6
โข 1 โ
โ |
26 | | resubcl 8223 |
. . . . . 6
โข (((๐ต / ๐ด) โ โ โง 1 โ โ)
โ ((๐ต / ๐ด) โ 1) โ
โ) |
27 | 24, 25, 26 | sylancl 413 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ) |
28 | | relogcl 14322 |
. . . . . . 7
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
29 | 20, 28 | syl 14 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ด) โ โ) |
30 | 27, 29 | remulcld 7990 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)) โ
โ) |
31 | | reeflog 14323 |
. . . . . . . . 9
โข ((๐ต / ๐ด) โ โ+ โ
(expโ(logโ(๐ต /
๐ด))) = (๐ต / ๐ด)) |
32 | 21, 31 | syl 14 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ(๐ต / ๐ด))) = (๐ต / ๐ด)) |
33 | | ax-1cn 7906 |
. . . . . . . . 9
โข 1 โ
โ |
34 | 24 | recnd 7988 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต / ๐ด) โ โ) |
35 | | pncan3 8167 |
. . . . . . . . 9
โข ((1
โ โ โง (๐ต /
๐ด) โ โ) โ
(1 + ((๐ต / ๐ด) โ 1)) = (๐ต / ๐ด)) |
36 | 33, 34, 35 | sylancr 414 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 + ((๐ต / ๐ด) โ 1)) = (๐ต / ๐ด)) |
37 | 32, 36 | eqtr4d 2213 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ(๐ต / ๐ด))) = (1 + ((๐ต / ๐ด) โ 1))) |
38 | 5 | recnd 7988 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ โ) |
39 | 38 | mulid2d 7978 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 ยท ๐ด) = ๐ด) |
40 | 39, 3 | eqbrtrd 4027 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 ยท ๐ด) < ๐ต) |
41 | | 1red 7974 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 โ โ) |
42 | | ltmuldiv 8833 |
. . . . . . . . . . 11
โข ((1
โ โ โง ๐ต
โ โ โง (๐ด
โ โ โง 0 < ๐ด)) โ ((1 ยท ๐ด) < ๐ต โ 1 < (๐ต / ๐ด))) |
43 | 41, 1, 5, 19, 42 | syl112anc 1242 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((1 ยท ๐ด) < ๐ต โ 1 < (๐ต / ๐ด))) |
44 | 40, 43 | mpbid 147 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 < (๐ต / ๐ด)) |
45 | | difrp 9694 |
. . . . . . . . . 10
โข ((1
โ โ โง (๐ต /
๐ด) โ โ) โ
(1 < (๐ต / ๐ด) โ ((๐ต / ๐ด) โ 1) โ
โ+)) |
46 | 25, 24, 45 | sylancr 414 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 < (๐ต / ๐ด) โ ((๐ต / ๐ด) โ 1) โ
โ+)) |
47 | 44, 46 | mpbid 147 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ+) |
48 | | efgt1p 11706 |
. . . . . . . 8
โข (((๐ต / ๐ด) โ 1) โ โ+
โ (1 + ((๐ต / ๐ด) โ 1)) <
(expโ((๐ต / ๐ด) โ 1))) |
49 | 47, 48 | syl 14 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 + ((๐ต / ๐ด) โ 1)) < (expโ((๐ต / ๐ด) โ 1))) |
50 | 37, 49 | eqbrtrd 4027 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ(๐ต / ๐ด))) < (expโ((๐ต / ๐ด) โ 1))) |
51 | | eflt 14235 |
. . . . . . 7
โข
(((logโ(๐ต /
๐ด)) โ โ โง
((๐ต / ๐ด) โ 1) โ โ) โ
((logโ(๐ต / ๐ด)) < ((๐ต / ๐ด) โ 1) โ
(expโ(logโ(๐ต /
๐ด))) <
(expโ((๐ต / ๐ด) โ 1)))) |
52 | 23, 27, 51 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ(๐ต / ๐ด)) < ((๐ต / ๐ด) โ 1) โ
(expโ(logโ(๐ต /
๐ด))) <
(expโ((๐ต / ๐ด) โ 1)))) |
53 | 50, 52 | mpbird 167 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) < ((๐ต / ๐ด) โ 1)) |
54 | 27 | recnd 7988 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ) |
55 | 54 | mulridd 7976 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท 1) = ((๐ต / ๐ด) โ 1)) |
56 | | df-e 11659 |
. . . . . . . . 9
โข e =
(expโ1) |
57 | | reeflog 14323 |
. . . . . . . . . . 11
โข (๐ด โ โ+
โ (expโ(logโ๐ด)) = ๐ด) |
58 | 20, 57 | syl 14 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ๐ด)) = ๐ด) |
59 | 2, 58 | breqtrrd 4033 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ e โค (expโ(logโ๐ด))) |
60 | 56, 59 | eqbrtrrid 4041 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ1) โค
(expโ(logโ๐ด))) |
61 | | efle 14236 |
. . . . . . . . 9
โข ((1
โ โ โง (logโ๐ด) โ โ) โ (1 โค
(logโ๐ด) โ
(expโ1) โค (expโ(logโ๐ด)))) |
62 | 25, 29, 61 | sylancr 414 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 โค (logโ๐ด) โ (expโ1) โค
(expโ(logโ๐ด)))) |
63 | 60, 62 | mpbird 167 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 โค (logโ๐ด)) |
64 | | posdif 8414 |
. . . . . . . . . 10
โข ((1
โ โ โง (๐ต /
๐ด) โ โ) โ
(1 < (๐ต / ๐ด) โ 0 < ((๐ต / ๐ด) โ 1))) |
65 | 25, 24, 64 | sylancr 414 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 < (๐ต / ๐ด) โ 0 < ((๐ต / ๐ด) โ 1))) |
66 | 44, 65 | mpbid 147 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 0 < ((๐ต / ๐ด) โ 1)) |
67 | | lemul2 8816 |
. . . . . . . 8
โข ((1
โ โ โง (logโ๐ด) โ โ โง (((๐ต / ๐ด) โ 1) โ โ โง 0 <
((๐ต / ๐ด) โ 1))) โ (1 โค
(logโ๐ด) โ
(((๐ต / ๐ด) โ 1) ยท 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)))) |
68 | 41, 29, 27, 66, 67 | syl112anc 1242 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 โค (logโ๐ด) โ (((๐ต / ๐ด) โ 1) ยท 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)))) |
69 | 63, 68 | mpbid 147 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด))) |
70 | 55, 69 | eqbrtrrd 4029 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด))) |
71 | 23, 27, 30, 53, 70 | ltletrd 8382 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) < (((๐ต / ๐ด) โ 1) ยท (logโ๐ด))) |
72 | | relogdiv 14330 |
. . . . 5
โข ((๐ต โ โ+
โง ๐ด โ
โ+) โ (logโ(๐ต / ๐ด)) = ((logโ๐ต) โ (logโ๐ด))) |
73 | 15, 20, 72 | syl2anc 411 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) = ((logโ๐ต) โ (logโ๐ด))) |
74 | | 1cnd 7975 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 โ โ) |
75 | 29 | recnd 7988 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ด) โ โ) |
76 | 34, 74, 75 | subdird 8374 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)) = (((๐ต / ๐ด) ยท (logโ๐ด)) โ (1 ยท (logโ๐ด)))) |
77 | 1 | recnd 7988 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ต โ โ) |
78 | 20 | rpap0d 9704 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด # 0) |
79 | 77, 38, 75, 78 | div32apd 8773 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) ยท (logโ๐ด)) = (๐ต ยท ((logโ๐ด) / ๐ด))) |
80 | 75 | mulid2d 7978 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 ยท (logโ๐ด)) = (logโ๐ด)) |
81 | 79, 80 | oveq12d 5895 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) ยท (logโ๐ด)) โ (1 ยท (logโ๐ด))) = ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด))) |
82 | 76, 81 | eqtrd 2210 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)) = ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด))) |
83 | 71, 73, 82 | 3brtr3d 4036 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ต) โ (logโ๐ด)) < ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด))) |
84 | | relogcl 14322 |
. . . . 5
โข (๐ต โ โ+
โ (logโ๐ต) โ
โ) |
85 | 15, 84 | syl 14 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ต) โ โ) |
86 | 29, 20 | rerpdivcld 9730 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ด) / ๐ด) โ โ) |
87 | 1, 86 | remulcld 7990 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต ยท ((logโ๐ด) / ๐ด)) โ โ) |
88 | 85, 87, 29 | ltsub1d 8513 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ต) < (๐ต ยท ((logโ๐ด) / ๐ด)) โ ((logโ๐ต) โ (logโ๐ด)) < ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด)))) |
89 | 83, 88 | mpbird 167 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ต) < (๐ต ยท ((logโ๐ด) / ๐ด))) |
90 | 85, 86, 15 | ltdivmuld 9750 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((logโ๐ต) / ๐ต) < ((logโ๐ด) / ๐ด) โ (logโ๐ต) < (๐ต ยท ((logโ๐ด) / ๐ด)))) |
91 | 89, 90 | mpbird 167 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ต) / ๐ต) < ((logโ๐ด) / ๐ด)) |