Theorem logm1

Description: The natural logarithm of negative 1 . (Contributed by Paul Chapman, 21-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

	Ref	Expression
Assertion	logm1	$$⊢\log -1=\mathrm{i}\mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		1rp	$$⊢1\in {ℝ}^{+}$$
2		logneg	$$⊢1\in {ℝ}^{+}\to \log -1=\log 1+\mathrm{i}\mathrm{\pi }$$
3	1 2	ax-mp	$$⊢\log -1=\log 1+\mathrm{i}\mathrm{\pi }$$
4		log1	$$⊢\log 1=0$$
5	4	oveq1i	$$⊢\log 1+\mathrm{i}\mathrm{\pi }=0+\mathrm{i}\mathrm{\pi }$$
6		ax-icn	$$⊢\mathrm{i}\in ℂ$$
7		picn	$$⊢\mathrm{\pi }\in ℂ$$
8	6 7	mulcli	$$⊢\mathrm{i}\mathrm{\pi }\in ℂ$$
9	8	addlidi	$$⊢0+\mathrm{i}\mathrm{\pi }=\mathrm{i}\mathrm{\pi }$$
10	3 5 9	3eqtri	$$⊢\log -1=\mathrm{i}\mathrm{\pi }$$