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 )