Theorem iexpire

Description: _i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020)

	Ref	Expression
Assertion	iexpire	$$⊢{\mathrm{i}}^{\mathrm{i}}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		ine0	$$⊢\mathrm{i}\ne 0$$
3		cxpef	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge \mathrm{i}\in ℂ\right)\to {\mathrm{i}}^{\mathrm{i}}={\mathrm{e}}^{\mathrm{i}\log \mathrm{i}}$$
4	1 2 1 3	mp3an	$$⊢{\mathrm{i}}^{\mathrm{i}}={\mathrm{e}}^{\mathrm{i}\log \mathrm{i}}$$
5		logi	$$⊢\log \mathrm{i}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
6	5	oveq2i	$$⊢\mathrm{i}\log \mathrm{i}=\mathrm{i}\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
7		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
8	7	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
9	1 1 8	mulassi	$$⊢\mathrm{i}\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{i}\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
10		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
11	10	oveq1i	$$⊢\mathrm{i}\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)=-1\left(\frac{\mathrm{\pi }}{2}\right)$$
12	6 9 11	3eqtr2i	$$⊢\mathrm{i}\log \mathrm{i}=-1\left(\frac{\mathrm{\pi }}{2}\right)$$
13	12	fveq2i	$$⊢{\mathrm{e}}^{\mathrm{i}\log \mathrm{i}}={\mathrm{e}}^{-1\left(\frac{\mathrm{\pi }}{2}\right)}$$
14	4 13	eqtri	$$⊢{\mathrm{i}}^{\mathrm{i}}={\mathrm{e}}^{-1\left(\frac{\mathrm{\pi }}{2}\right)}$$
15		neg1rr	$$⊢-1\in ℝ$$
16	15 7	remulcli	$$⊢-1\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ$$
17		reefcl	$$⊢-1\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ\to {\mathrm{e}}^{-1\left(\frac{\mathrm{\pi }}{2}\right)}\in ℝ$$
18	16 17	ax-mp	$$⊢{\mathrm{e}}^{-1\left(\frac{\mathrm{\pi }}{2}\right)}\in ℝ$$
19	14 18	eqeltri	$$⊢{\mathrm{i}}^{\mathrm{i}}\in ℝ$$