Step |
Hyp |
Ref |
Expression |
1 |
|
relogcl |
โข ( ๐ด โ โ+ โ ( log โ ๐ด ) โ โ ) |
2 |
1
|
recnd |
โข ( ๐ด โ โ+ โ ( log โ ๐ด ) โ โ ) |
3 |
|
efexp |
โข ( ( ( log โ ๐ด ) โ โ โง ๐ โ โค ) โ ( exp โ ( ๐ ยท ( log โ ๐ด ) ) ) = ( ( exp โ ( log โ ๐ด ) ) โ ๐ ) ) |
4 |
2 3
|
sylan |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ( exp โ ( ๐ ยท ( log โ ๐ด ) ) ) = ( ( exp โ ( log โ ๐ด ) ) โ ๐ ) ) |
5 |
|
reeflog |
โข ( ๐ด โ โ+ โ ( exp โ ( log โ ๐ด ) ) = ๐ด ) |
6 |
5
|
oveq1d |
โข ( ๐ด โ โ+ โ ( ( exp โ ( log โ ๐ด ) ) โ ๐ ) = ( ๐ด โ ๐ ) ) |
7 |
6
|
adantr |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ( ( exp โ ( log โ ๐ด ) ) โ ๐ ) = ( ๐ด โ ๐ ) ) |
8 |
4 7
|
eqtr2d |
โข ( ( ๐ด โ โ+ โง ๐ โ โค ) โ ( ๐ด โ ๐ ) = ( exp โ ( ๐ ยท ( log โ ๐ด ) ) ) ) |