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 27311).
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 14101 for its closure, sqrtval 13977 for its value, sqrtth 14104 and sqsqrti 14115 for its relationship to squares, and sqrt11i 14124 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 13973 | . 2 class √ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cc 9934 | . . 3 class ℂ | |
4 | vy | . . . . . . . 8 setvar 𝑦 | |
5 | 4 | cv 1482 | . . . . . . 7 class 𝑦 |
6 | c2 11070 | . . . . . . 7 class 2 | |
7 | cexp 12860 | . . . . . . 7 class ↑ | |
8 | 5, 6, 7 | co 6650 | . . . . . 6 class (𝑦↑2) |
9 | 2 | cv 1482 | . . . . . 6 class 𝑥 |
10 | 8, 9 | wceq 1483 | . . . . 5 wff (𝑦↑2) = 𝑥 |
11 | cc0 9936 | . . . . . 6 class 0 | |
12 | cre 13837 | . . . . . . 7 class ℜ | |
13 | 5, 12 | cfv 5888 | . . . . . 6 class (ℜ‘𝑦) |
14 | cle 10075 | . . . . . 6 class ≤ | |
15 | 11, 13, 14 | wbr 4653 | . . . . 5 wff 0 ≤ (ℜ‘𝑦) |
16 | ci 9938 | . . . . . . 7 class i | |
17 | cmul 9941 | . . . . . . 7 class · | |
18 | 16, 5, 17 | co 6650 | . . . . . 6 class (i · 𝑦) |
19 | crp 11832 | . . . . . 6 class ℝ+ | |
20 | 18, 19 | wnel 2897 | . . . . 5 wff (i · 𝑦) ∉ ℝ+ |
21 | 10, 15, 20 | w3a 1037 | . . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+) |
22 | 21, 4, 3 | crio 6610 | . . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)) |
23 | 2, 3, 22 | cmpt 4729 | . 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
24 | 1, 23 | wceq 1483 | 1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
Colors of variables: wff setvar class |
This definition is referenced by: sqrtval 13977 sqrtf 14103 |
Copyright terms: Public domain | W3C validator |