Metamath Proof Explorer

Theorem iexpire

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

Ref Expression
Assertion iexpire 
|- ( _i ^c _i ) e. RR

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 ine0 
 |-  _i =/= 0
3 cxpef 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ _i e. CC ) -> ( _i ^c _i ) = ( exp ` ( _i x. ( log ` _i ) ) ) )
4 1 2 1 3 mp3an 
 |-  ( _i ^c _i ) = ( exp ` ( _i x. ( log ` _i ) ) )
5 logi 
 |-  ( log ` _i ) = ( _i x. ( _pi / 2 ) )
6 5 oveq2i 
 |-  ( _i x. ( log ` _i ) ) = ( _i x. ( _i x. ( _pi / 2 ) ) )
7 halfpire 
 |-  ( _pi / 2 ) e. RR
8 7 recni 
 |-  ( _pi / 2 ) e. CC
9 1 1 8 mulassi 
 |-  ( ( _i x. _i ) x. ( _pi / 2 ) ) = ( _i x. ( _i x. ( _pi / 2 ) ) )
10 ixi 
 |-  ( _i x. _i ) = -u 1
11 10 oveq1i 
 |-  ( ( _i x. _i ) x. ( _pi / 2 ) ) = ( -u 1 x. ( _pi / 2 ) )
12 6 9 11 3eqtr2i 
 |-  ( _i x. ( log ` _i ) ) = ( -u 1 x. ( _pi / 2 ) )
13 12 fveq2i 
 |-  ( exp ` ( _i x. ( log ` _i ) ) ) = ( exp ` ( -u 1 x. ( _pi / 2 ) ) )
14 4 13 eqtri 
 |-  ( _i ^c _i ) = ( exp ` ( -u 1 x. ( _pi / 2 ) ) )
15 neg1rr 
 |-  -u 1 e. RR
16 15 7 remulcli 
 |-  ( -u 1 x. ( _pi / 2 ) ) e. RR
17 reefcl 
 |-  ( ( -u 1 x. ( _pi / 2 ) ) e. RR -> ( exp ` ( -u 1 x. ( _pi / 2 ) ) ) e. RR )
18 16 17 ax-mp 
 |-  ( exp ` ( -u 1 x. ( _pi / 2 ) ) ) e. RR
19 14 18 eqeltri 
 |-  ( _i ^c _i ) e. RR