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

Definition df-sqrt 13925
Description: Define a function whose value is the square root of a complex number. For example, (√‘25) = 5 (ex-sqrt 27199).

Since (𝑦↑2) = 𝑥 iff (-𝑦↑2) = 𝑥, we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root. The square root symbol was introduced in 1525 by Christoff Rudolff.

See sqrtcl 14051 for its closure, sqrtval 13927 for its value, sqrtth 14054 and sqsqrti 14065 for its relationship to squares, and sqrt11i 14074 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)

Assertion
Ref Expression
df-sqrt √ = (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-sqrt
StepHypRef Expression
1 csqrt 13923 . 2 class
2 vx . . 3 setvar 𝑥
3 cc 9894 . . 3 class
4 vy . . . . . . . 8 setvar 𝑦
54cv 1479 . . . . . . 7 class 𝑦
6 c2 11030 . . . . . . 7 class 2
7 cexp 12816 . . . . . . 7 class
85, 6, 7co 6615 . . . . . 6 class (𝑦↑2)
92cv 1479 . . . . . 6 class 𝑥
108, 9wceq 1480 . . . . 5 wff (𝑦↑2) = 𝑥
11 cc0 9896 . . . . . 6 class 0
12 cre 13787 . . . . . . 7 class
135, 12cfv 5857 . . . . . 6 class (ℜ‘𝑦)
14 cle 10035 . . . . . 6 class
1511, 13, 14wbr 4623 . . . . 5 wff 0 ≤ (ℜ‘𝑦)
16 ci 9898 . . . . . . 7 class i
17 cmul 9901 . . . . . . 7 class ·
1816, 5, 17co 6615 . . . . . 6 class (i · 𝑦)
19 crp 11792 . . . . . 6 class +
2018, 19wnel 2893 . . . . 5 wff (i · 𝑦) ∉ ℝ+
2110, 15, 20w3a 1036 . . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
2221, 4, 3crio 6575 . . 3 class (𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
232, 3, 22cmpt 4683 . 2 class (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
241, 23wceq 1480 1 wff √ = (𝑥 ∈ ℂ ↦ (𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
Colors of variables: wff setvar class
This definition is referenced by:  sqrtval  13927  sqrtf  14053
  Copyright terms: Public domain W3C validator