MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cxp Structured version   Visualization version   GIF version

Definition df-cxp 24108
Description: Define the power function on complex numbers. Note that the value of this function when 𝑥 = 0 and (ℜ‘𝑦) ≤ 0, 𝑦 ≠ 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014.)
Assertion
Ref Expression
df-cxp 𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-cxp
StepHypRef Expression
1 ccxp 24106 . 2 class 𝑐
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cc 9813 . . 3 class
52cv 1474 . . . . 5 class 𝑥
6 cc0 9815 . . . . 5 class 0
75, 6wceq 1475 . . . 4 wff 𝑥 = 0
83cv 1474 . . . . . 6 class 𝑦
98, 6wceq 1475 . . . . 5 wff 𝑦 = 0
10 c1 9816 . . . . 5 class 1
119, 10, 6cif 4036 . . . 4 class if(𝑦 = 0, 1, 0)
12 clog 24105 . . . . . . 7 class log
135, 12cfv 5804 . . . . . 6 class (log‘𝑥)
14 cmul 9820 . . . . . 6 class ·
158, 13, 14co 6549 . . . . 5 class (𝑦 · (log‘𝑥))
16 ce 14631 . . . . 5 class exp
1715, 16cfv 5804 . . . 4 class (exp‘(𝑦 · (log‘𝑥)))
187, 11, 17cif 4036 . . 3 class if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))
192, 3, 4, 4, 18cmpt2 6551 . 2 class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))
201, 19wceq 1475 1 wff 𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))))
Colors of variables: wff setvar class
This definition is referenced by:  cxpval  24210
  Copyright terms: Public domain W3C validator