![]() |
Metamath
Proof Explorer Theorem List (p. 153 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | resqrtthlem 15201 | Lemma for resqrtth 15202. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((โโ๐ด)โ2) = ๐ด โง 0 โค (โโ(โโ๐ด)) โง (i ยท (โโ๐ด)) โ โ+)) | ||
Theorem | resqrtth 15202 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด)โ2) = ๐ด) | ||
Theorem | remsqsqrt 15203 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ ((โโ๐ด) ยท (โโ๐ด)) = ๐ด) | ||
Theorem | sqrtge0 15204 | 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 15205 | 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 15206 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (โโ(๐ด ยท ๐ต)) = ((โโ๐ด) ยท (โโ๐ต))) | ||
Theorem | sqrtle 15207 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โค ๐ต โ (โโ๐ด) โค (โโ๐ต))) | ||
Theorem | sqrtlt 15208 | Square root is strictly monotonic. Closed form of sqrtlti 15336. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (โโ๐ด) < (โโ๐ต))) | ||
Theorem | sqrt11 15209 | The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = (โโ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | sqrt00 15210 | 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 15211 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
โข (๐ด โ โ+ โ (โโ๐ด) โ โ+) | ||
Theorem | sqrtdiv 15212 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ+) โ (โโ(๐ด / ๐ต)) = ((โโ๐ด) / (โโ๐ต))) | ||
Theorem | sqrtneglem 15213 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (((i ยท (โโ๐ด))โ2) = -๐ด โง 0 โค (โโ(i ยท (โโ๐ด))) โง (i ยท (i ยท (โโ๐ด))) โ โ+)) | ||
Theorem | sqrtneg 15214 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ-๐ด) = (i ยท (โโ๐ด))) | ||
Theorem | sqrtsq2 15215 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((โโ๐ด) = ๐ต โ ๐ด = (๐ตโ2))) | ||
Theorem | sqrtsq 15216 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ดโ2)) = ๐ด) | ||
Theorem | sqrtmsq 15217 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง 0 โค ๐ด) โ (โโ(๐ด ยท ๐ด)) = ๐ด) | ||
Theorem | sqrt1 15218 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
โข (โโ1) = 1 | ||
Theorem | sqrt4 15219 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
โข (โโ4) = 2 | ||
Theorem | sqrt9 15220 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
โข (โโ9) = 3 | ||
Theorem | sqrt2gt1lt2 15221 | 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 15222 | 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 15182 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 11178 or i2 14166 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 15223 | 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 15224 | Absolute value of the opposite. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ (absโ-๐ด) = (absโ๐ด)) | ||
Theorem | abscl 15225 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
โข (๐ด โ โ โ (absโ๐ด) โ โ) | ||
Theorem | abscj 15226 | 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 15227 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (๐ด ยท (โโ๐ด))) | ||
Theorem | absvalsq2 15228 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) | ||
Theorem | sqabsadd 15229 | 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 15230 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ(๐ด โ ๐ต))โ2) = ((((absโ๐ด)โ2) + ((absโ๐ต)โ2)) โ (2 ยท (โโ(๐ด ยท (โโ๐ต)))))) | ||
Theorem | absval2 15231 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
โข (๐ด โ โ โ (absโ๐ด) = (โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2)))) | ||
Theorem | abs0 15232 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (absโ0) = 0 | ||
Theorem | absi 15233 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
โข (absโi) = 1 | ||
Theorem | absge0 15234 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
โข (๐ด โ โ โ 0 โค (absโ๐ด)) | ||
Theorem | absrpcl 15235 | 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 15236 | 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 15237 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 15236. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ((absโ๐ด) = 0 โ ๐ด = 0)) | ||
Theorem | abs00bd 15238 | If a complex number is zero, its absolute value is zero. Converse of abs00d 15393. One-way deduction form of abs00 15236. (Contributed by David Moews, 28-Feb-2017.) |
โข (๐ โ ๐ด = 0) โ โข (๐ โ (absโ๐ด) = 0) | ||
Theorem | absreimsq 15239 | 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 15240 | 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 15241 | 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 15242 | Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (absโ(๐ด / ๐ต)) = ((absโ๐ด) / (absโ๐ต))) | ||
Theorem | absid 15243 | 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 15244 | The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.) |
โข (absโ1) = 1 | ||
Theorem | absnid 15245 | A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.) |
โข ((๐ด โ โ โง ๐ด โค 0) โ (absโ๐ด) = -๐ด) | ||
Theorem | leabs 15246 | A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ ๐ด โค (absโ๐ด)) | ||
Theorem | absor 15247 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.) |
โข (๐ด โ โ โ ((absโ๐ด) = ๐ด โจ (absโ๐ด) = -๐ด)) | ||
Theorem | absre 15248 | Absolute value of a real number. (Contributed by NM, 17-Mar-2005.) |
โข (๐ด โ โ โ (absโ๐ด) = (โโ(๐ดโ2))) | ||
Theorem | absresq 15249 | Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.) |
โข (๐ด โ โ โ ((absโ๐ด)โ2) = (๐ดโ2)) | ||
Theorem | absmod0 15250 | ๐ด is divisible by ๐ต iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ ((๐ด mod ๐ต) = 0 โ ((absโ๐ด) mod ๐ต) = 0)) | ||
Theorem | absexp 15251 | Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) | ||
Theorem | absexpz 15252 | Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.) |
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) | ||
Theorem | abssq 15253 | 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 15254 | 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 15255 | 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 15256 | 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 15257 | 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 15258 | 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 15259 | 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 15260 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข (๐ด โ โค โ (absโ๐ด) โ โค) | ||
Theorem | abslt 15261 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ๐ด) < ๐ต โ (-๐ต < ๐ด โง ๐ด < ๐ต))) | ||
Theorem | absle 15262 | 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 15263 | 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 15264 | The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((absโ(๐ด โ ๐ต)) < ๐ถ โ ((๐ต โ ๐ถ) < ๐ด โง ๐ด < (๐ต + ๐ถ)))) | ||
Theorem | absdifle 15265 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((absโ(๐ด โ ๐ต)) โค ๐ถ โ ((๐ต โ ๐ถ) โค ๐ด โง ๐ด โค (๐ต + ๐ถ)))) | ||
Theorem | elicc4abs 15266 | Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ((๐ด โ ๐ต)[,](๐ด + ๐ต)) โ (absโ(๐ถ โ ๐ด)) โค ๐ต)) | ||
Theorem | lenegsq 15267 | Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 0 โค ๐ต) โ ((๐ด โค ๐ต โง -๐ด โค ๐ต) โ (๐ดโ2) โค (๐ตโ2))) | ||
Theorem | releabs 15268 | 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 15269 | Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) = ((โโ๐ด) / ((absโ๐ด)โ2))) | ||
Theorem | absidm 15270 | The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.) |
โข (๐ด โ โ โ (absโ(absโ๐ด)) = (absโ๐ด)) | ||
Theorem | absgt0 15271 | 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 15272 | 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 15273 | 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 15274 | Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โค ๐ต) โ (absโ(๐ต โ ๐ด)) = (๐ต โ ๐ด)) | ||
Theorem | abssuble0 15275 | Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โค ๐ต) โ (absโ(๐ด โ ๐ต)) = (๐ต โ ๐ด)) | ||
Theorem | absmax 15276 | The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ if(๐ด โค ๐ต, ๐ต, ๐ด) = (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) | ||
Theorem | abstri 15277 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by NM, 7-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ(๐ด + ๐ต)) โค ((absโ๐ด) + (absโ๐ต))) | ||
Theorem | abs3dif 15278 | Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (absโ(๐ด โ ๐ต)) โค ((absโ(๐ด โ ๐ถ)) + (absโ(๐ถ โ ๐ต)))) | ||
Theorem | abs2dif 15279 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((absโ๐ด) โ (absโ๐ต)) โค (absโ(๐ด โ ๐ต))) | ||
Theorem | abs2dif2 15280 | Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ(๐ด โ ๐ต)) โค ((absโ๐ด) + (absโ๐ต))) | ||
Theorem | abs2difabs 15281 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (absโ((absโ๐ด) โ (absโ๐ต))) โค (absโ(๐ด โ ๐ต))) | ||
Theorem | abs1m 15282* | For any complex number, there exists a unit-magnitude multiplier that produces its absolute value. Part of proof of Theorem 13-2.12 of [Gleason] p. 195. (Contributed by NM, 26-Mar-2005.) |
โข (๐ด โ โ โ โ๐ฅ โ โ ((absโ๐ฅ) = 1 โง (absโ๐ด) = (๐ฅ ยท ๐ด))) | ||
Theorem | recan 15283* | Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ฅ โ โ (โโ(๐ฅ ยท ๐ด)) = (โโ(๐ฅ ยท ๐ต)) โ ๐ด = ๐ต)) | ||
Theorem | absf 15284 | Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) |
โข abs:โโถโ | ||
Theorem | abs3lem 15285 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (((absโ(๐ด โ ๐ถ)) < (๐ท / 2) โง (absโ(๐ถ โ ๐ต)) < (๐ท / 2)) โ (absโ(๐ด โ ๐ต)) < ๐ท)) | ||
Theorem | abslem2 15286 | Lemma involving absolute values. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (((โโ(๐ด / (absโ๐ด))) ยท ๐ด) + ((๐ด / (absโ๐ด)) ยท (โโ๐ด))) = (2 ยท (absโ๐ด))) | ||
Theorem | rddif 15287 | The difference between a real number and its nearest integer is less than or equal to one half. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Sep-2015.) |
โข (๐ด โ โ โ (absโ((โโ(๐ด + (1 / 2))) โ ๐ด)) โค (1 / 2)) | ||
Theorem | absrdbnd 15288 | Bound on the absolute value of a real number rounded to the nearest integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Sep-2015.) |
โข (๐ด โ โ โ (absโ(โโ(๐ด + (1 / 2)))) โค ((โโ(absโ๐ด)) + 1)) | ||
Theorem | fzomaxdiflem 15289 | Lemma for fzomaxdif 15290. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข (((๐ด โ (๐ถ..^๐ท) โง ๐ต โ (๐ถ..^๐ท)) โง ๐ด โค ๐ต) โ (absโ(๐ต โ ๐ด)) โ (0..^(๐ท โ ๐ถ))) | ||
Theorem | fzomaxdif 15290 | A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ด โ (๐ถ..^๐ท) โง ๐ต โ (๐ถ..^๐ท)) โ (absโ(๐ด โ ๐ต)) โ (0..^(๐ท โ ๐ถ))) | ||
Theorem | uzin2 15291 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
โข ((๐ด โ ran โคโฅ โง ๐ต โ ran โคโฅ) โ (๐ด โฉ ๐ต) โ ran โคโฅ) | ||
Theorem | rexanuz 15292* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
โข (โ๐ โ โค โ๐ โ (โคโฅโ๐)(๐ โง ๐) โ (โ๐ โ โค โ๐ โ (โคโฅโ๐)๐ โง โ๐ โ โค โ๐ โ (โคโฅโ๐)๐)) | ||
Theorem | rexanre 15293* | Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.) |
โข (๐ด โ โ โ (โ๐ โ โ โ๐ โ ๐ด (๐ โค ๐ โ (๐ โง ๐)) โ (โ๐ โ โ โ๐ โ ๐ด (๐ โค ๐ โ ๐) โง โ๐ โ โ โ๐ โ ๐ด (๐ โค ๐ โ ๐)))) | ||
Theorem | rexfiuz 15294* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
โข (๐ด โ Fin โ (โ๐ โ โค โ๐ โ (โคโฅโ๐)โ๐ โ ๐ด ๐ โ โ๐ โ ๐ด โ๐ โ โค โ๐ โ (โคโฅโ๐)๐)) | ||
Theorem | rexuz3 15295* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ (โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ โ โ๐ โ โค โ๐ โ (โคโฅโ๐)๐)) | ||
Theorem | rexanuz2 15296* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
โข ๐ = (โคโฅโ๐) โ โข (โ๐ โ ๐ โ๐ โ (โคโฅโ๐)(๐ โง ๐) โ (โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ โง โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐)) | ||
Theorem | r19.29uz 15297* | A version of 19.29 1877 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
โข ๐ = (โคโฅโ๐) โ โข ((โ๐ โ ๐ ๐ โง โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐) โ โ๐ โ ๐ โ๐ โ (โคโฅโ๐)(๐ โง ๐)) | ||
Theorem | r19.2uz 15298* | A version of r19.2z 4495 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
โข ๐ = (โคโฅโ๐) โ โข (โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ โ โ๐ โ ๐ ๐) | ||
Theorem | rexuzre 15299* | Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ (โ๐ โ ๐ โ๐ โ (โคโฅโ๐)๐ โ โ๐ โ โ โ๐ โ ๐ (๐ โค ๐ โ ๐))) | ||
Theorem | rexico 15300* | Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ โ (๐ต[,)+โ)โ๐ โ ๐ด (๐ โค ๐ โ ๐) โ โ๐ โ โ โ๐ โ ๐ด (๐ โค ๐ โ ๐))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |