The derivative of the logarithm is the reciprocal:
( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )