mmtheorems63 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

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-12229

Color key:

Metamath Proof Explorer
(1-9062)

Hilbert Space Explorer
(9063-10650)

Users' Mathboxes
(10651-12229)

**Statement List for Metamath Proof Explorer -** 6201-6300 - Page 63 of 123
Type	Label	Description
Statement

Theorem	rpregt0 6201	A positive real is a positive real number.
$/\$

Theorem	rpne0 6202	A positive real is nonzero.


Theorem	rprene0 6203	A positive real is a nonzero real number.
$/\$

Theorem	rpcnne0 6204	A positive real is a nonzero complex number.
$/\$

Theorem	ralrp 6205	Quantification over positive reals.


Theorem	rpaddcl 6206	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20.
$/\$

Theorem	rpmulcl 6207	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20.
$/\$

Theorem	rpdivcl 6208	Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
$/\$

Theorem	rpreccl 6209	Closure law for reciprocation of positive reals. (Contributed by Jeffrey Hankins, 23-Nov-2008.)


Theorem	rerpdivcl 6210	Closure law for division of a real by a positive real.
$/\$

Theorem	rpneg 6211	Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of [Apostol] p. 20.
$/\$

Theorem	0nrp 6212	Zero is not a positive real. Axiom 9 of [Apostol] p. 20.


Completeness Axiom and Suprema

Theorem	lbreu 6213	If a set of reals contains a lower bound, it contains a unique lower bound.
$/\$

Theorem	lbcl 6214	If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set.
$/\$

Theorem	lble 6215	If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set.
$/\$ $/\$

Theorem	lbinfm 6216	If a set of reals contains a lower bound, the lower bound is its infimum.
$/\$

Theorem	lbinfmcl 6217	If a set of reals contains a lower bound, it contains its infimum.
$/\$

Theorem	lbinfmle 6218	If a set of reals contains a lower bound, its infmimum is less than or equal to all members of the set.
$/\$ $/\$

Theorem	sup2 6219	A non-empty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent).
$/\$ $/\$ $\/$ $/\$

Theorem	sup3 6220	A version of the completeness axiom for reals.
$/\$ $/\$ $/\$

Theorem	infm3lem 6221	Lemma for infm3 6222.

Theorem	infm3 6222	The completeness axiom for reals in terms of infimum: a non-empty, bounded-below set of reals has a infimum. (This theorem is the dual of sup3 6220.)
$/\$ $/\$ $/\$

Theorem	suprcl 6223	Closure of supremum of a non-empty bounded set of reals.
$/\$ $/\$

Theorem	suprub 6224	A member of a non-empty bounded set of reals is less than or equal to the set's upper bound.
$/\$ $/\$ $/\$

Theorem	suprlub 6225	The supremum of a non-empty bounded set of reals is the least upper bound.
$/\$ $/\$ $/\$ $/\$

Theorem	suprnub 6226	An upper bound is not less than the supremum of a non-empty bounded set of reals.
$/\$ $/\$ $/\$ $/\$

Theorem	suprleub 6227	The supremum of a non-empty bounded set of reals is less than or equal to an upper bound.
$/\$ $/\$ $/\$ $/\$

Theorem	sup3ii 6228	A version of the completeness axiom for reals.
$/\$ $/\$ $/\$

Theorem	suprclii 6229	Closure of supremum of a non-empty bounded set of reals.
$/\$ $/\$

Theorem	suprubii 6230	A member of a non-empty bounded set of reals is less than or equal to the set's upper bound.
$/\$ $/\$

Theorem	suprlubii 6231	The supremum of a non-empty bounded set of reals is the least upper bound.
$/\$ $/\$ $/\$

Theorem	suprnubii 6232	An upper bound is not less than the supremum of a non-empty bounded set of reals.
$/\$ $/\$ $/\$

Theorem	suprleubii 6233	The supremum of a non-empty bounded set of reals is less than or equal to an upper bound.
$/\$ $/\$ $/\$

Theorem	reuuninegi 6234	The negative of the unique real such that .


Theorem	dfinfmr 6235	The infimum (expressed as supremum with converse 'less-than') of a set of reals .
$/\$

Theorem	infmsup 6236	The infimum (expressed as supremum with converse 'less-than') of a set of reals is the negative of the supremum of the negatives of its elements. The antecedent ensures that is nonempty and has a lower bound.
$/\$ $/\$

Theorem	infmrcl 6237	Closure of infimum of a non-empty bounded set of reals.
$/\$ $/\$

Theorem	nnunb 6238	The set of natural numbers is unbounded above. Theorem I.28 of [Apostol] p. 26.
$\/$

Theorem	arch 6239	Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26.


Theorem	nnrecl 6240	There exists a natural number whose reciprocal is less than a given positive real. Exercise 3 of [Apostol] p. 28.
$/\$

Theorem	bndndx 6241	A bounded real sequence is less than or equal to at least one of its indices.
$/\$

Supremum on the extended reals

Theorem	xrsupexmnf 6242	Adding minus infinity to a set does not affect the existence of its supremum.
$/\$ $/\$

