![]() |
Metamath
Proof Explorer Theorem List (p. 154 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | r19.29uz 15301* | A version of 19.29 1874 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ ((βπ β π π β§ βπ β π βπ β (β€β₯βπ)π) β βπ β π βπ β (β€β₯βπ)(π β§ π)) | ||
Theorem | r19.2uz 15302* | A version of r19.2z 4493 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (βπ β π βπ β (β€β₯βπ)π β βπ β π π) | ||
Theorem | rexuzre 15303* | Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β (βπ β π βπ β (β€β₯βπ)π β βπ β β βπ β π (π β€ π β π))) | ||
Theorem | rexico 15304* | Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (βπ β (π΅[,)+β)βπ β π΄ (π β€ π β π) β βπ β β βπ β π΄ (π β€ π β π))) | ||
Theorem | cau3lem 15305* | Lemma for cau3 15306. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π β β€ & β’ (π β π) & β’ ((πΉβπ) = (πΉβπ) β (π β π)) & β’ ((πΉβπ) = (πΉβπ) β (π β π)) & β’ ((π β§ π β§ π) β (πΊβ((πΉβπ)π·(πΉβπ))) = (πΊβ((πΉβπ)π·(πΉβπ)))) & β’ ((π β§ π β§ π) β (πΊβ((πΉβπ)π·(πΉβπ))) = (πΊβ((πΉβπ)π·(πΉβπ)))) & β’ ((π β§ (π β§ π) β§ (π β§ π₯ β β)) β (((πΊβ((πΉβπ)π·(πΉβπ))) < (π₯ / 2) β§ (πΊβ((πΉβπ)π·(πΉβπ))) < (π₯ / 2)) β (πΊβ((πΉβπ)π·(πΉβπ))) < π₯)) β β’ (π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β§ (πΊβ((πΉβπ)π·(πΉβπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β§ βπ β (β€β₯βπ)(πΊβ((πΉβπ)π·(πΉβπ))) < π₯))) | ||
Theorem | cau3 15306* | Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of π in the assertion, so it can be used with rexanuz 15296 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯)) | ||
Theorem | cau4 15307* | Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) β β’ (π β π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) | ||
Theorem | caubnd2 15308* | A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ¦ β β βπ β π βπ β (β€β₯βπ)(absβ(πΉβπ)) < π¦) | ||
Theorem | caubnd 15309* | A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 14-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ ((βπ β π (πΉβπ) β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ¦ β β βπ β π (absβ(πΉβπ)) < π¦) | ||
Theorem | sqreulem 15310 | Lemma for sqreu 15311: write a general complex square root in terms of the square root function over nonnegative reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ π΅ = ((ββ(absβπ΄)) Β· (((absβπ΄) + π΄) / (absβ((absβπ΄) + π΄)))) β β’ ((π΄ β β β§ ((absβπ΄) + π΄) β 0) β ((π΅β2) = π΄ β§ 0 β€ (ββπ΅) β§ (i Β· π΅) β β+)) | ||
Theorem | sqreu 15311* | Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ (π΄ β β β β!π₯ β β ((π₯β2) = π΄ β§ 0 β€ (ββπ₯) β§ (i Β· π₯) β β+)) | ||
Theorem | sqrtcl 15312 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | sqrtthlem 15313 | Lemma for sqrtth 15315. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β (((ββπ΄)β2) = π΄ β§ 0 β€ (ββ(ββπ΄)) β§ (i Β· (ββπ΄)) β β+)) | ||
Theorem | sqrtf 15314 | Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ β:ββΆβ | ||
Theorem | sqrtth 15315 | Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β ((ββπ΄)β2) = π΄) | ||
Theorem | sqrtrege0 15316 | The square root function must make a choice between the two roots, which differ by a sign change. In the general complex case, the choice of "positive" and "negative" is not so clear. The convention we use is to take the root with positive real part, unless π΄ is a nonpositive real (in which case both roots have 0 real part); in this case we take the one in the positive imaginary direction. Another way to look at this is that we choose the root that is largest with respect to lexicographic order on the complex numbers (sorting by real part first, then by imaginary part as tie-breaker). (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β 0 β€ (ββ(ββπ΄))) | ||
Theorem | eqsqrtor 15317 | Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄β2) = π΅ β (π΄ = (ββπ΅) β¨ π΄ = -(ββπ΅)))) | ||
Theorem | eqsqrtd 15318 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄β2) = π΅) & β’ (π β 0 β€ (ββπ΄)) & β’ (π β Β¬ (i Β· π΄) β β+) β β’ (π β π΄ = (ββπ΅)) | ||
Theorem | eqsqrt2d 15319 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄β2) = π΅) & β’ (π β 0 < (ββπ΄)) β β’ (π β π΄ = (ββπ΅)) | ||
Theorem | amgm2 15320 | Arithmetic-geometric mean inequality for π = 2. (Contributed by Mario Carneiro, 2-Jul-2014.) (Proof shortened by AV, 9-Jul-2022.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β (ββ(π΄ Β· π΅)) β€ ((π΄ + π΅) / 2)) | ||
Theorem | sqrtthi 15321 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β β β’ (0 β€ π΄ β ((ββπ΄) Β· (ββπ΄)) = π΄) | ||
Theorem | sqrtcli 15322 | The square root of a nonnegative real is a real. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β β β’ (0 β€ π΄ β (ββπ΄) β β) | ||
Theorem | sqrtgt0i 15323 | The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β β β’ (0 < π΄ β 0 < (ββπ΄)) | ||
Theorem | sqrtmsqi 15324 | Square root of square. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β (ββ(π΄ Β· π΄)) = π΄) | ||
Theorem | sqrtsqi 15325 | Square root of square. (Contributed by NM, 11-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β (ββ(π΄β2)) = π΄) | ||
Theorem | sqsqrti 15326 | Square of square root. (Contributed by NM, 11-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β ((ββπ΄)β2) = π΄) | ||
Theorem | sqrtge0i 15327 | The square root of a nonnegative real is nonnegative. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β β β’ (0 β€ π΄ β 0 β€ (ββπ΄)) | ||
Theorem | absidi 15328 | A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β (absβπ΄) = π΄) | ||
Theorem | absnidi 15329 | A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (π΄ β€ 0 β (absβπ΄) = -π΄) | ||
Theorem | leabsi 15330 | A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ π΄ β€ (absβπ΄) | ||
Theorem | absori 15331 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.) |
β’ π΄ β β β β’ ((absβπ΄) = π΄ β¨ (absβπ΄) = -π΄) | ||
Theorem | absrei 15332 | Absolute value of a real number. (Contributed by NM, 3-Aug-1999.) |
β’ π΄ β β β β’ (absβπ΄) = (ββ(π΄β2)) | ||
Theorem | sqrtpclii 15333 | The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β & β’ 0 < π΄ β β’ (ββπ΄) β β | ||
Theorem | sqrtgt0ii 15334 | The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β & β’ 0 < π΄ β β’ 0 < (ββπ΄) | ||
Theorem | sqrt11i 15335 | The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β ((ββπ΄) = (ββπ΅) β π΄ = π΅)) | ||
Theorem | sqrtmuli 15336 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | sqrtmulii 15337 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β & β’ 0 β€ π΄ & β’ 0 β€ π΅ β β’ (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅)) | ||
Theorem | sqrtmsq2i 15338 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β ((ββπ΄) = π΅ β π΄ = (π΅ Β· π΅))) | ||
Theorem | sqrtlei 15339 | Square root is monotonic. (Contributed by NM, 3-Aug-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β (π΄ β€ π΅ β (ββπ΄) β€ (ββπ΅))) | ||
Theorem | sqrtlti 15340 | Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β (π΄ < π΅ β (ββπ΄) < (ββπ΅))) | ||
Theorem | abslti 15341 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) < π΅ β (-π΅ < π΄ β§ π΄ < π΅)) | ||
Theorem | abslei 15342 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅)) | ||
Theorem | cnsqrt00 15343 | A square root of a complex number is zero iff its argument is 0. Version of sqrt00 15214 for complex numbers. (Contributed by AV, 26-Jan-2023.) |
β’ (π΄ β β β ((ββπ΄) = 0 β π΄ = 0)) | ||
Theorem | absvalsqi 15344 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ ((absβπ΄)β2) = (π΄ Β· (ββπ΄)) | ||
Theorem | absvalsq2i 15345 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2)) | ||
Theorem | abscli 15346 | Real closure of absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (absβπ΄) β β | ||
Theorem | absge0i 15347 | Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ 0 β€ (absβπ΄) | ||
Theorem | absval2i 15348 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | abs00i 15349 | 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, 28-Jul-1999.) |
β’ π΄ β β β β’ ((absβπ΄) = 0 β π΄ = 0) | ||
Theorem | absgt0i 15350 | The absolute value of a nonzero number is positive. Remark in [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.) |
β’ π΄ β β β β’ (π΄ β 0 β 0 < (absβπ΄)) | ||
Theorem | absnegi 15351 | Absolute value of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (absβ-π΄) = (absβπ΄) | ||
Theorem | abscji 15352 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (absβ(ββπ΄)) = (absβπ΄) | ||
Theorem | releabsi 15353 | 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, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββπ΄) β€ (absβπ΄) | ||
Theorem | abssubi 15354 | Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ(π΄ β π΅)) = (absβ(π΅ β π΄)) | ||
Theorem | absmuli 15355 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 1-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ(π΄ Β· π΅)) = ((absβπ΄) Β· (absβπ΅)) | ||
Theorem | sqabsaddi 15356 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβ(π΄ + π΅))β2) = ((((absβπ΄)β2) + ((absβπ΅)β2)) + (2 Β· (ββ(π΄ Β· (ββπ΅))))) | ||
Theorem | sqabssubi 15357 | Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβ(π΄ β π΅))β2) = ((((absβπ΄)β2) + ((absβπ΅)β2)) β (2 Β· (ββ(π΄ Β· (ββπ΅))))) | ||
Theorem | absdivzi 15358 | Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΅ β 0 β (absβ(π΄ / π΅)) = ((absβπ΄) / (absβπ΅))) | ||
Theorem | abstrii 15359 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. This is Metamath 100 proof #91. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ(π΄ + π΅)) β€ ((absβπ΄) + (absβπ΅)) | ||
Theorem | abs3difi 15360 | Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (absβ(π΄ β π΅)) β€ ((absβ(π΄ β πΆ)) + (absβ(πΆ β π΅))) | ||
Theorem | abs3lemi 15361 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ (((absβ(π΄ β πΆ)) < (π· / 2) β§ (absβ(πΆ β π΅)) < (π· / 2)) β (absβ(π΄ β π΅)) < π·) | ||
Theorem | rpsqrtcld 15362 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β+) β β’ (π β (ββπ΄) β β+) | ||
Theorem | sqrtgt0d 15363 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β+) β β’ (π β 0 < (ββπ΄)) | ||
Theorem | absnidd 15364 | A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β€ 0) β β’ (π β (absβπ΄) = -π΄) | ||
Theorem | leabsd 15365 | A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β€ (absβπ΄)) | ||
Theorem | absord 15366 | The absolute value of a real number is either that number or its negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄) = π΄ β¨ (absβπ΄) = -π΄)) | ||
Theorem | absred 15367 | Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) = (ββ(π΄β2))) | ||
Theorem | resqrtcld 15368 | The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββπ΄) β β) | ||
Theorem | sqrtmsqd 15369 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββ(π΄ Β· π΄)) = π΄) | ||
Theorem | sqrtsqd 15370 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββ(π΄β2)) = π΄) | ||
Theorem | sqrtge0d 15371 | The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β 0 β€ (ββπ΄)) | ||
Theorem | sqrtnegd 15372 | The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββ-π΄) = (i Β· (ββπ΄))) | ||
Theorem | absidd 15373 | A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (absβπ΄) = π΄) | ||
Theorem | sqrtdivd 15374 | Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β+) β β’ (π β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | sqrtmuld 15375 | Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | sqrtsq2d 15376 | Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β ((ββπ΄) = π΅ β π΄ = (π΅β2))) | ||
Theorem | sqrtled 15377 | Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (π΄ β€ π΅ β (ββπ΄) β€ (ββπ΅))) | ||
Theorem | sqrtltd 15378 | Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (π΄ < π΅ β (ββπ΄) < (ββπ΅))) | ||
Theorem | sqr11d 15379 | The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) & β’ (π β (ββπ΄) = (ββπ΅)) β β’ (π β π΄ = π΅) | ||
Theorem | absltd 15380 | Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) < π΅ β (-π΅ < π΄ β§ π΄ < π΅))) | ||
Theorem | absled 15381 | Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅))) | ||
Theorem | abssubge0d 15382 | Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΅ β π΄)) = (π΅ β π΄)) | ||
Theorem | abssuble0d 15383 | Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΄ β π΅)) = (π΅ β π΄)) | ||
Theorem | absdifltd 15384 | The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) < πΆ β ((π΅ β πΆ) < π΄ β§ π΄ < (π΅ + πΆ)))) | ||
Theorem | absdifled 15385 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) β€ πΆ β ((π΅ β πΆ) β€ π΄ β§ π΄ β€ (π΅ + πΆ)))) | ||
Theorem | icodiamlt 15386 | Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β (π΄[,)π΅) β§ π· β (π΄[,)π΅))) β (absβ(πΆ β π·)) < (π΅ β π΄)) | ||
Theorem | abscld 15387 | Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) β β) | ||
Theorem | sqrtcld 15388 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | sqrtrege0d 15389 | The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (ββ(ββπ΄))) | ||
Theorem | sqsqrtd 15390 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄)β2) = π΄) | ||
Theorem | msqsqrtd 15391 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄) Β· (ββπ΄)) = π΄) | ||
Theorem | sqr00d 15392 | A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = 0) β β’ (π β π΄ = 0) | ||
Theorem | absvalsqd 15393 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (π΄ Β· (ββπ΄))) | ||
Theorem | absvalsq2d 15394 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | absge0d 15395 | Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (absβπ΄)) | ||
Theorem | absval2d 15396 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2)))) | ||
Theorem | abs00d 15397 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (absβπ΄) = 0) β β’ (π β π΄ = 0) | ||
Theorem | absne0d 15398 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (absβπ΄) β 0) | ||
Theorem | absrpcld 15399 | The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (absβπ΄) β β+) | ||
Theorem | absnegd 15400 | Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβ-π΄) = (absβπ΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |