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 28161).
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 28161. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 14711 for its closure, sqrtval 14586 for its value, sqrtth 14714 and sqsqrti 14725 for its relationship to squares, and sqrt11i 14734 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 14582 | . 2 class √ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cc 10524 | . . 3 class ℂ | |
4 | vy | . . . . . . . 8 setvar 𝑦 | |
5 | 4 | cv 1527 | . . . . . . 7 class 𝑦 |
6 | c2 11681 | . . . . . . 7 class 2 | |
7 | cexp 13419 | . . . . . . 7 class ↑ | |
8 | 5, 6, 7 | co 7145 | . . . . . 6 class (𝑦↑2) |
9 | 2 | cv 1527 | . . . . . 6 class 𝑥 |
10 | 8, 9 | wceq 1528 | . . . . 5 wff (𝑦↑2) = 𝑥 |
11 | cc0 10526 | . . . . . 6 class 0 | |
12 | cre 14446 | . . . . . . 7 class ℜ | |
13 | 5, 12 | cfv 6349 | . . . . . 6 class (ℜ‘𝑦) |
14 | cle 10665 | . . . . . 6 class ≤ | |
15 | 11, 13, 14 | wbr 5058 | . . . . 5 wff 0 ≤ (ℜ‘𝑦) |
16 | ci 10528 | . . . . . . 7 class i | |
17 | cmul 10531 | . . . . . . 7 class · | |
18 | 16, 5, 17 | co 7145 | . . . . . 6 class (i · 𝑦) |
19 | crp 12379 | . . . . . 6 class ℝ+ | |
20 | 18, 19 | wnel 3123 | . . . . 5 wff (i · 𝑦) ∉ ℝ+ |
21 | 10, 15, 20 | w3a 1079 | . . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+) |
22 | 21, 4, 3 | crio 7102 | . . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)) |
23 | 2, 3, 22 | cmpt 5138 | . 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
24 | 1, 23 | wceq 1528 | 1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) |
Colors of variables: wff setvar class |
This definition is referenced by: sqrtval 14586 sqrtf 14713 cphsscph 23783 |
Copyright terms: Public domain | W3C validator |