![]() |
Metamath
Proof Explorer Theorem List (p. 153 of 484) | < 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: | ![]() (1-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | remul2d 15201 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | immul2d 15202 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (โโ(๐ด ยท ๐ต)) = (๐ด ยท (โโ๐ต))) | ||
Theorem | redivd 15203 | Real part of a division. Related to remul2 15104. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | imdivd 15204 | Imaginary part of a division. Related to remul2 15104. (Contributed by Mario Carneiro, 29-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (โโ(๐ต / ๐ด)) = ((โโ๐ต) / ๐ด)) | ||
Theorem | crred 15205 | 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 15206 | 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 15207 | Extend class notation to include square root of a complex number. |
class โ | ||
Syntax | cabs 15208 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 15209* |
Define a function whose value is the square root of a complex number.
For example, (โโ25) = 5 (ex-sqrt 30303).
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 30303. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15335 for its closure, sqrtval 15211 for its value, sqrtth 15338 and sqsqrti 15349 for its relationship to squares, and sqrt11i 15358 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
โข โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โ ((๐ฆโ2) = ๐ฅ โง 0 โค (โโ๐ฆ) โง (i ยท ๐ฆ) โ โ+))) | ||
Definition | df-abs 15210 | Define the function for the absolute value (modulus) of a complex number. See abscli 15369 for its closure and absval 15212 or absval2i 15371 for its value. For example, (absโ-2) = 2 (ex-abs 30304). (Contributed by NM, 27-Jul-1999.) |
โข abs = (๐ฅ โ โ โฆ (โโ(๐ฅ ยท (โโ๐ฅ)))) | ||
Theorem | sqrtval 15211* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (โโ๐ด) = (โฉ๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+))) | ||
Theorem | absval 15212 | 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 15213 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
โข (๐ด โ โ โ (i ยท ๐ด) โ โ+) | ||
Theorem | cnpart 15214 | 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 | sqrt0 15215 | The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข (โโ0) = 0 | ||
Theorem | 01sqrexlem1 15216* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฆ โ ๐ ๐ฆ โค 1) | ||
Theorem | 01sqrexlem2 15217* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ๐ด โ ๐) | ||
Theorem | 01sqrexlem3 15218* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ฆ โ ๐ ๐ฆ โค ๐ง)) | ||
Theorem | 01sqrexlem4 15219* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ต โ โ+ โง ๐ต โค 1)) | ||
Theorem | 01sqrexlem5 15220* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ ((๐ โ โ โง ๐ โ โ โง โ๐ฃ โ โ โ๐ข โ ๐ ๐ข โค ๐ฃ) โง (๐ตโ2) = sup(๐, โ, < ))) | ||
Theorem | 01sqrexlem6 15221* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) โค ๐ด) | ||
Theorem | 01sqrexlem7 15222* | Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
โข ๐ = {๐ฅ โ โ+ โฃ (๐ฅโ2) โค ๐ด} & โข ๐ต = sup(๐, โ, < ) & โข ๐ = {๐ฆ โฃ โ๐ โ ๐ โ๐ โ ๐ ๐ฆ = (๐ ยท ๐)} โ โข ((๐ด โ โ+ โง ๐ด โค 1) โ (๐ตโ2) = ๐ด) | ||
Theorem | 01sqrex 15223* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ+ โง ๐ด โค 1) โ โ๐ฅ โ โ+ (๐ฅ โค 1 โง (๐ฅโ2) = ๐ด)) | ||
Theorem | resqrex 15224* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ โ๐ฅ โ โ (0 โค ๐ฅ โง (๐ฅโ2) = ๐ด)) | ||
Theorem | sqrmo 15225* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
โข (๐ด โ โ โ โ*๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)) | ||
Theorem | resqreu 15226* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ โ!๐ฅ โ โ ((๐ฅโ2) = ๐ด โง 0 โค (โโ๐ฅ) โง (i ยท ๐ฅ) โ โ+)) | ||
Theorem | resqrtcl 15227 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ๐ด) โ โ) | ||
Theorem | resqrtthlem 15228 | Lemma for resqrtth 15229. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((โโ๐ด)โ2) = ๐ด โง 0 โค (โโ(โโ๐ด)) โง (i ยท (โโ๐ด)) โ โ+)) | ||
Theorem | resqrtth 15229 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด)โ2) = ๐ด) | ||
Theorem | remsqsqrt 15230 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด) ยท (โโ๐ด)) = ๐ด) | ||
Theorem | sqrtge0 15231 | 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 15232 | 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 15233 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | sqrtle 15234 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โค ๐ต โ (โโ๐ด) โค (โโ๐ต))) | ||
Theorem | sqrtlt 15235 | Square root is strictly monotonic. Closed form of sqrtlti 15363. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (โโ๐ด) < (โโ๐ต))) | ||
Theorem | sqrt11 15236 | The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = (โโ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | sqrt00 15237 | 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 15238 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
โข (๐ด โ โ+ โ (โโ๐ด) โ โ+) | ||
Theorem | sqrtdiv 15239 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ+) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | sqrtneglem 15240 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((i ยท (โโ๐ด))โ2) = -๐ด โง 0 โค (โโ(i ยท (โโ๐ด))) โง (i ยท (i ยท (โโ๐ด))) โ โ+)) | ||
Theorem | sqrtneg 15241 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ-๐ด) = (i ยท (โโ๐ด))) | ||
Theorem | sqrtsq2 15242 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = ๐ต โ ๐ด = (๐ตโ2))) | ||
Theorem | sqrtsq 15243 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ดโ2)) = ๐ด) | ||
Theorem | sqrtmsq 15244 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ด ยท ๐ด)) = ๐ด) | ||
Theorem | sqrt1 15245 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
โข (โโ1) = 1 | ||
Theorem | sqrt4 15246 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
โข (โโ4) = 2 | ||
Theorem | sqrt9 15247 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
โข (โโ9) = 3 | ||
Theorem | sqrt2gt1lt2 15248 | 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 15249 | 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 15209 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 11201 or i2 14192 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 15250 | 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 15251 | Absolute value of the negative. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ (absโ-๐ด) = (absโ๐ด)) | ||
Theorem | abscl 15252 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
โข (๐ด โ โ โ (absโ๐ด) โ โ) | ||
Theorem | abscj 15253 | 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 15254 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (๐ด ยท (โโ๐ด))) | ||
Theorem | absvalsq2 15255 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) | ||
Theorem | sqabsadd 15256 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ(๐ด + ๐ต))โ2) = ((((absโ๐ด)โ2) + ((absโ๐ต)โ2)) + (2 ยท (โโ(๐ด ยท (โโ๐ต)))))) | ||
Theorem | sqabssub 15257 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ(๐ด โ ๐ต))โ2) = ((((absโ๐ด)โ2) + ((absโ๐ต)โ2)) โ (2 ยท (โโ(๐ด ยท (โโ๐ต)))))) | ||
Theorem | absval2 15258 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
โข (๐ด โ โ โ (absโ๐ด) = (โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2)))) | ||
Theorem | abs0 15259 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (absโ0) = 0 | ||
Theorem | absi 15260 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
โข (absโi) = 1 | ||
Theorem | absge0 15261 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ 0 โค (absโ๐ด)) | ||
Theorem | absrpcl 15262 | The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (absโ๐ด) โ โ+) | ||
Theorem | abs00 15263 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ ((absโ๐ด) = 0 โ ๐ด = 0)) | ||
Theorem | abs00ad 15264 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 15263. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ((absโ๐ด) = 0 โ ๐ด = 0)) | ||
Theorem | abs00bd 15265 | If a complex number is zero, its absolute value is zero. Converse of abs00d 15420. One-way deduction form of abs00 15263. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด = 0) โ โข (๐ โ (absโ๐ด) = 0) | ||
Theorem | absreimsq 15266 | Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ(๐ด + (i ยท ๐ต)))โ2) = ((๐ดโ2) + (๐ตโ2))) | ||
Theorem | absreim 15267 | Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ(๐ด + (i ยท ๐ต))) = (โโ((๐ดโ2) + (๐ตโ2)))) | ||
Theorem | absmul 15268 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ(๐ด ยท ๐ต)) = ((absโ๐ด) ยท (absโ๐ต))) | ||
Theorem | absdiv 15269 | Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (absโ(๐ด / ๐ต)) = ((absโ๐ด) / (absโ๐ต))) | ||
Theorem | absid 15270 | A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (absโ๐ด) = ๐ด) | ||
Theorem | abs1 15271 | The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.) |
โข (absโ1) = 1 | ||
Theorem | absnid 15272 | For a negative number, its absolute value is its negation. (Contributed by NM, 27-Feb-2005.) |
โข ((๐ด โ โ โง ๐ด โค 0) โ (absโ๐ด) = -๐ด) | ||
Theorem | leabs 15273 | A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ ๐ด โค (absโ๐ด)) | ||
Theorem | absor 15274 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ ((absโ๐ด) = ๐ด โจ (absโ๐ด) = -๐ด)) | ||
Theorem | absre 15275 | Absolute value of a real number. (Contributed by NM, 17-Mar-2005.) |
โข (๐ด โ โ โ (absโ๐ด) = (โโ(๐ดโ2))) | ||
Theorem | absresq 15276 | Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (๐ดโ2)) | ||
Theorem | absmod0 15277 | ๐ด is divisible by ๐ต iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ ((๐ด mod ๐ต) = 0 โ ((absโ๐ด) mod ๐ต) = 0)) | ||
Theorem | absexp 15278 | Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) | ||
Theorem | absexpz 15279 | Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.) |
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) | ||
Theorem | abssq 15280 | Square can be moved in and out of absolute value. (Contributed by Scott Fenton, 18-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (absโ(๐ดโ2))) | ||
Theorem | sqabs 15281 | The squares of two reals are equal iff their absolute values are equal. (Contributed by NM, 6-Mar-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ2) = (๐ตโ2) โ (absโ๐ด) = (absโ๐ต))) | ||
Theorem | absrele 15282 | The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005.) |
โข (๐ด โ โ โ (absโ(โโ๐ด)) โค (absโ๐ด)) | ||
Theorem | absimle 15283 | The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ (absโ(โโ๐ด)) โค (absโ๐ด)) | ||
Theorem | max0add 15284 | The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Mario Carneiro, 24-Aug-2014.) |
โข (๐ด โ โ โ (if(0 โค ๐ด, ๐ด, 0) + if(0 โค -๐ด, -๐ด, 0)) = (absโ๐ด)) | ||
Theorem | absz 15285 | A real number is an integer iff its absolute value is an integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ (๐ด โ โค โ (absโ๐ด) โ โค)) | ||
Theorem | nn0abscl 15286 | The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โค โ (absโ๐ด) โ โ0) | ||
Theorem | zabscl 15287 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข (๐ด โ โค โ (absโ๐ด) โ โค) | ||
Theorem | abslt 15288 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ๐ด) < ๐ต โ (-๐ต < ๐ด โง ๐ด < ๐ต))) | ||
Theorem | absle 15289 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ๐ด) โค ๐ต โ (-๐ต โค ๐ด โง ๐ด โค ๐ต))) | ||
Theorem | abssubne0 15290 | If the absolute value of a complex number is less than a real, its difference from the real is nonzero. (Contributed by NM, 2-Nov-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (absโ๐ด) < ๐ต) โ (๐ต โ ๐ด) โ 0) | ||
Theorem | absdiflt 15291 | The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((absโ(๐ด โ ๐ต)) < ๐ถ โ ((๐ต โ ๐ถ) < ๐ด โง ๐ด < (๐ต + ๐ถ)))) | ||
Theorem | absdifle 15292 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((absโ(๐ด โ ๐ต)) โค ๐ถ โ ((๐ต โ ๐ถ) โค ๐ด โง ๐ด โค (๐ต + ๐ถ)))) | ||
Theorem | elicc4abs 15293 | Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ((๐ด โ ๐ต)[,](๐ด + ๐ต)) โ (absโ(๐ถ โ ๐ด)) โค ๐ต)) | ||
Theorem | lenegsq 15294 | Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 0 โค ๐ต) โ ((๐ด โค ๐ต โง -๐ด โค ๐ต) โ (๐ดโ2) โค (๐ตโ2))) | ||
Theorem | releabs 15295 | The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by NM, 1-Apr-2005.) |
โข (๐ด โ โ โ (โโ๐ด) โค (absโ๐ด)) | ||
Theorem | recval 15296 | Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) = ((โโ๐ด) / ((absโ๐ด)โ2))) | ||
Theorem | absidm 15297 | The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.) |
โข (๐ด โ โ โ (absโ(absโ๐ด)) = (absโ๐ด)) | ||
Theorem | absgt0 15298 | The absolute value of a nonzero number is positive. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ (๐ด โ 0 โ 0 < (absโ๐ด))) | ||
Theorem | nnabscl 15299 | The absolute value of a nonzero integer is a positive integer. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
โข ((๐ โ โค โง ๐ โ 0) โ (absโ๐) โ โ) | ||
Theorem | abssub 15300 | Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ(๐ด โ ๐ต)) = (absโ(๐ต โ ๐ด))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |