This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpcxpcl

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

Ref Expression
Assertion rpcxpcl 
|- ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ )

Proof

Step Hyp Ref Expression
1 rprege0 
 |-  ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
2 recxpcl 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )
3 2 3expa 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) -> ( A ^c B ) e. RR )
4 1 3 sylan 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR )
5 id 
 |-  ( B e. RR -> B e. RR )
6 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
7 remulcl 
 |-  ( ( B e. RR /\ ( log ` A ) e. RR ) -> ( B x. ( log ` A ) ) e. RR )
8 5 6 7 syl2anr 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( B x. ( log ` A ) ) e. RR )
9 efgt0 
 |-  ( ( B x. ( log ` A ) ) e. RR -> 0 < ( exp ` ( B x. ( log ` A ) ) ) )
10 8 9 syl 
 |-  ( ( A e. RR+ /\ B e. RR ) -> 0 < ( exp ` ( B x. ( log ` A ) ) ) )
11 rpcnne0 
 |-  ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
12 recn 
 |-  ( B e. RR -> B e. CC )
13 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
14 13 3expa 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
15 11 12 14 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
16 10 15 breqtrrd 
 |-  ( ( A e. RR+ /\ B e. RR ) -> 0 < ( A ^c B ) )
17 4 16 elrpd 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ )