Step |
Hyp |
Ref |
Expression |
1 |
|
recn |
|- ( A e. RR -> A e. CC ) |
2 |
|
recn |
|- ( B e. RR -> B e. CC ) |
3 |
|
cxpval |
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( A e. RR /\ B e. RR ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) ) |
5 |
4
|
3adant2 |
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) ) |
6 |
|
1re |
|- 1 e. RR |
7 |
|
0re |
|- 0 e. RR |
8 |
6 7
|
ifcli |
|- if ( B = 0 , 1 , 0 ) e. RR |
9 |
8
|
a1i |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A = 0 ) -> if ( B = 0 , 1 , 0 ) e. RR ) |
10 |
|
df-ne |
|- ( A =/= 0 <-> -. A = 0 ) |
11 |
|
simpl3 |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> B e. RR ) |
12 |
|
simpl1 |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> A e. RR ) |
13 |
|
simpl2 |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> 0 <_ A ) |
14 |
|
simpr |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> A =/= 0 ) |
15 |
12 13 14
|
ne0gt0d |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> 0 < A ) |
16 |
12 15
|
elrpd |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> A e. RR+ ) |
17 |
16
|
relogcld |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> ( log ` A ) e. RR ) |
18 |
11 17
|
remulcld |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> ( B x. ( log ` A ) ) e. RR ) |
19 |
18
|
reefcld |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ A =/= 0 ) -> ( exp ` ( B x. ( log ` A ) ) ) e. RR ) |
20 |
10 19
|
sylan2br |
|- ( ( ( A e. RR /\ 0 <_ A /\ B e. RR ) /\ -. A = 0 ) -> ( exp ` ( B x. ( log ` A ) ) ) e. RR ) |
21 |
9 20
|
ifclda |
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) e. RR ) |
22 |
5 21
|
eqeltrd |
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR ) |