# Real Natural Logarithm Function is Continuous

## Proof 1

We have that the Natural Logarithm Function is Differentiable.

The result follows from Differentiable Function is Continuous.

$\blacksquare$

## Proof 2

$\dfrac 1 2 < \map \ln 2 < 1$

Fix $x \in \R$.

Consider $\dfrac x {\map \ln 2}$.

$\forall \epsilon \in \R_{>0} \exists r \in \Q : \size {r - \dfrac x {\map \ln 2} } < \epsilon$

Thus:

 $\ds \size {r - \dfrac x {\map \ln 2} }$ $<$ $\ds \epsilon$ $\ds \leadsto \ \$ $\ds \map \ln 2 \size {r - \dfrac x {\map \ln 2} }$ $=$ $\ds \size {\map \ln {2^r} - x }$ Natural Logarithm of Rational Power $\ds$ $<$ $\ds \epsilon \, \map \ln 2$ Real Number Ordering is Compatible with Multiplication $\ds$ $<$ $\ds \epsilon$ as $\map \ln 2 < 1$ $\ds \leadsto \ \$ $\ds \size {\map \ln t - x}$ $<$ $\ds \epsilon$ substituting $t = 2^r$

Thus:

$\forall \epsilon \in \R_{>0}: \exists t \in \R_{>0}: \size {\map \ln t - x} < \epsilon$

Thus, the image of $\R_{>0}$ under $\ln$ is everywhere dense in $\R$.

From Monotone Real Function with Everywhere Dense Image is Continuous, $\ln$ is continuous on $\R_{>0}$.

Hence the result.

$\blacksquare$
{"ft_lang_label":"__label__en","ft_lang_prob":0.6508106,"math_prob":1.0000073,"size":1380,"snap":"2023-14-2023-23","text_gpt3_token_len":480,"char_repetition_ratio":0.17659883,"word_repetition_ratio":0.08510638,"special_character_ratio":0.3905797,"punctuation_ratio":0.07826087,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":1.0000085,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2023-03-31T06:50:01Z\",\"WARC-Record-ID\":\"<urn:uuid:4640e98a-d443-4bba-80d4-fc2f3ff7bafa>\",\"Content-Length\":\"42585\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:45b5c8ab-8797-4a8d-a414-e9be644a954b>\",\"WARC-Concurrent-To\":\"<urn:uuid:a8ed68fd-1b54-44f8-985e-c0e7a6b8a36a>\",\"WARC-IP-Address\":\"172.67.198.93\",\"WARC-Target-URI\":\"https://proofwiki.org/wiki/Real_Natural_Logarithm_Function_is_Continuous\",\"WARC-Payload-Digest\":\"sha1:IMFPXJJ2IFFV4XX7CAPJ4ZR5F5DUBZE3\",\"WARC-Block-Digest\":\"sha1:Q23IJ2YRLMATDHQEIZOWN2BEACDKTYKY\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2023/CC-MAIN-2023-14/CC-MAIN-2023-14_segments_1679296949573.84_warc_CC-MAIN-20230331051439-20230331081439-00260.warc.gz\"}"}