Home | Metamath
Proof Explorer Theorem List (p. 151 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | addcji 15001 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ โ โข (๐ด + (โโ๐ด)) = (2 ยท (โโ๐ด)) | ||
Theorem | readdi 15002 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | imaddi 15003 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | remuli 15004 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | immuli 15005 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjaddi 15006 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | cjmuli 15007 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต)) | ||
Theorem | ipcni 15008 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjdivi 15009 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | crrei 15010 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + (i ยท ๐ต))) = ๐ด | ||
Theorem | crimi 15011 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + (i ยท ๐ต))) = ๐ต | ||
Theorem | recld 15012 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | imcld 15013 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | cjcld 15014 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | replimd 15015 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด)))) | ||
Theorem | remimd 15016 | Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = ((โโ๐ด) โ (i ยท (โโ๐ด)))) | ||
Theorem | cjcjd 15017 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = ๐ด) | ||
Theorem | reim0bd 15018 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = 0) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rerebd 15019 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = ๐ด) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | cjrebd 15020 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = ๐ด) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | cjne0d 15021 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ๐ด) โ 0) | ||
Theorem | recjd 15022 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = (โโ๐ด)) | ||
Theorem | imcjd 15023 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = -(โโ๐ด)) | ||
Theorem | cjmulrcld 15024 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) โ โ) | ||
Theorem | cjmulvald 15025 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) | ||
Theorem | cjmulge0d 15026 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 โค (๐ด ยท (โโ๐ด))) | ||
Theorem | renegd 15027 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | imnegd 15028 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | cjnegd 15029 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | addcjd 15030 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด + (โโ๐ด)) = (2 ยท (โโ๐ด))) | ||
Theorem | cjexpd 15031 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) | ||
Theorem | readdd 15032 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | imaddd 15033 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | resubd 15034 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | imsubd 15035 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | remuld 15036 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | immuld 15037 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjaddd 15038 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | cjmuld 15039 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | ipcnd 15040 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjdivd 15041 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | rered 15042 | A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = ๐ด) | ||
Theorem | reim0d 15043 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = 0) | ||
Theorem | cjred 15044 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = ๐ด) | ||
Theorem | remul2d 15045 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | immul2d 15046 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | redivd 15047 | Real part of a division. Related to remul2 14948. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | imdivd 15048 | Imaginary part of a division. Related to remul2 14948. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | crred 15049 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ด) | ||
Theorem | crimd 15050 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + (i ยท ๐ต))) = ๐ต) | ||
Syntax | csqrt 15051 | Extend class notation to include square root of a complex number. |
class โ | ||
Syntax | cabs 15052 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 15053* |
Define a function whose value is the square root of a complex number.
For example, (โโ25) = 5 (ex-sqrt 29196).
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 29196. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15180 for its closure, sqrtval 15055 for its value, sqrtth 15183 and sqsqrti 15194 for its relationship to squares, and sqrt11i 15203 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
โข โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) | ||
Definition | df-abs 15054 | Define the function for the absolute value (modulus) of a complex number. See abscli 15214 for its closure and absval 15056 or absval2i 15216 for its value. For example, (absโ-2) = 2 (ex-abs 29197). (Contributed by NM, 27-Jul-1999.) |
โข abs = (๐ฅ โ โ โฆ (โโ(๐ฅ ยท (โโ๐ฅ)))) | ||
Theorem | sqrtval 15055* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (โโ๐ด) = (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))) | ||
Theorem | absval 15056 | The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
โข (๐ด โ โ โ (absโ๐ด) = (โโ(๐ด ยท (โโ๐ด)))) | ||
Theorem | rennim 15057 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (i ยท ๐ด) โ โ+) | ||
Theorem | cnpart 15058 | The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map ๐ฅ โฆ -๐ฅ). (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ ((0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+) โ ยฌ (0 โค (โโ-๐ด) โง (i ยท -๐ด) โ โ+))) | ||
Theorem | sqr0lem 15059 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง ((๐ดโ2) = 0 โง 0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+)) โ ๐ด = 0) | ||
Theorem | sqrt0 15060 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข (โโ0) = 0 | ||
Theorem | sqrlem1 15061* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฆ โ ๐ ๐ฆ โค 1) | ||
Theorem | sqrlem2 15062* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ๐ด โ ๐) | ||
Theorem | sqrlem3 15063* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ฆ โ ๐ ๐ฆ โค ๐ง)) | ||
Theorem | sqrlem4 15064* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ต โ โ+ โง ๐ต โค 1)) | ||
Theorem | sqrlem5 15065* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ((๐ โ โ โง ๐ โ โ โง โ๐ฃ โ โ โ๐ข โ ๐ ๐ข โค ๐ฃ) โง (๐ตโ2) = sup(๐, โ, < ))) | ||
Theorem | sqrlem6 15066* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) โค ๐ด) | ||
Theorem | sqrlem7 15067* | Lemma for 01sqrex 15068. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) = ๐ด) | ||
Theorem | 01sqrex 15068* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฅ โ โ+ (๐ฅ โค 1 โง (๐ฅโ2) = ๐ด)) | ||
Theorem | resqrex 15069* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ โ๐ฅ โ โ (0 โค ๐ฅ โง (๐ฅโ2) = ๐ด)) | ||
Theorem | sqrmo 15070* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
โข (๐ด โ โ โ โ*๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)) | ||
Theorem | resqreu 15071* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ โ!๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)) | ||
Theorem | resqrtcl 15072 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ๐ด) โ โ) | ||
Theorem | resqrtthlem 15073 | Lemma for resqrtth 15074. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((โโ๐ด)โ2) = ๐ด โง 0 โค (โโ(โโ๐ด)) โง (i ยท (โโ๐ด)) โ โ+)) | ||
Theorem | resqrtth 15074 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด)โ2) = ๐ด) | ||
Theorem | remsqsqrt 15075 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด) ยท (โโ๐ด)) = ๐ด) | ||
Theorem | sqrtge0 15076 | The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ 0 โค (โโ๐ด)) | ||
Theorem | sqrtgt0 15077 | The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ 0 < (โโ๐ด)) | ||
Theorem | sqrtmul 15078 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | sqrtle 15079 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โค ๐ต โ (โโ๐ด) โค (โโ๐ต))) | ||
Theorem | sqrtlt 15080 | Square root is strictly monotonic. Closed form of sqrtlti 15208. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (โโ๐ด) < (โโ๐ต))) | ||
Theorem | sqrt11 15081 | The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = (โโ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | sqrt00 15082 | A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด) = 0 โ ๐ด = 0)) | ||
Theorem | rpsqrtcl 15083 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
โข (๐ด โ โ+ โ (โโ๐ด) โ โ+) | ||
Theorem | sqrtdiv 15084 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ+) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | sqrtneglem 15085 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((i ยท (โโ๐ด))โ2) = -๐ด โง 0 โค (โโ(i ยท (โโ๐ด))) โง (i ยท (i ยท (โโ๐ด))) โ โ+)) | ||
Theorem | sqrtneg 15086 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ-๐ด) = (i ยท (โโ๐ด))) | ||
Theorem | sqrtsq2 15087 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = ๐ต โ ๐ด = (๐ตโ2))) | ||
Theorem | sqrtsq 15088 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ดโ2)) = ๐ด) | ||
Theorem | sqrtmsq 15089 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ด ยท ๐ด)) = ๐ด) | ||
Theorem | sqrt1 15090 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
โข (โโ1) = 1 | ||
Theorem | sqrt4 15091 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
โข (โโ4) = 2 | ||
Theorem | sqrt9 15092 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
โข (โโ9) = 3 | ||
Theorem | sqrt2gt1lt2 15093 | The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.) |
โข (1 < (โโ2) โง (โโ2) < 2) | ||
Theorem | sqrtm1 15094 | The imaginary unit is the square root of negative 1. A lot of people like to call this the "definition" of i, but the definition of โ df-sqrt 15053 has already been crafted with i being mentioned explicitly, and in any case it doesn't make too much sense to define a value based on a function evaluated outside its domain. A more appropriate view is to take ax-i2m1 11052 or i2 14032 as the "definition", and simply postulate the existence of a number satisfying this property. This is the approach we take here. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข i = (โโ-1) | ||
Theorem | nn0sqeq1 15095 | A natural number with square one is equal to one. (Contributed by Thierry Arnoux, 2-Feb-2020.) (Proof shortened by Thierry Arnoux, 6-Jun-2023.) |
โข ((๐ โ โ0 โง (๐โ2) = 1) โ ๐ = 1) | ||
Theorem | absneg 15096 | Absolute value of the opposite. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ (absโ-๐ด) = (absโ๐ด)) | ||
Theorem | abscl 15097 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
โข (๐ด โ โ โ (absโ๐ด) โ โ) | ||
Theorem | abscj 15098 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.) |
โข (๐ด โ โ โ (absโ(โโ๐ด)) = (absโ๐ด)) | ||
Theorem | absvalsq 15099 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (๐ด ยท (โโ๐ด))) | ||
Theorem | absvalsq2 15100 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |