Step |
Hyp |
Ref |
Expression |
1 |
|
logcn.d |
โข ๐ท = ( โ โ ( -โ (,] 0 ) ) |
2 |
|
logcnlem.s |
โข ๐ = if ( ๐ด โ โ+ , ๐ด , ( abs โ ( โ โ ๐ด ) ) ) |
3 |
|
logcnlem.t |
โข ๐ = ( ( abs โ ๐ด ) ยท ( ๐
/ ( 1 + ๐
) ) ) |
4 |
|
logcnlem.a |
โข ( ๐ โ ๐ด โ ๐ท ) |
5 |
|
logcnlem.r |
โข ( ๐ โ ๐
โ โ+ ) |
6 |
|
simpr |
โข ( ( ๐ โง ๐ด โ โ+ ) โ ๐ด โ โ+ ) |
7 |
1
|
ellogdm |
โข ( ๐ด โ ๐ท โ ( ๐ด โ โ โง ( ๐ด โ โ โ ๐ด โ โ+ ) ) ) |
8 |
7
|
simplbi |
โข ( ๐ด โ ๐ท โ ๐ด โ โ ) |
9 |
4 8
|
syl |
โข ( ๐ โ ๐ด โ โ ) |
10 |
9
|
imcld |
โข ( ๐ โ ( โ โ ๐ด ) โ โ ) |
11 |
10
|
adantr |
โข ( ( ๐ โง ยฌ ๐ด โ โ+ ) โ ( โ โ ๐ด ) โ โ ) |
12 |
11
|
recnd |
โข ( ( ๐ โง ยฌ ๐ด โ โ+ ) โ ( โ โ ๐ด ) โ โ ) |
13 |
|
reim0b |
โข ( ๐ด โ โ โ ( ๐ด โ โ โ ( โ โ ๐ด ) = 0 ) ) |
14 |
9 13
|
syl |
โข ( ๐ โ ( ๐ด โ โ โ ( โ โ ๐ด ) = 0 ) ) |
15 |
7
|
simprbi |
โข ( ๐ด โ ๐ท โ ( ๐ด โ โ โ ๐ด โ โ+ ) ) |
16 |
4 15
|
syl |
โข ( ๐ โ ( ๐ด โ โ โ ๐ด โ โ+ ) ) |
17 |
14 16
|
sylbird |
โข ( ๐ โ ( ( โ โ ๐ด ) = 0 โ ๐ด โ โ+ ) ) |
18 |
17
|
necon3bd |
โข ( ๐ โ ( ยฌ ๐ด โ โ+ โ ( โ โ ๐ด ) โ 0 ) ) |
19 |
18
|
imp |
โข ( ( ๐ โง ยฌ ๐ด โ โ+ ) โ ( โ โ ๐ด ) โ 0 ) |
20 |
12 19
|
absrpcld |
โข ( ( ๐ โง ยฌ ๐ด โ โ+ ) โ ( abs โ ( โ โ ๐ด ) ) โ โ+ ) |
21 |
6 20
|
ifclda |
โข ( ๐ โ if ( ๐ด โ โ+ , ๐ด , ( abs โ ( โ โ ๐ด ) ) ) โ โ+ ) |
22 |
2 21
|
eqeltrid |
โข ( ๐ โ ๐ โ โ+ ) |
23 |
1
|
logdmn0 |
โข ( ๐ด โ ๐ท โ ๐ด โ 0 ) |
24 |
4 23
|
syl |
โข ( ๐ โ ๐ด โ 0 ) |
25 |
9 24
|
absrpcld |
โข ( ๐ โ ( abs โ ๐ด ) โ โ+ ) |
26 |
|
1rp |
โข 1 โ โ+ |
27 |
|
rpaddcl |
โข ( ( 1 โ โ+ โง ๐
โ โ+ ) โ ( 1 + ๐
) โ โ+ ) |
28 |
26 5 27
|
sylancr |
โข ( ๐ โ ( 1 + ๐
) โ โ+ ) |
29 |
5 28
|
rpdivcld |
โข ( ๐ โ ( ๐
/ ( 1 + ๐
) ) โ โ+ ) |
30 |
25 29
|
rpmulcld |
โข ( ๐ โ ( ( abs โ ๐ด ) ยท ( ๐
/ ( 1 + ๐
) ) ) โ โ+ ) |
31 |
3 30
|
eqeltrid |
โข ( ๐ โ ๐ โ โ+ ) |
32 |
22 31
|
ifcld |
โข ( ๐ โ if ( ๐ โค ๐ , ๐ , ๐ ) โ โ+ ) |