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

Color key:

Metamath Proof Explorer (1-8757)

Hilbert Space Explorer (8758-10682)

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

Theorem	flwordit 6201	Ordering relationship for the greatest integer function.
$/\$ $/\$

Theorem	flbit 6202	A condition equivalent to floor.
$/\$ $/\$

Theorem	flge0nn0t 6203	The floor of a number greater than or equal to 0 is a nonnegative integer.
$/\$

Theorem	flge1nnt 6204	The floor of a number greater than or equal to 1 is a natural number.
$/\$

Theorem	fladdzt 6205	An integer can be moved in and out of the floor of a sum.
$/\$

Theorem	btwnzge0t 6206	A real bounded between an integer and its successor is nonnegative iff the integer is nonnegative. Second half of Lemma 13-4.1 of [Gleason] p. 217. (For the first half see rebtwnz 6188.)
$/\$ $/\$ $/\$

Theorem	flhalft 6207	Ordering relation for the floor of half of an integer.


Theorem	ceiclt 6208	The ceiling function returns an integer (closure law). (Contributed by Jeffrey Hankins, 10-Jun-2007.)


Theorem	ceiget 6209	The ceiling of a real number is greater than or equal to that number. (Contributed by Jeffrey Hankins, 10-Jun-2007.)


Theorem	ceim1lt 6210	One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeffrey Hankins, 10-Jun-2007.)


Theorem	ceilet 6211	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jeffrey Hankins, 10-Jun-2007.)
$/\$ $/\$

Rational numbers (as a subset of complex numbers)

Definition	df-q 6212	Define the set of rational numbers. Definition of rationals in [Apostol] p. 22.


Theorem	elq 6213	Membership in the set of rationals.


Theorem	znq 6214	The ratio of an integer and a natural number is a rational number.
$/\$

Theorem	qret 6215	A rational number is a real number.


Theorem	zqt 6216	An integer is a rational number.


Theorem	zssq 6217	The integers are a subset of the rationals.


Theorem	nn0ssq 6218	The nonnegative integers are a subset of the rationals.


Theorem	nnssq 6219	The natural numbers are a subset of the rationals.


Theorem	qssre 6220	The rationals are a subset of the reals.


Theorem	qsscn 6221	The rationals are a subset of the complex numbers.


Theorem	nnqt 6222	A natural number is rational.


Theorem	qcnt 6223	A rational number is a complex number.


Theorem	qex 6224	The set of rational numbers exists.


Theorem	qaddclt 6225	Closure of addition of rationals.
$/\$

Theorem	qnegclt 6226	Closure law for the negative of a rational.


Theorem	qmulclt 6227	Closure of multiplication of rationals.
$/\$

Theorem	qsubclt 6228	Closure of subtraction of rationals.
$/\$

Theorem	qrecclt 6229	Closure of reciprocal of rationals.
$/\$

Theorem	qdivclt 6230	Closure of division of rationals.
$/\$ $/\$

Theorem	qrevaddclt 6231	Reverse closure law for addition of rationals.
$/\$

Theorem	nnrecqt 6232	The reciprocal of a natural number is rational.


Theorem	nnrecret 6233	The reciprocal of a natural number is real.


Theorem	qbtwnre 6234	The rational numbers are dense in : any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28.
$/\$ $/\$ $/\$

Theorem	qbtwnxr 6235	The rational numbers are dense in : any two extended real numbers have a rational between them.
$/\$ $/\$ $/\$

Theorem	qsqueeze 6236	If a nonnegative real is less than any positive rational, it is zero.
$/\$ $/\$

Positive reals (as a subset of complex numbers)

Definition	df-rp 6237	Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20.


Theorem	elrp 6238	Membership in the set of positive reals.
$/\$

Theorem	elrpi 6239	Membership in the set of positive reals.


Theorem	rpret 6240	A positive real is a real.


Theorem	rpssre 6241	The positive reals are a subset of the reals.


Theorem	rpgt0t 6242	A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)


Theorem	rpge0t 6243	A positive real is greater than or equal to zero.


Theorem	ralrp 6244	Quantification over positive reals.


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

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

Theorem	rpdivclt 6247	Closure law for multiplication of positive reals. (Contributed by FL, 27-Dec-2007.)
$/\$

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


Monotonic sequences

Theorem	monoord 6249	Ordering relation for a monotonic sequence.
$/\$ $/\$

The infinite sequence builder "seq1"

Theorem	om2uz0 6250	The mapping is a one-to-one mapping from onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number (normally 0 for the upper integers or 1 for the upper integers ), 1 maps to + 1, etc. This theorem shows the value of at ordinal natural number zero. (This series of theorems generalizes an earlier series for contributed by Raph Levien, 10-Apr-2004.)


Theorem	om2uzsuc 6251	The value of (see om2uz0 6250) at a successor.


Theorem	om2uzuz 6252	The value (see om2uz0 6250) at an ordinal natural number is in the upper integers.


Theorem	om2uzlt 6253	Less-than relation for (see om2uz0 6250).
$/\$

Theorem	om2uzlt2 6254	The mapping (see om2uz0 6250) preserves order.
$/\$

Theorem	om2uzran 6255	Range of (see om2uz0 6250).


Theorem	om2uzf1o 6256	(see om2uz0 6250) is a one-to-one onto mapping.


Theorem	uzrdgval 6257	A helper lemma for the value of a recursive definition generator on upper integers (typically either or ) with characteristic function and initial value . Normally is a function on the partition, and is a member of the partition. See also comment in om2uz0 6250.


Theorem	uzrdgini 6258	Initial value of a recursive definition generator on upper integers. See comment in uzrdgval 6257.


Theorem	uzrdgsuc 6259	Successor value of a recursive definition generator on upper integers. See comment in uzrdgval 6257.


Theorem	uzrdginip1 6260	A helper lemma for the value of an or -based recursive definition generator. Value at second index. See comment in uzrdgval 6257.