Home Intuitionistic Logic ExplorerTheorem List (p. 101 of 106) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 10001-10100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremabsltd 10001 Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsled 10002 Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabssubge0d 10003 Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabssuble0d 10004 Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsdifltd 10005 The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsdifled 10006 The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremicodiamlt 10007 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.)

Theoremabscld 10008 Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsvalsqd 10009 Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsvalsq2d 10010 Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsge0d 10011 Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsval2d 10012 Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabs00d 10013 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.)

Theoremabsne0d 10014 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.)

Theoremabsrpclapd 10015 The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
#

Theoremabsnegd 10016 Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabscjd 10017 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.)

Theoremreleabsd 10018 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.)

Theoremabsexpd 10019 Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabssubd 10020 Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsmuld 10021 Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabsdivapd 10022 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
#

Theoremabstrid 10023 Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabs2difd 10024 Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabs2dif2d 10025 Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabs2difabsd 10026 Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabs3difd 10027 Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremabs3lemd 10028 Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)

Theoremqdenre 10029* The rational numbers are dense in : any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 9213. (Contributed by BJ, 15-Oct-2021.)

3.8  Elementary limits and convergence

3.8.1  Limits

Syntaxcli 10030 Extend class notation with convergence relation for limits.

Definitiondf-clim 10031* Define the limit relation for complex number sequences. See clim 10033 for its relational expression. (Contributed by NM, 28-Aug-2005.)

Theoremclimrel 10032 The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim 10033* Express the predicate: The limit of complex number sequence is , or converges to . This means that for any real , no matter how small, there always exists an integer such that the absolute difference of any later complex number in the sequence and the limit is less than . (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Theoremclimcl 10034 Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Theoremclim2 10035* Express the predicate: The limit of complex number sequence is , or converges to , with more general quantifier restrictions than clim 10033. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim2c 10036* Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim0 10037* Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim0c 10038* Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimi 10039* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimi2 10040* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimi0 10041* Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimconst 10042* An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimconst2 10043 A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimz 10044 The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimuni 10045 An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

Theoremfclim 10046 The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremclimdm 10047 Two ways to express that a function has a limit. (The expression is sometimes useful as a shorthand for "the unique limit of the function "). (Contributed by Mario Carneiro, 18-Mar-2014.)

Theoremclimeu 10048* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

Theoremclimreu 10049* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

Theoremclimmo 10050* An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)

Theoremclimeq 10051* Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimmpt 10052* Exhibit a function with the same convergence properties as the not-quite-function . (Contributed by Mario Carneiro, 31-Jan-2014.)

Theorem2clim 10053* If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

Theoremclimshftlemg 10054 A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)

Theoremclimres 10055 A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimshft 10056 A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremiserclim0 10057 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)

Theoremclimshft2 10058* A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)

Theoremclimabs0 10059* Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimcn1 10060* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremclimcn2 10061* Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremaddcn2 10062* Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremsubcn2 10063* Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremmulcn2 10064* Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremcn1lem 10065* A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremabscn2 10066* The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremcjcn2 10067* The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremrecn2 10068* The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremimcn2 10069* The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremclimcn1lem 10070* The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremclimabs 10071* Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimcj 10072* Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimre 10073* Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimim 10074* Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimrecl 10075* The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)

Theoremclimge0 10076* A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)

Theoremclimadd 10077* Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

Theoremclimmul 10078* Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)

Theoremclimsub 10079* Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)

Theoremclimaddc1 10080* Limit of a constant added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimaddc2 10081* Limit of a constant added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimmulc2 10082* Limit of a sequence multiplied by a constant . Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimsubc1 10083* Limit of a constant subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremclimsubc2 10084* Limit of a constant minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimle 10085* Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)

Theoremclimsqz 10086* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimsqz2 10087* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclim2iser 10088* The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)

Theoremclim2iser2 10089* The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)

Theoremiiserex 10090* An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)

Theoremiisermulc2 10091* Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)

Theoremclimlec2 10092* Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)

Theoremiserile 10093* Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)

Theoremiserige0 10094* The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)

Theoremclimub 10095* The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)

Theoremclimserile 10096* The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)

Theoremclimcau 10097* A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 10100). Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)

Theoremclimrecvg1n 10098* A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)

Theoremclimcvg1nlem 10099* Lemma for climcvg1n 10100. We construct sequences of the real and imaginary parts of each term of , show those converge, and use that to show that converges. (Contributed by Jim Kingdon, 24-Aug-2021.)

Theoremclimcvg1n 10100* A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
 Copyright terms: Public domain < Previous  Next >