![]() |
Metamath
Proof Explorer Theorem List (p. 154 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-30159) |
![]() (30160-31682) |
![]() (31683-47806) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | caubnd2 15301* | A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ¦ β β βπ β π βπ β (β€β₯βπ)(absβ(πΉβπ)) < π¦) | ||
Theorem | caubnd 15302* | 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 15303 | Lemma for sqreu 15304: 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 15304* | Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ (π΄ β β β β!π₯ β β ((π₯β2) = π΄ β§ 0 β€ (ββπ₯) β§ (i Β· π₯) β β+)) | ||
Theorem | sqrtcl 15305 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | sqrtthlem 15306 | Lemma for sqrtth 15308. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β (((ββπ΄)β2) = π΄ β§ 0 β€ (ββ(ββπ΄)) β§ (i Β· (ββπ΄)) β β+)) | ||
Theorem | sqrtf 15307 | Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ β:ββΆβ | ||
Theorem | sqrtth 15308 | Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ (π΄ β β β ((ββπ΄)β2) = π΄) | ||
Theorem | sqrtrege0 15309 | 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 15310 | Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄β2) = π΅ β (π΄ = (ββπ΅) β¨ π΄ = -(ββπ΅)))) | ||
Theorem | eqsqrtd 15311 | 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 15312 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄β2) = π΅) & β’ (π β 0 < (ββπ΄)) β β’ (π β π΄ = (ββπ΅)) | ||
Theorem | amgm2 15313 | 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 15314 | 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 15315 | 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 15316 | 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 15317 | Square root of square. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β (ββ(π΄ Β· π΄)) = π΄) | ||
Theorem | sqrtsqi 15318 | Square root of square. (Contributed by NM, 11-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β (ββ(π΄β2)) = π΄) | ||
Theorem | sqsqrti 15319 | Square of square root. (Contributed by NM, 11-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β ((ββπ΄)β2) = π΄) | ||
Theorem | sqrtge0i 15320 | 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 15321 | A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (0 β€ π΄ β (absβπ΄) = π΄) | ||
Theorem | absnidi 15322 | A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (π΄ β€ 0 β (absβπ΄) = -π΄) | ||
Theorem | leabsi 15323 | A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ π΄ β€ (absβπ΄) | ||
Theorem | absori 15324 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.) |
β’ π΄ β β β β’ ((absβπ΄) = π΄ β¨ (absβπ΄) = -π΄) | ||
Theorem | absrei 15325 | Absolute value of a real number. (Contributed by NM, 3-Aug-1999.) |
β’ π΄ β β β β’ (absβπ΄) = (ββ(π΄β2)) | ||
Theorem | sqrtpclii 15326 | The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.) |
β’ π΄ β β & β’ 0 < π΄ β β’ (ββπ΄) β β | ||
Theorem | sqrtgt0ii 15327 | 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 15328 | The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β ((ββπ΄) = (ββπ΅) β π΄ = π΅)) | ||
Theorem | sqrtmuli 15329 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | sqrtmulii 15330 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β & β’ 0 β€ π΄ & β’ 0 β€ π΅ β β’ (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅)) | ||
Theorem | sqrtmsq2i 15331 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β ((ββπ΄) = π΅ β π΄ = (π΅ Β· π΅))) | ||
Theorem | sqrtlei 15332 | Square root is monotonic. (Contributed by NM, 3-Aug-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β (π΄ β€ π΅ β (ββπ΄) β€ (ββπ΅))) | ||
Theorem | sqrtlti 15333 | Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ ((0 β€ π΄ β§ 0 β€ π΅) β (π΄ < π΅ β (ββπ΄) < (ββπ΅))) | ||
Theorem | abslti 15334 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) < π΅ β (-π΅ < π΄ β§ π΄ < π΅)) | ||
Theorem | abslei 15335 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅)) | ||
Theorem | cnsqrt00 15336 | A square root of a complex number is zero iff its argument is 0. Version of sqrt00 15207 for complex numbers. (Contributed by AV, 26-Jan-2023.) |
β’ (π΄ β β β ((ββπ΄) = 0 β π΄ = 0)) | ||
Theorem | absvalsqi 15337 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ ((absβπ΄)β2) = (π΄ Β· (ββπ΄)) | ||
Theorem | absvalsq2i 15338 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2)) | ||
Theorem | abscli 15339 | Real closure of absolute value. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (absβπ΄) β β | ||
Theorem | absge0i 15340 | Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ 0 β€ (absβπ΄) | ||
Theorem | absval2i 15341 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | abs00i 15342 | 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 15343 | 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 15344 | Absolute value of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (absβ-π΄) = (absβπ΄) | ||
Theorem | abscji 15345 | 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 15346 | 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 15347 | 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 15348 | 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 15349 | 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 15350 | Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.) |
β’ π΄ β β & β’ π΅ β β β β’ ((absβ(π΄ β π΅))β2) = ((((absβπ΄)β2) + ((absβπ΅)β2)) β (2 Β· (ββ(π΄ Β· (ββπ΅))))) | ||
Theorem | absdivzi 15351 | Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΅ β 0 β (absβ(π΄ / π΅)) = ((absβπ΄) / (absβπ΅))) | ||
Theorem | abstrii 15352 | 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 15353 | Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (absβ(π΄ β π΅)) β€ ((absβ(π΄ β πΆ)) + (absβ(πΆ β π΅))) | ||
Theorem | abs3lemi 15354 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ (((absβ(π΄ β πΆ)) < (π· / 2) β§ (absβ(πΆ β π΅)) < (π· / 2)) β (absβ(π΄ β π΅)) < π·) | ||
Theorem | rpsqrtcld 15355 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β+) β β’ (π β (ββπ΄) β β+) | ||
Theorem | sqrtgt0d 15356 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β+) β β’ (π β 0 < (ββπ΄)) | ||
Theorem | absnidd 15357 | A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β€ 0) β β’ (π β (absβπ΄) = -π΄) | ||
Theorem | leabsd 15358 | A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ β€ (absβπ΄)) | ||
Theorem | absord 15359 | 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 15360 | Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) = (ββ(π΄β2))) | ||
Theorem | resqrtcld 15361 | The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββπ΄) β β) | ||
Theorem | sqrtmsqd 15362 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββ(π΄ Β· π΄)) = π΄) | ||
Theorem | sqrtsqd 15363 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββ(π΄β2)) = π΄) | ||
Theorem | sqrtge0d 15364 | The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β 0 β€ (ββπ΄)) | ||
Theorem | sqrtnegd 15365 | The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (ββ-π΄) = (i Β· (ββπ΄))) | ||
Theorem | absidd 15366 | A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (absβπ΄) = π΄) | ||
Theorem | sqrtdivd 15367 | Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β+) β β’ (π β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | sqrtmuld 15368 | Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | sqrtsq2d 15369 | Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β ((ββπ΄) = π΅ β π΄ = (π΅β2))) | ||
Theorem | sqrtled 15370 | Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (π΄ β€ π΅ β (ββπ΄) β€ (ββπ΅))) | ||
Theorem | sqrtltd 15371 | Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (π΄ < π΅ β (ββπ΄) < (ββπ΅))) | ||
Theorem | sqr11d 15372 | The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) & β’ (π β (ββπ΄) = (ββπ΅)) β β’ (π β π΄ = π΅) | ||
Theorem | absltd 15373 | Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) < π΅ β (-π΅ < π΄ β§ π΄ < π΅))) | ||
Theorem | absled 15374 | Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅))) | ||
Theorem | abssubge0d 15375 | Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΅ β π΄)) = (π΅ β π΄)) | ||
Theorem | abssuble0d 15376 | Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΄ β π΅)) = (π΅ β π΄)) | ||
Theorem | absdifltd 15377 | The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) < πΆ β ((π΅ β πΆ) < π΄ β§ π΄ < (π΅ + πΆ)))) | ||
Theorem | absdifled 15378 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) β€ πΆ β ((π΅ β πΆ) β€ π΄ β§ π΄ β€ (π΅ + πΆ)))) | ||
Theorem | icodiamlt 15379 | 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 15380 | Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) β β) | ||
Theorem | sqrtcld 15381 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | sqrtrege0d 15382 | The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (ββ(ββπ΄))) | ||
Theorem | sqsqrtd 15383 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄)β2) = π΄) | ||
Theorem | msqsqrtd 15384 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄) Β· (ββπ΄)) = π΄) | ||
Theorem | sqr00d 15385 | A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = 0) β β’ (π β π΄ = 0) | ||
Theorem | absvalsqd 15386 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (π΄ Β· (ββπ΄))) | ||
Theorem | absvalsq2d 15387 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | absge0d 15388 | Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (absβπ΄)) | ||
Theorem | absval2d 15389 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2)))) | ||
Theorem | abs00d 15390 | 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 15391 | 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 15392 | The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (absβπ΄) β β+) | ||
Theorem | absnegd 15393 | Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβ-π΄) = (absβπ΄)) | ||
Theorem | abscjd 15394 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβ(ββπ΄)) = (absβπ΄)) | ||
Theorem | releabsd 15395 | 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 Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β€ (absβπ΄)) | ||
Theorem | absexpd 15396 | Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β (absβ(π΄βπ)) = ((absβπ΄)βπ)) | ||
Theorem | abssubd 15397 | Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ β π΅)) = (absβ(π΅ β π΄))) | ||
Theorem | absmuld 15398 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ Β· π΅)) = ((absβπ΄) Β· (absβπ΅))) | ||
Theorem | absdivd 15399 | Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) β β’ (π β (absβ(π΄ / π΅)) = ((absβπ΄) / (absβπ΅))) | ||
Theorem | abstrid 15400 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ + π΅)) β€ ((absβπ΄) + (absβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |