Theorem iexpire

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

	Ref	Expression
Assertion	iexpire	⊢ ( i ↑𝑐 i ) ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		ine0	⊢ i ≠ 0
3		cxpef	⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ i ∈ ℂ ) → ( i ↑𝑐 i ) = ( exp ‘ ( i · ( log ‘ i ) ) ) )
4	1 2 1 3	mp3an	⊢ ( i ↑𝑐 i ) = ( exp ‘ ( i · ( log ‘ i ) ) )
5		logi	⊢ ( log ‘ i ) = ( i · ( π / 2 ) )
6	5	oveq2i	⊢ ( i · ( log ‘ i ) ) = ( i · ( i · ( π / 2 ) ) )
7		halfpire	⊢ ( π / 2 ) ∈ ℝ
8	7	recni	⊢ ( π / 2 ) ∈ ℂ
9	1 1 8	mulassi	⊢ ( ( i · i ) · ( π / 2 ) ) = ( i · ( i · ( π / 2 ) ) )
10		ixi	⊢ ( i · i ) = - 1
11	10	oveq1i	⊢ ( ( i · i ) · ( π / 2 ) ) = ( - 1 · ( π / 2 ) )
12	6 9 11	3eqtr2i	⊢ ( i · ( log ‘ i ) ) = ( - 1 · ( π / 2 ) )
13	12	fveq2i	⊢ ( exp ‘ ( i · ( log ‘ i ) ) ) = ( exp ‘ ( - 1 · ( π / 2 ) ) )
14	4 13	eqtri	⊢ ( i ↑𝑐 i ) = ( exp ‘ ( - 1 · ( π / 2 ) ) )
15		neg1rr	⊢ - 1 ∈ ℝ
16	15 7	remulcli	⊢ ( - 1 · ( π / 2 ) ) ∈ ℝ
17		reefcl	⊢ ( ( - 1 · ( π / 2 ) ) ∈ ℝ → ( exp ‘ ( - 1 · ( π / 2 ) ) ) ∈ ℝ )
18	16 17	ax-mp	⊢ ( exp ‘ ( - 1 · ( π / 2 ) ) ) ∈ ℝ
19	14 18	eqeltri	⊢ ( i ↑𝑐 i ) ∈ ℝ