This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cxp

Description: Define the power function on complex numbers. Note that the value of this function when x = 0 and ( Rey ) <_ 0 , y =/= 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion df-cxp ↑𝑐 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccxp ⊢ ↑𝑐
1 vx ⊢ 𝑥
2 cc ⊢ ℂ
3 vy ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 cc0 ⊢ 0
6 4 5 wceq ⊢ 𝑥 = 0
7 3 cv ⊢ 𝑦
8 7 5 wceq ⊢ 𝑦 = 0
9 c1 ⊢ 1
10 8 9 5 cif ⊢ if ( 𝑦 = 0 , 1 , 0 )
11 ce ⊢ exp
12 cmul ⊢ ·
13 clog ⊢ log
14 4 13 cfv ⊢ ( log ‘ 𝑥 )
15 7 14 12 co ⊢ ( 𝑦 · ( log ‘ 𝑥 ) )
16 15 11 cfv ⊢ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) )
17 6 10 16 cif ⊢ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) )
18 1 3 2 2 17 cmpo ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )
19 0 18 wceq ⊢ ↑𝑐 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ if ( 𝑥 = 0 , if ( 𝑦 = 0 , 1 , 0 ) , ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) )