Home Intuitionistic Logic ExplorerTheorem List (p. 112 of 137) < 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 - 11101-11200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremmax0addsup 11101 The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)

Theoremrexanre 11102* Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)

Theoremrexico 11103* Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)

Theoremmaxclpr 11104 The maximum of two real numbers is one of those numbers if and only if dichotomy ( ) holds. For example, this can be combined with zletric 9194 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.)

Theoremrpmaxcl 11105 The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.)

Theoremzmaxcl 11106 The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.)

Theorem2zsupmax 11107 Two ways to express the maximum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 22-Jan-2023.)

Theoremfimaxre2 11108* A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)

Theoremnegfi 11109* The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.)

4.7.6  The minimum of two real numbers

Theoremmincom 11110 The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.)
inf inf

Theoremminmax 11111 Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 8-Feb-2021.)
inf

Theoremmincl 11112 The minumum of two real numbers is a real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
inf

Theoremmin1inf 11113 The minimum of two numbers is less than or equal to the first. (Contributed by Jim Kingdon, 8-Feb-2021.)
inf

Theoremmin2inf 11114 The minimum of two numbers is less than or equal to the second. (Contributed by Jim Kingdon, 9-Feb-2021.)
inf

Theoremlemininf 11115 Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.)
inf

Theoremltmininf 11116 Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.)
inf

Theoremminabs 11117 The minimum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 15-May-2023.)
inf

Theoremminclpr 11118 The minimum of two real numbers is one of those numbers if and only if dichotomy ( ) holds. For example, this can be combined with zletric 9194 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 23-May-2023.)
inf

Theoremrpmincl 11119 The minumum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
inf

Theorembdtrilem 11120 Lemma for bdtri 11121. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.)

Theorembdtri 11121 Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.)
inf inf inf

Theoremmul0inf 11122 Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 10944 and mulap0bd 8514 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.)
inf

4.7.7  The maximum of two extended reals

Theoremxrmaxleim 11123 Value of maximum when we know which extended real is larger. (Contributed by Jim Kingdon, 25-Apr-2023.)

Theoremxrmaxiflemcl 11124 Lemma for xrmaxif 11130. Closure. (Contributed by Jim Kingdon, 29-Apr-2023.)

Theoremxrmaxifle 11125 An upper bound for in the extended reals. (Contributed by Jim Kingdon, 26-Apr-2023.)

Theoremxrmaxiflemab 11126 Lemma for xrmaxif 11130. A variation of xrmaxleim 11123- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 26-Apr-2023.)

Theoremxrmaxiflemlub 11127 Lemma for xrmaxif 11130. A least upper bound for . (Contributed by Jim Kingdon, 28-Apr-2023.)

Theoremxrmaxiflemcom 11128 Lemma for xrmaxif 11130. Commutativity of an expression which we will later show to be the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)

Theoremxrmaxiflemval 11129* Lemma for xrmaxif 11130. Value of the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)

Theoremxrmaxif 11130 Maximum of two extended reals in terms of expressions. (Contributed by Jim Kingdon, 26-Apr-2023.)

Theoremxrmaxcl 11131 The maximum of two extended reals is an extended real. (Contributed by Jim Kingdon, 29-Apr-2023.)

Theoremxrmax1sup 11132 An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)

Theoremxrmax2sup 11133 An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)

Theoremxrmaxrecl 11134 The maximum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.)

Theoremxrmaxleastlt 11135 The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)

Theoremxrltmaxsup 11136 The maximum as a least upper bound. (Contributed by Jim Kingdon, 10-May-2023.)

Theoremxrmaxltsup 11137 Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 30-Apr-2023.)

Theoremxrmaxlesup 11138 Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 10-May-2023.)

Theoremxrmaxaddlem 11139 Lemma for xrmaxadd 11140. The case where is real. (Contributed by Jim Kingdon, 11-May-2023.)

4.7.8  The minimum of two extended reals

Theoremxrnegiso 11141 Negation is an order anti-isomorphism of the extended reals, which is its own inverse. (Contributed by Jim Kingdon, 2-May-2023.)

Theoreminfxrnegsupex 11142* The infimum of a set of extended reals is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 2-May-2023.)
inf

Theoremxrnegcon1d 11143 Contraposition law for extended real unary minus. (Contributed by Jim Kingdon, 2-May-2023.)

Theoremxrminmax 11144 Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 2-May-2023.)
inf

Theoremxrmincl 11145 The minumum of two extended reals is an extended real. (Contributed by Jim Kingdon, 3-May-2023.)
inf

Theoremxrmin1inf 11146 The minimum of two extended reals is less than or equal to the first. (Contributed by Jim Kingdon, 3-May-2023.)
inf

Theoremxrmin2inf 11147 The minimum of two extended reals is less than or equal to the second. (Contributed by Jim Kingdon, 3-May-2023.)
inf

Theoremxrmineqinf 11148 The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim Kingdon, 3-May-2023.)
inf

Theoremxrltmininf 11149 Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 3-May-2023.)
inf

Theoremxrlemininf 11150 Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 4-May-2023.)
inf

Theoremxrminltinf 11151 Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.)
inf

Theoremxrminrecl 11152 The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.)
inf inf

Theoremxrminrpcl 11153 The minimum of two positive reals is a positive real. (Contributed by Jim Kingdon, 4-May-2023.)
inf

inf inf

Theoremxrbdtri 11155 Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.)
inf inf inf

Theoremiooinsup 11156 Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.)
inf

4.8  Elementary limits and convergence

4.8.1  Limits

Syntaxcli 11157 Extend class notation with convergence relation for limits.

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

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

Theoremclim 11160* 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 11161 Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

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

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

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

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

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

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

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

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

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

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

Theoremclimuni 11172 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 11173 The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremclimdm 11174 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 11175* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

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

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

Theoremclimeq 11178* 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 11179* Exhibit a function with the same convergence properties as the not-quite-function . (Contributed by Mario Carneiro, 31-Jan-2014.)

Theorem2clim 11180* 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 11181 A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)

Theoremclimres 11182 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 11183 A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremserclim0 11184 The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

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

Theoremclimabs0 11186* 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 11187* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)

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

Theoremaddcn2 11189* 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 addcncntop 12912 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremsubcn2 11190* 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 11191* Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremreccn2ap 11192* The reciprocal function is continuous. The class is just for convenience in writing the proof and typically would be passed in as an instance of eqid 2157. (Contributed by Mario Carneiro, 9-Feb-2014.) Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.)
inf        # #

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

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

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

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

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

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

Theoremclimabs 11199* 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 11200* 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.)

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-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13615
 Copyright terms: Public domain < Previous  Next >