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+BAB+

Proof

Step Hyp Ref Expression
1 rprege0 A+A0A
2 recxpcl A0ABAB
3 2 3expa A0ABAB
4 1 3 sylan A+BAB
5 id BB
6 relogcl A+logA
7 remulcl BlogABlogA
8 5 6 7 syl2anr A+BBlogA
9 efgt0 BlogA0<eBlogA
10 8 9 syl A+B0<eBlogA
11 rpcnne0 A+AA0
12 recn BB
13 cxpef AA0BAB=eBlogA
14 13 3expa AA0BAB=eBlogA
15 11 12 14 syl2an A+BAB=eBlogA
16 10 15 breqtrrd A+B0<AB
17 4 16 elrpd A+BAB+