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 26703).
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 13949 for its closure, sqrtval 13825 for its value, sqrtth 13952 and sqsqrti 13963 for its relationship to squares, and sqrt11i 13972 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 13821 | . 2 class √ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cc 9813 | . . 3 class ℂ | |
4 | vy | . . . . . . . 8 setvar 𝑦 | |
5 | 4 | cv 1474 | . . . . . . 7 class 𝑦 |
6 | c2 10947 | . . . . . . 7 class 2 | |
7 | cexp 12722 | . . . . . . 7 class ↑ | |
8 | 5, 6, 7 | co 6549 | . . . . . 6 class (𝑦↑2) |
9 | 2 | cv 1474 | . . . . . 6 class 𝑥 |
10 | 8, 9 | wceq 1475 | . . . . 5 wff (𝑦↑2) = 𝑥 |
11 | cc0 9815 | . . . . . 6 class 0 | |
12 | cre 13685 | . . . . . . 7 class ℜ | |
13 | 5, 12 | cfv 5804 | . . . . . 6 class (ℜ‘𝑦) |
14 | cle 9954 | . . . . . 6 class ≤ | |
15 | 11, 13, 14 | wbr 4583 | . . . . 5 wff 0 ≤ (ℜ‘𝑦) |
16 | ci 9817 | . . . . . . 7 class i | |
17 | cmul 9820 | . . . . . . 7 class · | |
18 | 16, 5, 17 | co 6549 | . . . . . 6 class (i · 𝑦) |
19 | crp 11708 | . . . . . 6 class ℝ+ | |
20 | 18, 19 | wnel 2781 | . . . . 5 wff (i · 𝑦) ∉ ℝ+ |
21 | 10, 15, 20 | w3a 1031 | . . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+) |
22 | 21, 4, 3 | crio 6510 | . . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)) |
23 | 2, 3, 22 | cmpt 4643 | . 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
24 | 1, 23 | wceq 1475 | 1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
Colors of variables: wff setvar class |
This definition is referenced by: sqrtval 13825 sqrtf 13951 |
Copyright terms: Public domain | W3C validator |