This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = i π$

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