Step |
Hyp |
Ref |
Expression |
1 |
|
cxpgt0d.1 |
|- ( ph -> A e. RR+ ) |
2 |
|
cxpgt0d.2 |
|- ( ph -> N e. RR ) |
3 |
1
|
relogcld |
|- ( ph -> ( log ` A ) e. RR ) |
4 |
2 3
|
remulcld |
|- ( ph -> ( N x. ( log ` A ) ) e. RR ) |
5 |
|
efgt0 |
|- ( ( N x. ( log ` A ) ) e. RR -> 0 < ( exp ` ( N x. ( log ` A ) ) ) ) |
6 |
4 5
|
syl |
|- ( ph -> 0 < ( exp ` ( N x. ( log ` A ) ) ) ) |
7 |
1
|
rpcnd |
|- ( ph -> A e. CC ) |
8 |
1
|
rpne0d |
|- ( ph -> A =/= 0 ) |
9 |
2
|
recnd |
|- ( ph -> N e. CC ) |
10 |
7 8 9
|
cxpefd |
|- ( ph -> ( A ^c N ) = ( exp ` ( N x. ( log ` A ) ) ) ) |
11 |
6 10
|
breqtrrd |
|- ( ph -> 0 < ( A ^c N ) ) |