Step | Hyp | Ref
| Expression |
1 | | 1red 11212 |
. . 3
โข (โค
โ 1 โ โ) |
2 | | 1cnd 11206 |
. . 3
โข (โค
โ 1 โ โ) |
3 | | relogcl 26426 |
. . . . . . . . 9
โข (๐ฅ โ โ+
โ (logโ๐ฅ) โ
โ) |
4 | 3 | adantl 481 |
. . . . . . . 8
โข
((โค โง ๐ฅ
โ โ+) โ (logโ๐ฅ) โ โ) |
5 | 4 | recnd 11239 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ โ+) โ (logโ๐ฅ) โ โ) |
6 | | 1cnd 11206 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ โ+) โ 1 โ โ) |
7 | | rpcnne0 12989 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (๐ฅ โ โ
โง ๐ฅ โ
0)) |
8 | 7 | adantl 481 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ โ+) โ (๐ฅ โ โ โง ๐ฅ โ 0)) |
9 | | divdir 11894 |
. . . . . . 7
โข
(((logโ๐ฅ)
โ โ โง 1 โ โ โง (๐ฅ โ โ โง ๐ฅ โ 0)) โ (((logโ๐ฅ) + 1) / ๐ฅ) = (((logโ๐ฅ) / ๐ฅ) + (1 / ๐ฅ))) |
10 | 5, 6, 8, 9 | syl3anc 1368 |
. . . . . 6
โข
((โค โง ๐ฅ
โ โ+) โ (((logโ๐ฅ) + 1) / ๐ฅ) = (((logโ๐ฅ) / ๐ฅ) + (1 / ๐ฅ))) |
11 | 10 | mpteq2dva 5238 |
. . . . 5
โข (โค
โ (๐ฅ โ
โ+ โฆ (((logโ๐ฅ) + 1) / ๐ฅ)) = (๐ฅ โ โ+ โฆ
(((logโ๐ฅ) / ๐ฅ) + (1 / ๐ฅ)))) |
12 | | simpr 484 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ โ+) โ ๐ฅ โ โ+) |
13 | 4, 12 | rerpdivcld 13044 |
. . . . . 6
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ๐ฅ) / ๐ฅ) โ โ) |
14 | | rpreccl 12997 |
. . . . . . . 8
โข (๐ฅ โ โ+
โ (1 / ๐ฅ) โ
โ+) |
15 | 14 | adantl 481 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ โ+) โ (1 / ๐ฅ) โ
โ+) |
16 | 15 | rpred 13013 |
. . . . . 6
โข
((โค โง ๐ฅ
โ โ+) โ (1 / ๐ฅ) โ โ) |
17 | 8 | simpld 494 |
. . . . . . . . . 10
โข
((โค โง ๐ฅ
โ โ+) โ ๐ฅ โ โ) |
18 | 17 | cxp1d 26556 |
. . . . . . . . 9
โข
((โค โง ๐ฅ
โ โ+) โ (๐ฅโ๐1) = ๐ฅ) |
19 | 18 | oveq2d 7417 |
. . . . . . . 8
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ๐ฅ) / (๐ฅโ๐1)) =
((logโ๐ฅ) / ๐ฅ)) |
20 | 19 | mpteq2dva 5238 |
. . . . . . 7
โข (โค
โ (๐ฅ โ
โ+ โฆ ((logโ๐ฅ) / (๐ฅโ๐1))) = (๐ฅ โ โ+
โฆ ((logโ๐ฅ) /
๐ฅ))) |
21 | | 1rp 12975 |
. . . . . . . 8
โข 1 โ
โ+ |
22 | | cxploglim 26826 |
. . . . . . . 8
โข (1 โ
โ+ โ (๐ฅ โ โ+ โฆ
((logโ๐ฅ) / (๐ฅโ๐1)))
โ๐ 0) |
23 | 21, 22 | mp1i 13 |
. . . . . . 7
โข (โค
โ (๐ฅ โ
โ+ โฆ ((logโ๐ฅ) / (๐ฅโ๐1)))
โ๐ 0) |
24 | 20, 23 | eqbrtrrd 5162 |
. . . . . 6
โข (โค
โ (๐ฅ โ
โ+ โฆ ((logโ๐ฅ) / ๐ฅ)) โ๐
0) |
25 | | ax-1cn 11164 |
. . . . . . 7
โข 1 โ
โ |
26 | | divrcnv 15795 |
. . . . . . 7
โข (1 โ
โ โ (๐ฅ โ
โ+ โฆ (1 / ๐ฅ)) โ๐
0) |
27 | 25, 26 | mp1i 13 |
. . . . . 6
โข (โค
โ (๐ฅ โ
โ+ โฆ (1 / ๐ฅ)) โ๐
0) |
28 | 13, 16, 24, 27 | rlimadd 15584 |
. . . . 5
โข (โค
โ (๐ฅ โ
โ+ โฆ (((logโ๐ฅ) / ๐ฅ) + (1 / ๐ฅ))) โ๐ (0 +
0)) |
29 | 11, 28 | eqbrtrd 5160 |
. . . 4
โข (โค
โ (๐ฅ โ
โ+ โฆ (((logโ๐ฅ) + 1) / ๐ฅ)) โ๐ (0 +
0)) |
30 | | 00id 11386 |
. . . 4
โข (0 + 0) =
0 |
31 | 29, 30 | breqtrdi 5179 |
. . 3
โข (โค
โ (๐ฅ โ
โ+ โฆ (((logโ๐ฅ) + 1) / ๐ฅ)) โ๐
0) |
32 | | peano2re 11384 |
. . . . . 6
โข
((logโ๐ฅ)
โ โ โ ((logโ๐ฅ) + 1) โ โ) |
33 | 4, 32 | syl 17 |
. . . . 5
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ๐ฅ) + 1) โ โ) |
34 | 33, 12 | rerpdivcld 13044 |
. . . 4
โข
((โค โง ๐ฅ
โ โ+) โ (((logโ๐ฅ) + 1) / ๐ฅ) โ โ) |
35 | 34 | recnd 11239 |
. . 3
โข
((โค โง ๐ฅ
โ โ+) โ (((logโ๐ฅ) + 1) / ๐ฅ) โ โ) |
36 | | rprege0 12986 |
. . . . . . . . . 10
โข (๐ฅ โ โ+
โ (๐ฅ โ โ
โง 0 โค ๐ฅ)) |
37 | 36 | adantl 481 |
. . . . . . . . 9
โข
((โค โง ๐ฅ
โ โ+) โ (๐ฅ โ โ โง 0 โค ๐ฅ)) |
38 | | flge0nn0 13782 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง 0 โค
๐ฅ) โ
(โโ๐ฅ) โ
โ0) |
39 | | faccl 14240 |
. . . . . . . . 9
โข
((โโ๐ฅ)
โ โ0 โ (!โ(โโ๐ฅ)) โ โ) |
40 | 37, 38, 39 | 3syl 18 |
. . . . . . . 8
โข
((โค โง ๐ฅ
โ โ+) โ (!โ(โโ๐ฅ)) โ โ) |
41 | 40 | nnrpd 13011 |
. . . . . . 7
โข
((โค โง ๐ฅ
โ โ+) โ (!โ(โโ๐ฅ)) โ
โ+) |
42 | | relogcl 26426 |
. . . . . . 7
โข
((!โ(โโ๐ฅ)) โ โ+ โ
(logโ(!โ(โโ๐ฅ))) โ โ) |
43 | 41, 42 | syl 17 |
. . . . . 6
โข
((โค โง ๐ฅ
โ โ+) โ (logโ(!โ(โโ๐ฅ))) โ
โ) |
44 | 43, 12 | rerpdivcld 13044 |
. . . . 5
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ) โ โ) |
45 | 44 | recnd 11239 |
. . . 4
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ) โ โ) |
46 | 5, 45 | subcld 11568 |
. . 3
โข
((โค โง ๐ฅ
โ โ+) โ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ โ) |
47 | | logfacbnd3 27072 |
. . . . . 6
โข ((๐ฅ โ โ+
โง 1 โค ๐ฅ) โ
(absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) โค ((logโ๐ฅ) + 1)) |
48 | 47 | adantl 481 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
(absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) โค ((logโ๐ฅ) + 1)) |
49 | 43 | recnd 11239 |
. . . . . . . . 9
โข
((โค โง ๐ฅ
โ โ+) โ (logโ(!โ(โโ๐ฅ))) โ
โ) |
50 | 49 | adantrr 714 |
. . . . . . . 8
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
(logโ(!โ(โโ๐ฅ))) โ โ) |
51 | 7 | ad2antrl 725 |
. . . . . . . . . 10
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (๐ฅ โ โ โง ๐ฅ โ 0)) |
52 | 51 | simpld 494 |
. . . . . . . . 9
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ๐ฅ โ โ) |
53 | 5 | adantrr 714 |
. . . . . . . . . 10
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (logโ๐ฅ) โ โ) |
54 | | subcl 11456 |
. . . . . . . . . 10
โข
(((logโ๐ฅ)
โ โ โง 1 โ โ) โ ((logโ๐ฅ) โ 1) โ โ) |
55 | 53, 25, 54 | sylancl 585 |
. . . . . . . . 9
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((logโ๐ฅ) โ 1) โ โ) |
56 | 52, 55 | mulcld 11231 |
. . . . . . . 8
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
โ) |
57 | 50, 56 | subcld 11568 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))) โ
โ) |
58 | 57 | abscld 15380 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
(absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) โ
โ) |
59 | 4 | adantrr 714 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (logโ๐ฅ) โ โ) |
60 | 59, 32 | syl 17 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((logโ๐ฅ) + 1) โ โ) |
61 | | rpregt0 12985 |
. . . . . . 7
โข (๐ฅ โ โ+
โ (๐ฅ โ โ
โง 0 < ๐ฅ)) |
62 | 61 | ad2antrl 725 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (๐ฅ โ โ โง 0 < ๐ฅ)) |
63 | | lediv1 12076 |
. . . . . 6
โข
(((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) โ โ โง
((logโ๐ฅ) + 1) โ
โ โง (๐ฅ โ
โ โง 0 < ๐ฅ))
โ ((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) โค ((logโ๐ฅ) + 1) โ
((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) / ๐ฅ) โค (((logโ๐ฅ) + 1) / ๐ฅ))) |
64 | 58, 60, 62, 63 | syl3anc 1368 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) โค ((logโ๐ฅ) + 1) โ
((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) / ๐ฅ) โค (((logโ๐ฅ) + 1) / ๐ฅ))) |
65 | 48, 64 | mpbid 231 |
. . . 4
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) / ๐ฅ) โค (((logโ๐ฅ) + 1) / ๐ฅ)) |
66 | 51 | simprd 495 |
. . . . . . . . 9
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ๐ฅ โ 0) |
67 | 55, 52, 66 | divcan3d 11992 |
. . . . . . . 8
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((๐ฅ ยท ((logโ๐ฅ) โ 1)) / ๐ฅ) = ((logโ๐ฅ) โ 1)) |
68 | 67 | oveq1d 7416 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (((๐ฅ ยท ((logโ๐ฅ) โ 1)) / ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) = (((logโ๐ฅ) โ 1) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
69 | | divsubdir 11905 |
. . . . . . . 8
โข (((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ โ
โง (logโ(!โ(โโ๐ฅ))) โ โ โง (๐ฅ โ โ โง ๐ฅ โ 0)) โ (((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) = (((๐ฅ ยท ((logโ๐ฅ) โ 1)) / ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
70 | 56, 50, 51, 69 | syl3anc 1368 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ) = (((๐ฅ ยท ((logโ๐ฅ) โ 1)) / ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
71 | 45 | adantrr 714 |
. . . . . . . 8
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ) โ โ) |
72 | | 1cnd 11206 |
. . . . . . . 8
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ 1 โ โ) |
73 | 53, 71, 72 | sub32d 11600 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ 1) = (((logโ๐ฅ) โ 1) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) |
74 | 68, 70, 73 | 3eqtr4rd 2775 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ 1) = (((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) |
75 | 74 | fveq2d 6885 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ(((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ 1)) = (absโ(((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ))) |
76 | 56, 50 | subcld 11568 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ)))) โ โ) |
77 | 76, 52, 66 | absdivd 15399 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ(((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ)))) / ๐ฅ)) = ((absโ((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ))))) / (absโ๐ฅ))) |
78 | 56, 50 | abssubd 15397 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ))))) =
(absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1))))) |
79 | 36 | ad2antrl 725 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (๐ฅ โ โ โง 0 โค ๐ฅ)) |
80 | | absid 15240 |
. . . . . . 7
โข ((๐ฅ โ โ โง 0 โค
๐ฅ) โ (absโ๐ฅ) = ๐ฅ) |
81 | 79, 80 | syl 17 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ๐ฅ) = ๐ฅ) |
82 | 78, 81 | oveq12d 7419 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((absโ((๐ฅ ยท ((logโ๐ฅ) โ 1)) โ
(logโ(!โ(โโ๐ฅ))))) / (absโ๐ฅ)) =
((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) / ๐ฅ)) |
83 | 75, 77, 82 | 3eqtrd 2768 |
. . . 4
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ(((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ 1)) =
((absโ((logโ(!โ(โโ๐ฅ))) โ (๐ฅ ยท ((logโ๐ฅ) โ 1)))) / ๐ฅ)) |
84 | 35 | adantrr 714 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (((logโ๐ฅ) + 1) / ๐ฅ) โ โ) |
85 | 84 | subid1d 11557 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((((logโ๐ฅ) + 1) / ๐ฅ) โ 0) = (((logโ๐ฅ) + 1) / ๐ฅ)) |
86 | 85 | fveq2d 6885 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ((((logโ๐ฅ) + 1) / ๐ฅ) โ 0)) = (absโ(((logโ๐ฅ) + 1) / ๐ฅ))) |
87 | | log1 26436 |
. . . . . . . . 9
โข
(logโ1) = 0 |
88 | | simprr 770 |
. . . . . . . . . 10
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ 1 โค ๐ฅ) |
89 | 12 | adantrr 714 |
. . . . . . . . . . 11
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ๐ฅ โ โ+) |
90 | | logleb 26453 |
. . . . . . . . . . 11
โข ((1
โ โ+ โง ๐ฅ โ โ+) โ (1 โค
๐ฅ โ (logโ1) โค
(logโ๐ฅ))) |
91 | 21, 89, 90 | sylancr 586 |
. . . . . . . . . 10
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (1 โค ๐ฅ โ (logโ1) โค (logโ๐ฅ))) |
92 | 88, 91 | mpbid 231 |
. . . . . . . . 9
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (logโ1) โค (logโ๐ฅ)) |
93 | 87, 92 | eqbrtrrid 5174 |
. . . . . . . 8
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ 0 โค (logโ๐ฅ)) |
94 | 59, 93 | ge0p1rpd 13043 |
. . . . . . 7
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ ((logโ๐ฅ) + 1) โ
โ+) |
95 | 94, 89 | rpdivcld 13030 |
. . . . . 6
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (((logโ๐ฅ) + 1) / ๐ฅ) โ
โ+) |
96 | | rprege0 12986 |
. . . . . 6
โข
((((logโ๐ฅ) +
1) / ๐ฅ) โ
โ+ โ ((((logโ๐ฅ) + 1) / ๐ฅ) โ โ โง 0 โค
(((logโ๐ฅ) + 1) /
๐ฅ))) |
97 | | absid 15240 |
. . . . . 6
โข
(((((logโ๐ฅ) +
1) / ๐ฅ) โ โ
โง 0 โค (((logโ๐ฅ) + 1) / ๐ฅ)) โ (absโ(((logโ๐ฅ) + 1) / ๐ฅ)) = (((logโ๐ฅ) + 1) / ๐ฅ)) |
98 | 95, 96, 97 | 3syl 18 |
. . . . 5
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ(((logโ๐ฅ) + 1) / ๐ฅ)) = (((logโ๐ฅ) + 1) / ๐ฅ)) |
99 | 86, 98 | eqtrd 2764 |
. . . 4
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ((((logโ๐ฅ) + 1) / ๐ฅ) โ 0)) = (((logโ๐ฅ) + 1) / ๐ฅ)) |
100 | 65, 83, 99 | 3brtr4d 5170 |
. . 3
โข
((โค โง (๐ฅ
โ โ+ โง 1 โค ๐ฅ)) โ (absโ(((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ)) โ 1)) โค
(absโ((((logโ๐ฅ)
+ 1) / ๐ฅ) โ
0))) |
101 | 1, 2, 31, 35, 46, 100 | rlimsqzlem 15592 |
. 2
โข (โค
โ (๐ฅ โ
โ+ โฆ ((logโ๐ฅ) โ
((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ๐
1) |
102 | 101 | mptru 1540 |
1
โข (๐ฅ โ โ+
โฆ ((logโ๐ฅ)
โ ((logโ(!โ(โโ๐ฅ))) / ๐ฅ))) โ๐
1 |