Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ต โ โ) |
2 | | simpl3 1194 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ e โค ๐ด) |
3 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
4 | | ere 15976 |
. . . . . . . . . . 11
โข e โ
โ |
5 | | simpl1 1192 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ โ) |
6 | | lelttr 11250 |
. . . . . . . . . . 11
โข ((e
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((e โค ๐ด โง ๐ด < ๐ต) โ e < ๐ต)) |
7 | 4, 5, 1, 6 | mp3an2i 1467 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((e โค ๐ด โง ๐ด < ๐ต) โ e < ๐ต)) |
8 | 2, 3, 7 | mp2and 698 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ e < ๐ต) |
9 | | epos 16094 |
. . . . . . . . . 10
โข 0 <
e |
10 | | 0re 11162 |
. . . . . . . . . . 11
โข 0 โ
โ |
11 | | lttr 11236 |
. . . . . . . . . . 11
โข ((0
โ โ โง e โ โ โง ๐ต โ โ) โ ((0 < e โง e
< ๐ต) โ 0 < ๐ต)) |
12 | 10, 4, 1, 11 | mp3an12i 1466 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((0 < e โง e < ๐ต) โ 0 < ๐ต)) |
13 | 9, 12 | mpani 695 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (e < ๐ต โ 0 < ๐ต)) |
14 | 8, 13 | mpd 15 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 0 < ๐ต) |
15 | 1, 14 | elrpd 12959 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ต โ
โ+) |
16 | | ltletr 11252 |
. . . . . . . . . . 11
โข ((0
โ โ โง e โ โ โง ๐ด โ โ) โ ((0 < e โง e
โค ๐ด) โ 0 < ๐ด)) |
17 | 10, 4, 5, 16 | mp3an12i 1466 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((0 < e โง e โค ๐ด) โ 0 < ๐ด)) |
18 | 9, 17 | mpani 695 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (e โค ๐ด โ 0 < ๐ด)) |
19 | 2, 18 | mpd 15 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 0 < ๐ด) |
20 | 5, 19 | elrpd 12959 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ
โ+) |
21 | 15, 20 | rpdivcld 12979 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต / ๐ด) โ
โ+) |
22 | | relogcl 25947 |
. . . . . 6
โข ((๐ต / ๐ด) โ โ+ โ
(logโ(๐ต / ๐ด)) โ
โ) |
23 | 21, 22 | syl 17 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) โ โ) |
24 | 1, 20 | rerpdivcld 12993 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต / ๐ด) โ โ) |
25 | | 1re 11160 |
. . . . . 6
โข 1 โ
โ |
26 | | resubcl 11470 |
. . . . . 6
โข (((๐ต / ๐ด) โ โ โง 1 โ โ)
โ ((๐ต / ๐ด) โ 1) โ
โ) |
27 | 24, 25, 26 | sylancl 587 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ) |
28 | | relogcl 25947 |
. . . . . . 7
โข (๐ด โ โ+
โ (logโ๐ด) โ
โ) |
29 | 20, 28 | syl 17 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ด) โ โ) |
30 | 27, 29 | remulcld 11190 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)) โ
โ) |
31 | | reeflog 25952 |
. . . . . . . . 9
โข ((๐ต / ๐ด) โ โ+ โ
(expโ(logโ(๐ต /
๐ด))) = (๐ต / ๐ด)) |
32 | 21, 31 | syl 17 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ(๐ต / ๐ด))) = (๐ต / ๐ด)) |
33 | | ax-1cn 11114 |
. . . . . . . . 9
โข 1 โ
โ |
34 | 24 | recnd 11188 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต / ๐ด) โ โ) |
35 | | pncan3 11414 |
. . . . . . . . 9
โข ((1
โ โ โง (๐ต /
๐ด) โ โ) โ
(1 + ((๐ต / ๐ด) โ 1)) = (๐ต / ๐ด)) |
36 | 33, 34, 35 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 + ((๐ต / ๐ด) โ 1)) = (๐ต / ๐ด)) |
37 | 32, 36 | eqtr4d 2776 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ(๐ต / ๐ด))) = (1 + ((๐ต / ๐ด) โ 1))) |
38 | 5 | recnd 11188 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ โ) |
39 | 38 | mulid2d 11178 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 ยท ๐ด) = ๐ด) |
40 | 39, 3 | eqbrtrd 5128 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 ยท ๐ด) < ๐ต) |
41 | | 1red 11161 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 โ โ) |
42 | | ltmuldiv 12033 |
. . . . . . . . . . 11
โข ((1
โ โ โง ๐ต
โ โ โง (๐ด
โ โ โง 0 < ๐ด)) โ ((1 ยท ๐ด) < ๐ต โ 1 < (๐ต / ๐ด))) |
43 | 41, 1, 5, 19, 42 | syl112anc 1375 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((1 ยท ๐ด) < ๐ต โ 1 < (๐ต / ๐ด))) |
44 | 40, 43 | mpbid 231 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 < (๐ต / ๐ด)) |
45 | | difrp 12958 |
. . . . . . . . . 10
โข ((1
โ โ โง (๐ต /
๐ด) โ โ) โ
(1 < (๐ต / ๐ด) โ ((๐ต / ๐ด) โ 1) โ
โ+)) |
46 | 25, 24, 45 | sylancr 588 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 < (๐ต / ๐ด) โ ((๐ต / ๐ด) โ 1) โ
โ+)) |
47 | 44, 46 | mpbid 231 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ+) |
48 | | efgt1p 16002 |
. . . . . . . 8
โข (((๐ต / ๐ด) โ 1) โ โ+
โ (1 + ((๐ต / ๐ด) โ 1)) <
(expโ((๐ต / ๐ด) โ 1))) |
49 | 47, 48 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 + ((๐ต / ๐ด) โ 1)) < (expโ((๐ต / ๐ด) โ 1))) |
50 | 37, 49 | eqbrtrd 5128 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ(๐ต / ๐ด))) < (expโ((๐ต / ๐ด) โ 1))) |
51 | | eflt 16004 |
. . . . . . 7
โข
(((logโ(๐ต /
๐ด)) โ โ โง
((๐ต / ๐ด) โ 1) โ โ) โ
((logโ(๐ต / ๐ด)) < ((๐ต / ๐ด) โ 1) โ
(expโ(logโ(๐ต /
๐ด))) <
(expโ((๐ต / ๐ด) โ 1)))) |
52 | 23, 27, 51 | syl2anc 585 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ(๐ต / ๐ด)) < ((๐ต / ๐ด) โ 1) โ
(expโ(logโ(๐ต /
๐ด))) <
(expโ((๐ต / ๐ด) โ 1)))) |
53 | 50, 52 | mpbird 257 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) < ((๐ต / ๐ด) โ 1)) |
54 | 27 | recnd 11188 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ) |
55 | 54 | mulid1d 11177 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท 1) = ((๐ต / ๐ด) โ 1)) |
56 | | df-e 15956 |
. . . . . . . . 9
โข e =
(expโ1) |
57 | | reeflog 25952 |
. . . . . . . . . . 11
โข (๐ด โ โ+
โ (expโ(logโ๐ด)) = ๐ด) |
58 | 20, 57 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ(logโ๐ด)) = ๐ด) |
59 | 2, 58 | breqtrrd 5134 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ e โค (expโ(logโ๐ด))) |
60 | 56, 59 | eqbrtrrid 5142 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (expโ1) โค
(expโ(logโ๐ด))) |
61 | | efle 16005 |
. . . . . . . . 9
โข ((1
โ โ โง (logโ๐ด) โ โ) โ (1 โค
(logโ๐ด) โ
(expโ1) โค (expโ(logโ๐ด)))) |
62 | 25, 29, 61 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 โค (logโ๐ด) โ (expโ1) โค
(expโ(logโ๐ด)))) |
63 | 60, 62 | mpbird 257 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 โค (logโ๐ด)) |
64 | | posdif 11653 |
. . . . . . . . . 10
โข ((1
โ โ โง (๐ต /
๐ด) โ โ) โ
(1 < (๐ต / ๐ด) โ 0 < ((๐ต / ๐ด) โ 1))) |
65 | 25, 24, 64 | sylancr 588 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 < (๐ต / ๐ด) โ 0 < ((๐ต / ๐ด) โ 1))) |
66 | 44, 65 | mpbid 231 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 0 < ((๐ต / ๐ด) โ 1)) |
67 | | lemul2 12013 |
. . . . . . . 8
โข ((1
โ โ โง (logโ๐ด) โ โ โง (((๐ต / ๐ด) โ 1) โ โ โง 0 <
((๐ต / ๐ด) โ 1))) โ (1 โค
(logโ๐ด) โ
(((๐ต / ๐ด) โ 1) ยท 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)))) |
68 | 41, 29, 27, 66, 67 | syl112anc 1375 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 โค (logโ๐ด) โ (((๐ต / ๐ด) โ 1) ยท 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)))) |
69 | 63, 68 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด))) |
70 | 55, 69 | eqbrtrrd 5130 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) โ 1) โค (((๐ต / ๐ด) โ 1) ยท (logโ๐ด))) |
71 | 23, 27, 30, 53, 70 | ltletrd 11320 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) < (((๐ต / ๐ด) โ 1) ยท (logโ๐ด))) |
72 | | relogdiv 25964 |
. . . . 5
โข ((๐ต โ โ+
โง ๐ด โ
โ+) โ (logโ(๐ต / ๐ด)) = ((logโ๐ต) โ (logโ๐ด))) |
73 | 15, 20, 72 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ(๐ต / ๐ด)) = ((logโ๐ต) โ (logโ๐ด))) |
74 | | 1cnd 11155 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ 1 โ โ) |
75 | 29 | recnd 11188 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ด) โ โ) |
76 | 34, 74, 75 | subdird 11617 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)) = (((๐ต / ๐ด) ยท (logโ๐ด)) โ (1 ยท (logโ๐ด)))) |
77 | 1 | recnd 11188 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ต โ โ) |
78 | 20 | rpne0d 12967 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ๐ด โ 0) |
79 | 77, 38, 75, 78 | div32d 11959 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((๐ต / ๐ด) ยท (logโ๐ด)) = (๐ต ยท ((logโ๐ด) / ๐ด))) |
80 | 75 | mulid2d 11178 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (1 ยท (logโ๐ด)) = (logโ๐ด)) |
81 | 79, 80 | oveq12d 7376 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) ยท (logโ๐ด)) โ (1 ยท (logโ๐ด))) = ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด))) |
82 | 76, 81 | eqtrd 2773 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((๐ต / ๐ด) โ 1) ยท (logโ๐ด)) = ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด))) |
83 | 71, 73, 82 | 3brtr3d 5137 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ต) โ (logโ๐ด)) < ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด))) |
84 | | relogcl 25947 |
. . . . 5
โข (๐ต โ โ+
โ (logโ๐ต) โ
โ) |
85 | 15, 84 | syl 17 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ต) โ โ) |
86 | 29, 20 | rerpdivcld 12993 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ด) / ๐ด) โ โ) |
87 | 1, 86 | remulcld 11190 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (๐ต ยท ((logโ๐ด) / ๐ด)) โ โ) |
88 | 85, 87, 29 | ltsub1d 11769 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ต) < (๐ต ยท ((logโ๐ด) / ๐ด)) โ ((logโ๐ต) โ (logโ๐ด)) < ((๐ต ยท ((logโ๐ด) / ๐ด)) โ (logโ๐ด)))) |
89 | 83, 88 | mpbird 257 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (logโ๐ต) < (๐ต ยท ((logโ๐ด) / ๐ด))) |
90 | 85, 86, 15 | ltdivmuld 13013 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ (((logโ๐ต) / ๐ต) < ((logโ๐ด) / ๐ด) โ (logโ๐ต) < (๐ต ยท ((logโ๐ด) / ๐ด)))) |
91 | 89, 90 | mpbird 257 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง e โค
๐ด) โง ๐ด < ๐ต) โ ((logโ๐ต) / ๐ต) < ((logโ๐ด) / ๐ด)) |