Step | Hyp | Ref
| Expression |
1 | | rpre 12928 |
. . . 4
โข (๐ด โ โ+
โ ๐ด โ
โ) |
2 | | reefcl 15974 |
. . . 4
โข (๐ด โ โ โ
(expโ๐ด) โ
โ) |
3 | 1, 2 | syl 17 |
. . 3
โข (๐ด โ โ+
โ (expโ๐ด) โ
โ) |
4 | | efgt1 16003 |
. . 3
โข (๐ด โ โ+
โ 1 < (expโ๐ด)) |
5 | | cxp2limlem 26341 |
. . 3
โข
(((expโ๐ด)
โ โ โง 1 < (expโ๐ด)) โ (๐ โ โ+ โฆ (๐ / ((expโ๐ด)โ๐๐))) โ๐
0) |
6 | 3, 4, 5 | syl2anc 585 |
. 2
โข (๐ด โ โ+
โ (๐ โ
โ+ โฆ (๐ / ((expโ๐ด)โ๐๐))) โ๐
0) |
7 | | reefcl 15974 |
. . . . . . . 8
โข (๐ง โ โ โ
(expโ๐ง) โ
โ) |
8 | 7 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ง โ โ)
โ (expโ๐ง) โ
โ) |
9 | | 1re 11160 |
. . . . . . 7
โข 1 โ
โ |
10 | | ifcl 4532 |
. . . . . . 7
โข
(((expโ๐ง)
โ โ โง 1 โ โ) โ if(1 โค (expโ๐ง), (expโ๐ง), 1) โ โ) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ง โ โ)
โ if(1 โค (expโ๐ง), (expโ๐ง), 1) โ โ) |
12 | | rpre 12928 |
. . . . . . . . . 10
โข (๐ โ โ+
โ ๐ โ
โ) |
13 | | maxlt 13118 |
. . . . . . . . . 10
โข ((1
โ โ โง (expโ๐ง) โ โ โง ๐ โ โ) โ (if(1 โค
(expโ๐ง),
(expโ๐ง), 1) <
๐ โ (1 < ๐ โง (expโ๐ง) < ๐))) |
14 | 9, 8, 12, 13 | mp3an3an 1468 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง ๐ โ
โ+) โ (if(1 โค (expโ๐ง), (expโ๐ง), 1) < ๐ โ (1 < ๐ โง (expโ๐ง) < ๐))) |
15 | | simprrr 781 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ๐ง) < ๐) |
16 | | reeflog 25952 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ+
โ (expโ(logโ๐)) = ๐) |
17 | 16 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ(logโ๐)) = ๐) |
18 | 15, 17 | breqtrrd 5134 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ๐ง) < (expโ(logโ๐))) |
19 | | simplr 768 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ง โ โ) |
20 | 12 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ โ โ) |
21 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ 1 < ๐) |
22 | 20, 21 | rplogcld 26000 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (logโ๐) โ
โ+) |
23 | 22 | rpred 12962 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (logโ๐) โ โ) |
24 | | eflt 16004 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โ โง
(logโ๐) โ
โ) โ (๐ง <
(logโ๐) โ
(expโ๐ง) <
(expโ(logโ๐)))) |
25 | 19, 23, 24 | syl2anc 585 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (๐ง < (logโ๐) โ (expโ๐ง) < (expโ(logโ๐)))) |
26 | 18, 25 | mpbird 257 |
. . . . . . . . . . . 12
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ง < (logโ๐)) |
27 | | breq2 5110 |
. . . . . . . . . . . . . . 15
โข (๐ = (logโ๐) โ (๐ง < ๐ โ ๐ง < (logโ๐))) |
28 | | id 22 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (logโ๐) โ ๐ = (logโ๐)) |
29 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (logโ๐) โ ((expโ๐ด)โ๐๐) = ((expโ๐ด)โ๐(logโ๐))) |
30 | 28, 29 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (logโ๐) โ (๐ / ((expโ๐ด)โ๐๐)) = ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) |
31 | 30 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
โข (๐ = (logโ๐) โ (absโ(๐ / ((expโ๐ด)โ๐๐))) =
(absโ((logโ๐) /
((expโ๐ด)โ๐(logโ๐))))) |
32 | 31 | breq1d 5116 |
. . . . . . . . . . . . . . 15
โข (๐ = (logโ๐) โ ((absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ โ (absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) < ๐ฅ)) |
33 | 27, 32 | imbi12d 345 |
. . . . . . . . . . . . . 14
โข (๐ = (logโ๐) โ ((๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (๐ง < (logโ๐) โ (absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) < ๐ฅ))) |
34 | 33 | rspcv 3576 |
. . . . . . . . . . . . 13
โข
((logโ๐)
โ โ+ โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (๐ง < (logโ๐) โ (absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) < ๐ฅ))) |
35 | 22, 34 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (๐ง < (logโ๐) โ (absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) < ๐ฅ))) |
36 | 26, 35 | mpid 44 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) < ๐ฅ)) |
37 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ด โ โ) |
38 | 37 | relogefd 25999 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (logโ(expโ๐ด)) = ๐ด) |
39 | 38 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((logโ๐) ยท (logโ(expโ๐ด))) = ((logโ๐) ยท ๐ด)) |
40 | 22 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (logโ๐) โ โ) |
41 | | rpcn 12930 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โ+
โ ๐ด โ
โ) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ด โ โ) |
43 | 40, 42 | mulcomd 11181 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((logโ๐) ยท ๐ด) = (๐ด ยท (logโ๐))) |
44 | 39, 43 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((logโ๐) ยท (logโ(expโ๐ด))) = (๐ด ยท (logโ๐))) |
45 | 44 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ((logโ๐) ยท
(logโ(expโ๐ด))))
= (expโ(๐ด ยท
(logโ๐)))) |
46 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ๐ด) โ โ) |
47 | 46 | recnd 11188 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ๐ด) โ โ) |
48 | | efne0 15984 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ โ โ
(expโ๐ด) โ
0) |
49 | 42, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (expโ๐ด) โ 0) |
50 | 47, 49, 40 | cxpefd 26083 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((expโ๐ด)โ๐(logโ๐)) =
(expโ((logโ๐)
ยท (logโ(expโ๐ด))))) |
51 | | rpcn 12930 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ+
โ ๐ โ
โ) |
52 | 51 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ โ โ) |
53 | | rpne0 12936 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ+
โ ๐ โ
0) |
54 | 53 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ๐ โ 0) |
55 | 52, 54, 42 | cxpefd 26083 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (๐โ๐๐ด) = (expโ(๐ด ยท (logโ๐)))) |
56 | 45, 50, 55 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((expโ๐ด)โ๐(logโ๐)) = (๐โ๐๐ด)) |
57 | 56 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((logโ๐) / ((expโ๐ด)โ๐(logโ๐))) = ((logโ๐) / (๐โ๐๐ด))) |
58 | 57 | fveq2d 6847 |
. . . . . . . . . . . 12
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) =
(absโ((logโ๐) /
(๐โ๐๐ด)))) |
59 | 58 | breq1d 5116 |
. . . . . . . . . . 11
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ ((absโ((logโ๐) / ((expโ๐ด)โ๐(logโ๐)))) < ๐ฅ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ)) |
60 | 36, 59 | sylibd 238 |
. . . . . . . . . 10
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง (๐ โ
โ+ โง (1 < ๐ โง (expโ๐ง) < ๐))) โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ)) |
61 | 60 | expr 458 |
. . . . . . . . 9
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง ๐ โ
โ+) โ ((1 < ๐ โง (expโ๐ง) < ๐) โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
62 | 14, 61 | sylbid 239 |
. . . . . . . 8
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง ๐ โ
โ+) โ (if(1 โค (expโ๐ง), (expโ๐ง), 1) < ๐ โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
63 | 62 | com23 86 |
. . . . . . 7
โข (((๐ด โ โ+
โง ๐ง โ โ)
โง ๐ โ
โ+) โ (โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ (if(1 โค (expโ๐ง), (expโ๐ง), 1) < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
64 | 63 | ralrimdva 3148 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ง โ โ)
โ (โ๐ โ
โ+ (๐ง <
๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ โ๐ โ โ+ (if(1 โค
(expโ๐ง),
(expโ๐ง), 1) <
๐ โ
(absโ((logโ๐) /
(๐โ๐๐ด))) < ๐ฅ))) |
65 | | breq1 5109 |
. . . . . . 7
โข (๐ฆ = if(1 โค (expโ๐ง), (expโ๐ง), 1) โ (๐ฆ < ๐ โ if(1 โค (expโ๐ง), (expโ๐ง), 1) < ๐)) |
66 | 65 | rspceaimv 3584 |
. . . . . 6
โข ((if(1
โค (expโ๐ง),
(expโ๐ง), 1) โ
โ โง โ๐
โ โ+ (if(1 โค (expโ๐ง), (expโ๐ง), 1) < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ)) โ โ๐ฆ โ โ โ๐ โ โ+ (๐ฆ < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ)) |
67 | 11, 64, 66 | syl6an 683 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ง โ โ)
โ (โ๐ โ
โ+ (๐ง <
๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ โ๐ฆ โ โ โ๐ โ โ+ (๐ฆ < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
68 | 67 | rexlimdva 3149 |
. . . 4
โข (๐ด โ โ+
โ (โ๐ง โ
โ โ๐ โ
โ+ (๐ง <
๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ โ๐ฆ โ โ โ๐ โ โ+ (๐ฆ < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
69 | 68 | ralimdv 3163 |
. . 3
โข (๐ด โ โ+
โ (โ๐ฅ โ
โ+ โ๐ง โ โ โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ) โ โ๐ฅ โ โ+ โ๐ฆ โ โ โ๐ โ โ+
(๐ฆ < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
70 | | simpr 486 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ๐ โ โ+) |
71 | 1 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ๐ด โ โ) |
72 | 71 | rpefcld 15992 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ (expโ๐ด) โ
โ+) |
73 | | rpre 12928 |
. . . . . . . . 9
โข (๐ โ โ+
โ ๐ โ
โ) |
74 | 73 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ๐ โ โ) |
75 | 72, 74 | rpcxpcld 26103 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ((expโ๐ด)โ๐๐) โ
โ+) |
76 | 70, 75 | rpdivcld 12979 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ (๐ / ((expโ๐ด)โ๐๐)) โ
โ+) |
77 | 76 | rpcnd 12964 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ (๐ / ((expโ๐ด)โ๐๐)) โ
โ) |
78 | 77 | ralrimiva 3140 |
. . . 4
โข (๐ด โ โ+
โ โ๐ โ
โ+ (๐ /
((expโ๐ด)โ๐๐)) โ
โ) |
79 | | rpssre 12927 |
. . . . 5
โข
โ+ โ โ |
80 | 79 | a1i 11 |
. . . 4
โข (๐ด โ โ+
โ โ+ โ โ) |
81 | 78, 80 | rlim0lt 15397 |
. . 3
โข (๐ด โ โ+
โ ((๐ โ
โ+ โฆ (๐ / ((expโ๐ด)โ๐๐))) โ๐
0 โ โ๐ฅ โ
โ+ โ๐ง โ โ โ๐ โ โ+ (๐ง < ๐ โ (absโ(๐ / ((expโ๐ด)โ๐๐))) < ๐ฅ))) |
82 | | relogcl 25947 |
. . . . . . . 8
โข (๐ โ โ+
โ (logโ๐) โ
โ) |
83 | 82 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ (logโ๐) โ โ) |
84 | | simpr 486 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ๐ โ โ+) |
85 | 1 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ๐ด โ โ) |
86 | 84, 85 | rpcxpcld 26103 |
. . . . . . 7
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ (๐โ๐๐ด) โ
โ+) |
87 | 83, 86 | rerpdivcld 12993 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ((logโ๐) / (๐โ๐๐ด)) โ โ) |
88 | 87 | recnd 11188 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ โ
โ+) โ ((logโ๐) / (๐โ๐๐ด)) โ โ) |
89 | 88 | ralrimiva 3140 |
. . . 4
โข (๐ด โ โ+
โ โ๐ โ
โ+ ((logโ๐) / (๐โ๐๐ด)) โ โ) |
90 | 89, 80 | rlim0lt 15397 |
. . 3
โข (๐ด โ โ+
โ ((๐ โ
โ+ โฆ ((logโ๐) / (๐โ๐๐ด))) โ๐ 0 โ
โ๐ฅ โ
โ+ โ๐ฆ โ โ โ๐ โ โ+ (๐ฆ < ๐ โ (absโ((logโ๐) / (๐โ๐๐ด))) < ๐ฅ))) |
91 | 69, 81, 90 | 3imtr4d 294 |
. 2
โข (๐ด โ โ+
โ ((๐ โ
โ+ โฆ (๐ / ((expโ๐ด)โ๐๐))) โ๐
0 โ (๐ โ
โ+ โฆ ((logโ๐) / (๐โ๐๐ด))) โ๐
0)) |
92 | 6, 91 | mpd 15 |
1
โข (๐ด โ โ+
โ (๐ โ
โ+ โฆ ((logโ๐) / (๐โ๐๐ด))) โ๐
0) |