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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cjnegi 15001 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
โข ๐ด โ โ โ โข (โโ-๐ด) = -(โโ๐ด) | ||
Theorem | addcji 15002 | 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 15003 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | imaddi 15004 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | remuli 15005 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | immuli 15006 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjaddi 15007 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต)) | ||
Theorem | cjmuli 15008 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต)) | ||
Theorem | ipcni 15009 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | cjdivi 15010 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ต โ 0 โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | crrei 15011 | 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 15012 | 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 15013 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | imcld 15014 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | cjcld 15015 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โ) | ||
Theorem | replimd 15016 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด = ((โโ๐ด) + (i ยท (โโ๐ด)))) | ||
Theorem | remimd 15017 | 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 15018 | 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 15019 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (โโ๐ด) = 0) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | rerebd 15020 | 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 15021 | 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 15022 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ๐ด) โ 0) | ||
Theorem | recjd 15023 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = (โโ๐ด)) | ||
Theorem | imcjd 15024 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ(โโ๐ด)) = -(โโ๐ด)) | ||
Theorem | cjmulrcld 15025 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) โ โ) | ||
Theorem | cjmulvald 15026 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ด ยท (โโ๐ด)) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) | ||
Theorem | cjmulge0d 15027 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ 0 โค (๐ด ยท (โโ๐ด))) | ||
Theorem | renegd 15028 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | imnegd 15029 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | cjnegd 15030 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ-๐ด) = -(โโ๐ด)) | ||
Theorem | addcjd 15031 | 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 15032 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) | ||
Theorem | readdd 15033 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | imaddd 15034 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | resubd 15035 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | imsubd 15036 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด โ ๐ต)) = ((โโ๐ด) โ (โโ๐ต))) | ||
Theorem | remuld 15037 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) โ ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | immuld 15038 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjaddd 15039 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) | ||
Theorem | cjmuld 15040 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | ipcnd 15041 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท (โโ๐ต))) = (((โโ๐ด) ยท (โโ๐ต)) + ((โโ๐ด) ยท (โโ๐ต)))) | ||
Theorem | cjdivd 15042 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | rered 15043 | 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 15044 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) = 0) | ||
Theorem | cjred 15045 | 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 15046 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | immul2d 15047 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | redivd 15048 | Real part of a division. Related to remul2 14949. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | imdivd 15049 | Imaginary part of a division. Related to remul2 14949. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | crred 15050 | 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 15051 | 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 15052 | Extend class notation to include square root of a complex number. |
class โ | ||
Syntax | cabs 15053 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 15054* |
Define a function whose value is the square root of a complex number.
For example, (โโ25) = 5 (ex-sqrt 29184).
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 29184. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15181 for its closure, sqrtval 15056 for its value, sqrtth 15184 and sqsqrti 15195 for its relationship to squares, and sqrt11i 15204 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
โข โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) | ||
Definition | df-abs 15055 | Define the function for the absolute value (modulus) of a complex number. See abscli 15215 for its closure and absval 15057 or absval2i 15217 for its value. For example, (absโ-2) = 2 (ex-abs 29185). (Contributed by NM, 27-Jul-1999.) |
โข abs = (๐ฅ โ โ โฆ (โโ(๐ฅ ยท (โโ๐ฅ)))) | ||
Theorem | sqrtval 15056* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (โโ๐ด) = (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))) | ||
Theorem | absval 15057 | 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 15058 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (i ยท ๐ด) โ โ+) | ||
Theorem | cnpart 15059 | 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 15060 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง ((๐ดโ2) = 0 โง 0 โค (โโ๐ด) โง (i ยท ๐ด) โ โ+)) โ ๐ด = 0) | ||
Theorem | sqrt0 15061 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข (โโ0) = 0 | ||
Theorem | sqrlem1 15062* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฆ โ ๐ ๐ฆ โค 1) | ||
Theorem | sqrlem2 15063* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ๐ด โ ๐) | ||
Theorem | sqrlem3 15064* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ฆ โ ๐ ๐ฆ โค ๐ง)) | ||
Theorem | sqrlem4 15065* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ต โ โ+ โง ๐ต โค 1)) | ||
Theorem | sqrlem5 15066* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ((๐ โ โ โง ๐ โ โ โง โ๐ฃ โ โ โ๐ข โ ๐ ๐ข โค ๐ฃ) โง (๐ตโ2) = sup(๐, โ, < ))) | ||
Theorem | sqrlem6 15067* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) โค ๐ด) | ||
Theorem | sqrlem7 15068* | Lemma for 01sqrex 15069. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) = ๐ด) | ||
Theorem | 01sqrex 15069* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฅ โ โ+ (๐ฅ โค 1 โง (๐ฅโ2) = ๐ด)) | ||
Theorem | resqrex 15070* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ โ๐ฅ โ โ (0 โค ๐ฅ โง (๐ฅโ2) = ๐ด)) | ||
Theorem | sqrmo 15071* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
โข (๐ด โ โ โ โ*๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)) | ||
Theorem | resqreu 15072* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ โ!๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)) | ||
Theorem | resqrtcl 15073 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ๐ด) โ โ) | ||
Theorem | resqrtthlem 15074 | Lemma for resqrtth 15075. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((โโ๐ด)โ2) = ๐ด โง 0 โค (โโ(โโ๐ด)) โง (i ยท (โโ๐ด)) โ โ+)) | ||
Theorem | resqrtth 15075 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด)โ2) = ๐ด) | ||
Theorem | remsqsqrt 15076 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด) ยท (โโ๐ด)) = ๐ด) | ||
Theorem | sqrtge0 15077 | 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 15078 | 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 15079 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | sqrtle 15080 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โค ๐ต โ (โโ๐ด) โค (โโ๐ต))) | ||
Theorem | sqrtlt 15081 | Square root is strictly monotonic. Closed form of sqrtlti 15209. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (โโ๐ด) < (โโ๐ต))) | ||
Theorem | sqrt11 15082 | The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = (โโ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | sqrt00 15083 | 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 15084 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
โข (๐ด โ โ+ โ (โโ๐ด) โ โ+) | ||
Theorem | sqrtdiv 15085 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ+) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | sqrtneglem 15086 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((i ยท (โโ๐ด))โ2) = -๐ด โง 0 โค (โโ(i ยท (โโ๐ด))) โง (i ยท (i ยท (โโ๐ด))) โ โ+)) | ||
Theorem | sqrtneg 15087 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ-๐ด) = (i ยท (โโ๐ด))) | ||
Theorem | sqrtsq2 15088 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = ๐ต โ ๐ด = (๐ตโ2))) | ||
Theorem | sqrtsq 15089 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ดโ2)) = ๐ด) | ||
Theorem | sqrtmsq 15090 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ด ยท ๐ด)) = ๐ด) | ||
Theorem | sqrt1 15091 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
โข (โโ1) = 1 | ||
Theorem | sqrt4 15092 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
โข (โโ4) = 2 | ||
Theorem | sqrt9 15093 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
โข (โโ9) = 3 | ||
Theorem | sqrt2gt1lt2 15094 | 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 15095 | 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 15054 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 11053 or i2 14033 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 15096 | 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 15097 | Absolute value of the opposite. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ (absโ-๐ด) = (absโ๐ด)) | ||
Theorem | abscl 15098 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
โข (๐ด โ โ โ (absโ๐ด) โ โ) | ||
Theorem | abscj 15099 | 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 15100 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (๐ด ยท (โโ๐ด))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |