Step | Hyp | Ref
| Expression |
1 | | 3re 12240 |
. . 3
โข 3 โ
โ |
2 | 1 | a1i 11 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 3 โ โ) |
3 | | 0red 11165 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 0 โ โ) |
4 | 3 | recnd 11190 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 0 โ โ) |
5 | | ovexd 7397 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ ((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))) โ V) |
6 | | simpr 486 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ๐ต โ
โ+) |
7 | | recl 15002 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
8 | 7 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (โโ๐ด)
โ โ) |
9 | | 1re 11162 |
. . . . . . 7
โข 1 โ
โ |
10 | | ifcl 4536 |
. . . . . . 7
โข
(((โโ๐ด)
โ โ โง 1 โ โ) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ
โ) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+)
โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ โ) |
12 | 9 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 1 โ โ) |
13 | | 0lt1 11684 |
. . . . . . . 8
โข 0 <
1 |
14 | 13 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 0 < 1) |
15 | | max1 13111 |
. . . . . . . 8
โข ((1
โ โ โง (โโ๐ด) โ โ) โ 1 โค if(1 โค
(โโ๐ด),
(โโ๐ด),
1)) |
16 | 9, 8, 15 | sylancr 588 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 1 โค if(1 โค (โโ๐ด), (โโ๐ด), 1)) |
17 | 3, 12, 11, 14, 16 | ltletrd 11322 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+)
โ 0 < if(1 โค (โโ๐ด), (โโ๐ด), 1)) |
18 | 11, 17 | elrpd 12961 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+)
โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ
โ+) |
19 | 6, 18 | rpdivcld 12981 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ต / if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ+) |
20 | | cxploglim 26343 |
. . . 4
โข ((๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)) โ
โ+ โ (๐ โ โ+ โฆ
((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))))
โ๐ 0) |
21 | 19, 20 | syl 17 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ โ
โ+ โฆ ((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))) โ๐
0) |
22 | 5, 21, 18 | rlimcxp 26339 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ โ
โ+ โฆ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)))
โ๐ 0) |
23 | 5, 21 | rlimmptrcl 15497 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ ((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))) โ โ) |
24 | 11 | adantr 482 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ โ) |
25 | 24 | recnd 11190 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ โ) |
26 | 23, 25 | cxpcld 26079 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ) |
27 | | relogcl 25947 |
. . . . . 6
โข (๐ โ โ+
โ (logโ๐) โ
โ) |
28 | 27 | adantl 483 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (logโ๐) โ โ) |
29 | 28 | recnd 11190 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (logโ๐) โ โ) |
30 | | simpll 766 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ ๐ด โ โ) |
31 | 29, 30 | cxpcld 26079 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ ((logโ๐)โ๐๐ด) โ โ) |
32 | | simpr 486 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ ๐ โ โ+) |
33 | | rpre 12930 |
. . . . . 6
โข (๐ต โ โ+
โ ๐ต โ
โ) |
34 | 33 | ad2antlr 726 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ ๐ต โ โ) |
35 | 32, 34 | rpcxpcld 26103 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (๐โ๐๐ต) โ
โ+) |
36 | 35 | rpcnd 12966 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (๐โ๐๐ต) โ โ) |
37 | 35 | rpne0d 12969 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (๐โ๐๐ต) โ 0) |
38 | 31, 36, 37 | divcld 11938 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (((logโ๐)โ๐๐ด) / (๐โ๐๐ต)) โ โ) |
39 | 38 | adantrr 716 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐)โ๐๐ด) / (๐โ๐๐ต)) โ โ) |
40 | 39 | abscld 15328 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) โ โ) |
41 | | rpre 12930 |
. . . . . . . . 9
โข (๐ โ โ+
โ ๐ โ
โ) |
42 | 41 | ad2antrl 727 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ๐ โ โ) |
43 | 9 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ 1 โ โ) |
44 | 1 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ 3 โ โ) |
45 | | 1lt3 12333 |
. . . . . . . . . 10
โข 1 <
3 |
46 | 45 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ 1 < 3) |
47 | | simprr 772 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ 3 โค ๐) |
48 | 43, 44, 42, 46, 47 | ltletrd 11322 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ 1 < ๐) |
49 | 42, 48 | rplogcld 26000 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (logโ๐) โ
โ+) |
50 | 32 | adantrr 716 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ๐ โ โ+) |
51 | 33 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ๐ต โ โ) |
52 | 18 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ
โ+) |
53 | 51, 52 | rerpdivcld 12995 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)) โ โ) |
54 | 50, 53 | rpcxpcld 26103 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))) โ
โ+) |
55 | 49, 54 | rpdivcld 12981 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))) โ
โ+) |
56 | 11 | adantr 482 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ
โ) |
57 | 55, 56 | rpcxpcld 26103 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ+) |
58 | 57 | rpred 12964 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ) |
59 | 26 | adantrr 716 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ) |
60 | 59 | abscld 15328 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)))
โ โ) |
61 | 31 | adantrr 716 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((logโ๐)โ๐๐ด) โ โ) |
62 | 61 | abscld 15328 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ((logโ๐)โ๐๐ด)) โ
โ) |
63 | 49, 56 | rpcxpcld 26103 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ+) |
64 | 63 | rpred 12964 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ โ) |
65 | 35 | adantrr 716 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (๐โ๐๐ต) โ
โ+) |
66 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ๐ด โ โ) |
67 | | abscxp 26063 |
. . . . . . . 8
โข
(((logโ๐)
โ โ+ โง ๐ด โ โ) โ
(absโ((logโ๐)โ๐๐ด)) = ((logโ๐)โ๐(โโ๐ด))) |
68 | 49, 66, 67 | syl2anc 585 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ((logโ๐)โ๐๐ด)) = ((logโ๐)โ๐(โโ๐ด))) |
69 | 66 | recld 15086 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (โโ๐ด) โ โ) |
70 | | max2 13113 |
. . . . . . . . 9
โข ((1
โ โ โง (โโ๐ด) โ โ) โ (โโ๐ด) โค if(1 โค
(โโ๐ด),
(โโ๐ด),
1)) |
71 | 9, 69, 70 | sylancr 588 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (โโ๐ด) โค if(1 โค (โโ๐ด), (โโ๐ด), 1)) |
72 | 27 | ad2antrl 727 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (logโ๐) โ โ) |
73 | | loge 25958 |
. . . . . . . . . 10
โข
(logโe) = 1 |
74 | | ere 15978 |
. . . . . . . . . . . . 13
โข e โ
โ |
75 | 74 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ e โ โ) |
76 | | egt2lt3 16095 |
. . . . . . . . . . . . . 14
โข (2 < e
โง e < 3) |
77 | 76 | simpri 487 |
. . . . . . . . . . . . 13
โข e <
3 |
78 | 77 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ e < 3) |
79 | 75, 44, 42, 78, 47 | ltletrd 11322 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ e < ๐) |
80 | | epr 16097 |
. . . . . . . . . . . 12
โข e โ
โ+ |
81 | | logltb 25971 |
. . . . . . . . . . . 12
โข ((e
โ โ+ โง ๐ โ โ+) โ (e <
๐ โ (logโe) <
(logโ๐))) |
82 | 80, 50, 81 | sylancr 588 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (e < ๐ โ (logโe) < (logโ๐))) |
83 | 79, 82 | mpbid 231 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (logโe) < (logโ๐)) |
84 | 73, 83 | eqbrtrrid 5146 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ 1 < (logโ๐)) |
85 | 72, 84, 69, 56 | cxpled 26091 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((โโ๐ด) โค if(1 โค (โโ๐ด), (โโ๐ด), 1) โ ((logโ๐)โ๐(โโ๐ด)) โค ((logโ๐)โ๐if(1
โค (โโ๐ด),
(โโ๐ด),
1)))) |
86 | 71, 85 | mpbid 231 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((logโ๐)โ๐(โโ๐ด)) โค ((logโ๐)โ๐if(1
โค (โโ๐ด),
(โโ๐ด),
1))) |
87 | 68, 86 | eqbrtrd 5132 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ((logโ๐)โ๐๐ด)) โค ((logโ๐)โ๐if(1
โค (โโ๐ด),
(โโ๐ด),
1))) |
88 | 62, 64, 65, 87 | lediv1dd 13022 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((absโ((logโ๐)โ๐๐ด)) / (๐โ๐๐ต)) โค (((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) /
(๐โ๐๐ต))) |
89 | 31, 36, 37 | absdivd 15347 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง ๐ โ
โ+) โ (absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) = ((absโ((logโ๐)โ๐๐ด)) / (absโ(๐โ๐๐ต)))) |
90 | 89 | adantrr 716 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) = ((absโ((logโ๐)โ๐๐ด)) / (absโ(๐โ๐๐ต)))) |
91 | 65 | rprege0d 12971 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((๐โ๐๐ต) โ โ โง 0 โค (๐โ๐๐ต))) |
92 | | absid 15188 |
. . . . . . . 8
โข (((๐โ๐๐ต) โ โ โง 0 โค
(๐โ๐๐ต)) โ (absโ(๐โ๐๐ต)) = (๐โ๐๐ต)) |
93 | 91, 92 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(๐โ๐๐ต)) = (๐โ๐๐ต)) |
94 | 93 | oveq2d 7378 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((absโ((logโ๐)โ๐๐ด)) / (absโ(๐โ๐๐ต))) =
((absโ((logโ๐)โ๐๐ด)) / (๐โ๐๐ต))) |
95 | 90, 94 | eqtrd 2777 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) = ((absโ((logโ๐)โ๐๐ด)) / (๐โ๐๐ต))) |
96 | 49 | rprege0d 12971 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((logโ๐) โ โ โง 0 โค
(logโ๐))) |
97 | 11 | recnd 11190 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+)
โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ โ) |
98 | 97 | adantr 482 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ
โ) |
99 | | divcxp 26058 |
. . . . . . 7
โข
((((logโ๐)
โ โ โง 0 โค (logโ๐)) โง (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))) โ โ+ โง
if(1 โค (โโ๐ด),
(โโ๐ด), 1) โ
โ) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) =
(((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) /
((๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1)))) |
100 | 96, 54, 98, 99 | syl3anc 1372 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) =
(((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) /
((๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1)))) |
101 | 50, 53, 98 | cxpmuld 26107 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (๐โ๐((๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)) ยท if(1 โค
(โโ๐ด),
(โโ๐ด), 1))) =
((๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1))) |
102 | 51 | recnd 11190 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ๐ต โ โ) |
103 | 52 | rpne0d 12969 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ if(1 โค (โโ๐ด), (โโ๐ด), 1) โ 0) |
104 | 102, 98, 103 | divcan1d 11939 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)) ยท if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) =
๐ต) |
105 | 104 | oveq2d 7378 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (๐โ๐((๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)) ยท if(1 โค
(โโ๐ด),
(โโ๐ด), 1))) =
(๐โ๐๐ต)) |
106 | 101, 105 | eqtr3d 2779 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) =
(๐โ๐๐ต)) |
107 | 106 | oveq2d 7378 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) /
((๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1)))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))) =
(((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) /
(๐โ๐๐ต))) |
108 | 100, 107 | eqtrd 2777 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) =
(((logโ๐)โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) /
(๐โ๐๐ต))) |
109 | 88, 95, 108 | 3brtr4d 5142 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) โค (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1))) |
110 | 58 | leabsd 15306 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1)) โค
(absโ(((logโ๐)
/ (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1)))) |
111 | 40, 58, 60, 109, 110 | letrd 11319 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) โค (absโ(((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1)))) |
112 | 39 | subid1d 11508 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((((logโ๐)โ๐๐ด) / (๐โ๐๐ต)) โ 0) = (((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) |
113 | 112 | fveq2d 6851 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ((((logโ๐)โ๐๐ด) / (๐โ๐๐ต)) โ 0)) =
(absโ(((logโ๐)โ๐๐ด) / (๐โ๐๐ต)))) |
114 | 59 | subid1d 11508 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ ((((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ 0) = (((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1))) |
115 | 114 | fveq2d 6851 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ((((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ 0)) = (absโ(((logโ๐) / (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด),
1)))) |
116 | 111, 113,
115 | 3brtr4d 5142 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ
โ+ โง 3 โค ๐)) โ (absโ((((logโ๐)โ๐๐ด) / (๐โ๐๐ต)) โ 0)) โค
(absโ((((logโ๐)
/ (๐โ๐(๐ต / if(1 โค (โโ๐ด), (โโ๐ด), 1))))โ๐if(1 โค
(โโ๐ด),
(โโ๐ด), 1))
โ 0))) |
117 | 2, 4, 22, 26, 38, 116 | rlimsqzlem 15540 |
1
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ โ
โ+ โฆ (((logโ๐)โ๐๐ด) / (๐โ๐๐ต))) โ๐
0) |