![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-sqrt | Structured version Visualization version GIF version |
Description: Define a function whose
value is the square root of a complex number.
For example, (√‘25) = 5 (ex-sqrt 28014).
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 14585 for its closure, sqrtval 14460 for its value, sqrtth 14588 and sqsqrti 14599 for its relationship to squares, and sqrt11i 14608 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
Ref | Expression |
---|---|
df-sqrt | ⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csqrt 14456 | . 2 class √ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cc 10335 | . . 3 class ℂ | |
4 | vy | . . . . . . . 8 setvar 𝑦 | |
5 | 4 | cv 1506 | . . . . . . 7 class 𝑦 |
6 | c2 11498 | . . . . . . 7 class 2 | |
7 | cexp 13247 | . . . . . . 7 class ↑ | |
8 | 5, 6, 7 | co 6978 | . . . . . 6 class (𝑦↑2) |
9 | 2 | cv 1506 | . . . . . 6 class 𝑥 |
10 | 8, 9 | wceq 1507 | . . . . 5 wff (𝑦↑2) = 𝑥 |
11 | cc0 10337 | . . . . . 6 class 0 | |
12 | cre 14320 | . . . . . . 7 class ℜ | |
13 | 5, 12 | cfv 6190 | . . . . . 6 class (ℜ‘𝑦) |
14 | cle 10477 | . . . . . 6 class ≤ | |
15 | 11, 13, 14 | wbr 4930 | . . . . 5 wff 0 ≤ (ℜ‘𝑦) |
16 | ci 10339 | . . . . . . 7 class i | |
17 | cmul 10342 | . . . . . . 7 class · | |
18 | 16, 5, 17 | co 6978 | . . . . . 6 class (i · 𝑦) |
19 | crp 12207 | . . . . . 6 class ℝ+ | |
20 | 18, 19 | wnel 3073 | . . . . 5 wff (i · 𝑦) ∉ ℝ+ |
21 | 10, 15, 20 | w3a 1068 | . . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+) |
22 | 21, 4, 3 | crio 6938 | . . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)) |
23 | 2, 3, 22 | cmpt 5009 | . 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
24 | 1, 23 | wceq 1507 | 1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
Colors of variables: wff setvar class |
This definition is referenced by: sqrtval 14460 sqrtf 14587 cphsscph 23560 |
Copyright terms: Public domain | W3C validator |