Metamath Proof Explorer


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 = e i log i
4 1 2 1 3 mp3an i i = e 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 e i log i = e -1 π 2
14 4 13 eqtri i i = e -1 π 2
15 neg1rr 1
16 15 7 remulcli -1 π 2
17 reefcl -1 π 2 e -1 π 2
18 16 17 ax-mp e -1 π 2
19 14 18 eqeltri i i