Description: Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rpcxpcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rprege0 | |
|
2 | recxpcl | |
|
3 | 2 | 3expa | |
4 | 1 3 | sylan | |
5 | id | |
|
6 | relogcl | |
|
7 | remulcl | |
|
8 | 5 6 7 | syl2anr | |
9 | efgt0 | |
|
10 | 8 9 | syl | |
11 | rpcnne0 | |
|
12 | recn | |
|
13 | cxpef | |
|
14 | 13 | 3expa | |
15 | 11 12 14 | syl2an | |
16 | 10 15 | breqtrrd | |
17 | 4 16 | elrpd | |