Metamath Proof Explorer


Theorem recxpcld

Description: Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses recxpcld.1
|- ( ph -> A e. RR )
recxpcld.2
|- ( ph -> 0 <_ A )
recxpcld.3
|- ( ph -> B e. RR )
Assertion recxpcld
|- ( ph -> ( A ^c B ) e. RR )

Proof

Step Hyp Ref Expression
1 recxpcld.1
 |-  ( ph -> A e. RR )
2 recxpcld.2
 |-  ( ph -> 0 <_ A )
3 recxpcld.3
 |-  ( ph -> B e. RR )
4 recxpcl
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )
5 1 2 3 4 syl3anc
 |-  ( ph -> ( A ^c B ) e. RR )