Theorem	xrinfmexpnf 6243	Adding plus infinity to a set does not affect the existence of its infimum.
$/\$ $/\$

Theorem	xrsupsslem 6244	Lemma for xrsupss 6246.

Theorem	xrinfmsslem 6245	Lemma for xrinfmss 6247.

Theorem	xrsupss 6246	Any subset of extended reals has a supremum.
$/\$

Theorem	xrinfmss 6247	Any subset of extended reals has an infimum.
$/\$

Theorem	xrub 6248	By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals.
$/\$

Theorem	supxr 6249	The supremum of a set of extended reals.
$/\$ $/\$ $/\$

Theorem	supxr2 6250	The supremum of a set of extended reals.
$/\$ $/\$ $/\$

Theorem	supxrre 6251	The real and extended real suprema match when the real supremum exists.
$/\$ $/\$

Theorem	supxrcl 6252	The supremum of an arbitrary set of extended reals is an extended real.


Theorem	supxrun 6253	The supremum of the union of two sets of extended reals equals the largest of their suprema.
$/\$ $/\$

Theorem	infmxrcl 6254	The infimum of an arbitrary set of extended reals is an extended real.


Theorem	supxrmnf 6255	Adding minus infinity to a set does not affect its supremum.


Theorem	supxrpnf 6256	The supremum of a set of extended reals containing plus infnity is plus infinity.
$/\$

Theorem	supxrunb1 6257	The supremum of an unbounded-above set of extended reals is plus infinity.


Theorem	supxrunb2 6258	The supremum of an unbounded-above set of extended reals is plus infinity.


Theorem	supxrbnd 6259	The supremum of a bounded-above nonempty set of reals is real.
$/\$ $/\$

Theorem	supxrgtmnf 6260	The supremum of a nonempty set of reals is greater than minus infinity.
$/\$

Theorem	supxrre1 6261	The supremum of a nonempty set of reals is real iff it is less than plus infinity.
$/\$

Theorem	supxrre2 6262	The supremum of a nonempty set of reals is real iff it is not plus infinity.
$/\$

Theorem	supxrbnd1 6263	The supremum of a bounded-above set of extended reals is less than infinity.


Theorem	supxrbnd2 6264	The supremum of a bounded-above set of extended reals is less than infinity.


Theorem	xrsup0 6265	The supremum of an empty set under the extended reals is minus infinity.


Theorem	supxrub 6266	A member of a set of extended reals is less than or equal to the set's supremum.
$/\$

Theorem	supxrleub 6267	The supremum of a set of extended reals is less than or equal to an upper bound.
$/\$ $/\$

Nonnegative integers (as a subset of complex numbers)

Definition	df-n0 6268	Define the set of nonnegative integers.


Theorem	elnn0 6269	Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)
$\/$

Theorem	nnssnn0 6270	Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	nn0ssre 6271	Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	nn0sscn 6272	Nonnegative integers are a subset of the complex numbers.)


Theorem	nn0ex 6273	The set of nonnegative integers exists.


Theorem	nnnn0 6274	A natural number is a nonnegative integer.


Theorem	nnnn0i 6275	A natural number is a nonnegative integer.


Theorem	nn0re 6276	A nonnegative integer is a real number.


Theorem	nn0cn 6277	A nonnegative integer is a complex number.


Theorem	nn0rei 6278	A nonnegative integer is a real number.


Theorem	nn0cni 6279	A nonnegative integer is a complex number.


Theorem	dfn2 6280	The set of natural numbers (positive integers) defined in terms of nonnegative integers.


Theorem	0nn0 6281	0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	1nn0 6282	1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	2nn0 6283	2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	lt0nnn0 6284	No number less than zero is a nonnegative integer.
$/\$

Theorem	nn0ge0 6285	A nonnegative integer is greater than or equal to zero.


Theorem	nn0ge0i 6286	Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	nn0le0eq0 6287	A nonnegative integer is less than or equal to zero iff it is equal to zero.


Theorem	nn0addcl 6288	Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
$/\$

Theorem	nn0addcli 6289	Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	nn0mulcli 6290	Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)


Theorem	nn0mulcl 6291	Closure of multiplication of nonnegative integers.
$/\$

Theorem	peano2nn0 6292	Second Peano postulate for nonnegative integers.


Theorem	nnnn0addcl 6293	A natural number plus a nonnegative integer is a natural number.
$/\$

Theorem	nn0nnaddcl 6294	A nonnegative integer plus a natural number is a natural number.
$/\$

Theorem	nn0ltp1le 6295	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.)
$/\$

Theorem	nn0leltp1 6296	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
$/\$

Theorem	nn0ltlem1 6297	Nonnegative integer ordering relation.
$/\$

Theorem	nn0addge1 6298	A number is less than or equal to itself plus a nonnegative integer.
$/\$

Theorem	nn0addge2 6299	A number is less than or equal to itself plus a nonnegative integer.
$/\$

Theorem	nn0addge1i 6300	A number is less than or equal to itself plus a nonnegative integer.

MPE Home Contents

< Previous Next >