![]() |
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 29974).
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 29974. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15312 for its closure, sqrtval 15188 for its value, sqrtth 15315 and sqsqrti 15326 for its relationship to squares, and sqrt11i 15335 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 15184 | . 2 class โ | |
2 | vx | . . 3 setvar ๐ฅ | |
3 | cc 11110 | . . 3 class โ | |
4 | vy | . . . . . . . 8 setvar ๐ฆ | |
5 | 4 | cv 1538 | . . . . . . 7 class ๐ฆ |
6 | c2 12271 | . . . . . . 7 class 2 | |
7 | cexp 14031 | . . . . . . 7 class โ | |
8 | 5, 6, 7 | co 7411 | . . . . . 6 class (๐ฆโ2) |
9 | 2 | cv 1538 | . . . . . 6 class ๐ฅ |
10 | 8, 9 | wceq 1539 | . . . . 5 wff (๐ฆโ2) = ๐ฅ |
11 | cc0 11112 | . . . . . 6 class 0 | |
12 | cre 15048 | . . . . . . 7 class โ | |
13 | 5, 12 | cfv 6542 | . . . . . 6 class (โโ๐ฆ) |
14 | cle 11253 | . . . . . 6 class โค | |
15 | 11, 13, 14 | wbr 5147 | . . . . 5 wff 0 โค (โโ๐ฆ) |
16 | ci 11114 | . . . . . . 7 class i | |
17 | cmul 11117 | . . . . . . 7 class ยท | |
18 | 16, 5, 17 | co 7411 | . . . . . 6 class (i ยท ๐ฆ) |
19 | crp 12978 | . . . . . 6 class โ+ | |
20 | 18, 19 | wnel 3044 | . . . . 5 wff (i ยท ๐ฆ) โ โ+ |
21 | 10, 15, 20 | w3a 1085 | . . . 4 wff ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+) |
22 | 21, 4, 3 | crio 7366 | . . 3 class (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+)) |
23 | 2, 3, 22 | cmpt 5230 | . 2 class (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) |
24 | 1, 23 | wceq 1539 | 1 wff โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) |
Colors of variables: wff setvar class |
This definition is referenced by: sqrtval 15188 sqrtf 15314 cphsscph 24999 |
Copyright terms: Public domain | W3C validator |