Theorem log1

Description: The natural logarithm of 1 . One case of Property 1a of Cohen p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007)

	Ref	Expression
Assertion	log1	$$⊢\log 1=0$$

Proof

Step	Hyp	Ref	Expression
1		ef0	$$⊢{\mathrm{e}}^0=1$$
2		1rp	$$⊢1\in {ℝ}^{+}$$
3		0re	$$⊢0\in ℝ$$
4		relogeftb	$$⊢\left(1\in {ℝ}^{+}\wedge 0\in ℝ\right)\to \left(\log 1=0\leftrightarrow {\mathrm{e}}^0=1\right)$$
5	2 3 4	mp2an	$$⊢\log 1=0\leftrightarrow {\mathrm{e}}^0=1$$
6	1 5	mpbir	$$⊢\log 1=0$$