Theorem logi

Description: The natural logarithm of _i . (Contributed by Scott Fenton, 13-Apr-2020)

	Ref	Expression
Assertion	logi	$$⊢\log \mathrm{i}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		efhalfpi	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		ine0	$$⊢\mathrm{i}\ne 0$$
4		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
5	4	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
6	2 5	mulcli	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
7		pipos	$$⊢0<\mathrm{\pi }$$
8		pire	$$⊢\mathrm{\pi }\in ℝ$$
9		lt0neg2	$$⊢\mathrm{\pi }\in ℝ\to \left(0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0\right)$$
10	8 9	ax-mp	$$⊢0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0$$
11	7 10	mpbi	$$⊢-\mathrm{\pi }<0$$
12		halfpos2	$$⊢\mathrm{\pi }\in ℝ\to \left(0<\mathrm{\pi }\leftrightarrow 0<\frac{\mathrm{\pi }}{2}\right)$$
13	8 12	ax-mp	$$⊢0<\mathrm{\pi }\leftrightarrow 0<\frac{\mathrm{\pi }}{2}$$
14	7 13	mpbi	$$⊢0<\frac{\mathrm{\pi }}{2}$$
15	8	renegcli	$$⊢-\mathrm{\pi }\in ℝ$$
16		0re	$$⊢0\in ℝ$$
17	15 16 4	lttri	$$⊢\left(-\mathrm{\pi }<0\wedge 0<\frac{\mathrm{\pi }}{2}\right)\to -\mathrm{\pi }<\frac{\mathrm{\pi }}{2}$$
18	11 14 17	mp2an	$$⊢-\mathrm{\pi }<\frac{\mathrm{\pi }}{2}$$
19		reim	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to \Re \left(\frac{\mathrm{\pi }}{2}\right)=\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)$$
20	5 19	ax-mp	$$⊢\Re \left(\frac{\mathrm{\pi }}{2}\right)=\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)$$
21		rere	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \Re \left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
22	4 21	ax-mp	$$⊢\Re \left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
23	20 22	eqtr3i	$$⊢\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)=\frac{\mathrm{\pi }}{2}$$
24	18 23	breqtrri	$$⊢-\mathrm{\pi }<\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)$$
25	8	a1i	$$⊢\top \to \mathrm{\pi }\in ℝ$$
26	25 25	ltaddposd	$$⊢\top \to \left(0<\mathrm{\pi }\leftrightarrow \mathrm{\pi }<\mathrm{\pi }+\mathrm{\pi }\right)$$
27	7 26	mpbii	$$⊢\top \to \mathrm{\pi }<\mathrm{\pi }+\mathrm{\pi }$$
28		picn	$$⊢\mathrm{\pi }\in ℂ$$
29	28	times2i	$$⊢\mathrm{\pi }\cdot 2=\mathrm{\pi }+\mathrm{\pi }$$
30	27 29	breqtrrdi	$$⊢\top \to \mathrm{\pi }<\mathrm{\pi }\cdot 2$$
31		2rp	$$⊢2\in {ℝ}^{+}$$
32	31	a1i	$$⊢\top \to 2\in {ℝ}^{+}$$
33	25 25 32	ltdivmul2d	$$⊢\top \to \left(\frac{\mathrm{\pi }}{2}<\mathrm{\pi }\leftrightarrow \mathrm{\pi }<\mathrm{\pi }\cdot 2\right)$$
34	30 33	mpbird	$$⊢\top \to \frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
35	34	mptru	$$⊢\frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
36	4 8 35	ltleii	$$⊢\frac{\mathrm{\pi }}{2}\le \mathrm{\pi }$$
37	23 36	eqbrtri	$$⊢\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)\le \mathrm{\pi }$$
38		ellogrn	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in \mathrm{ran}log\leftrightarrow \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ\wedge -\mathrm{\pi }<\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge \Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)\le \mathrm{\pi }\right)$$
39	6 24 37 38	mpbir3an	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in \mathrm{ran}log$$
40		logeftb	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge \mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in \mathrm{ran}log\right)\to \left(\log \mathrm{i}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\leftrightarrow {\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}\right)$$
41	2 3 39 40	mp3an	$$⊢\log \mathrm{i}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\leftrightarrow {\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}$$
42	1 41	mpbir	$$⊢\log \mathrm{i}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$