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 ⊢ ↑ c = x ∈ ℂ , y ∈ ℂ ⟼ if x = 0 if y = 0 1 0 e y ⁢ log ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccxp class ↑ c
1 vx setvar x
2 cc class ℂ
3 vy setvar y
4 1 cv setvar x
5 cc0 class 0
6 4 5 wceq wff x = 0
7 3 cv setvar y
8 7 5 wceq wff y = 0
9 c1 class 1
10 8 9 5 cif class if y = 0 1 0
11 ce class exp
12 cmul class ×
13 clog class log
14 4 13 cfv class log ⁡ x
15 7 14 12 co class y ⁢ log ⁡ x
16 15 11 cfv class e y ⁢ log ⁡ x
17 6 10 16 cif class if x = 0 if y = 0 1 0 e y ⁢ log ⁡ x
18 1 3 2 2 17 cmpo class x ∈ ℂ , y ∈ ℂ ⟼ if x = 0 if y = 0 1 0 e y ⁢ log ⁡ x
19 0 18 wceq wff ↑ c = x ∈ ℂ , y ∈ ℂ ⟼ if x = 0 if y = 0 1 0 e y ⁢ log ⁡ x