Metamath Proof Explorer

Theorem recxpcl

Description: Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion recxpcl 
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 recn 
 |-  ( B e. RR -> B e. CC )
3 cxpval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )
5 4 3adant2 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )
6 1re 
 |-  1 e. RR
7 0re 
 |-  0 e. RR
8 6 7 ifcli 
 |-  if ( B = 0 , 1 , 0 ) e. RR
9 8 a1i 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A = 0 ) -> if ( B = 0 , 1 , 0 ) e. RR )
10 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
11 simpl3 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> B e. RR )
12 simpl1 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> A e. RR )
13 simpl2 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> 0 <_ A )
14 simpr 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> A =/= 0 )
15 12 13 14 ne0gt0d 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> 0 < A )
16 12 15 elrpd 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> A e. RR+ )
17 16 relogcld 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> ( log ` A ) e. RR )
18 11 17 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> ( B x. ( log ` A ) ) e. RR )
19 18 reefcld 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> ( exp ` ( B x. ( log ` A ) ) ) e. RR )
20 10 19 sylan2br 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ -. A = 0 ) -> ( exp ` ( B x. ( log ` A ) ) ) e. RR )
21 9 20 ifclda 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) e. RR )
22 5 21 eqeltrd 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )