| Step |
Hyp |
Ref |
Expression |
| 1 |
|
simpl |
|- ( ( x = A /\ y = B ) -> x = A ) |
| 2 |
1
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( x = 0 <-> A = 0 ) ) |
| 3 |
|
simpr |
|- ( ( x = A /\ y = B ) -> y = B ) |
| 4 |
3
|
eqeq1d |
|- ( ( x = A /\ y = B ) -> ( y = 0 <-> B = 0 ) ) |
| 5 |
4
|
ifbid |
|- ( ( x = A /\ y = B ) -> if ( y = 0 , 1 , 0 ) = if ( B = 0 , 1 , 0 ) ) |
| 6 |
1
|
fveq2d |
|- ( ( x = A /\ y = B ) -> ( log ` x ) = ( log ` A ) ) |
| 7 |
3 6
|
oveq12d |
|- ( ( x = A /\ y = B ) -> ( y x. ( log ` x ) ) = ( B x. ( log ` A ) ) ) |
| 8 |
7
|
fveq2d |
|- ( ( x = A /\ y = B ) -> ( exp ` ( y x. ( log ` x ) ) ) = ( exp ` ( B x. ( log ` A ) ) ) ) |
| 9 |
2 5 8
|
ifbieq12d |
|- ( ( x = A /\ y = B ) -> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) ) |
| 10 |
|
df-cxp |
|- ^c = ( x e. CC , y e. CC |-> if ( x = 0 , if ( y = 0 , 1 , 0 ) , ( exp ` ( y x. ( log ` x ) ) ) ) ) |
| 11 |
|
ax-1cn |
|- 1 e. CC |
| 12 |
|
0cn |
|- 0 e. CC |
| 13 |
11 12
|
ifcli |
|- if ( B = 0 , 1 , 0 ) e. CC |
| 14 |
13
|
elexi |
|- if ( B = 0 , 1 , 0 ) e. _V |
| 15 |
|
fvex |
|- ( exp ` ( B x. ( log ` A ) ) ) e. _V |
| 16 |
14 15
|
ifex |
|- if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) e. _V |
| 17 |
9 10 16
|
ovmpoa |
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) ) |