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