mmtheorems62 - Metamath Proof Explorer

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

Statement List for Metamath Proof Explorer - 6101-6200 - Page 62 of 108

Type	Label	Description
Statement
Theorem	supxrleub 6101	The supremum of a set of extended reals is less than or equal to an upper bound.
|- ((A (_ RR* /\ B e. RR* /\ A.x e. A x <_ B) -> sup(A, RR*, < ) <_ B)
Nonnegative integers (as a subset of complex numbers)
Definition	df-n0 6102	Define the set of nonnegative integers.
|- NN0 = (NN u. {0})
Theorem	elnn0 6103	Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)
|- (A e. NN0 <-> (A e. NN \/ A = 0))
Theorem	nnssnn0 6104	Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
|- NN (_ NN0
Theorem	nn0ssre 6105	Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002.)
|- NN0 (_ RR
Theorem	nn0sscn 6106	Nonnegative integers are a subset of the complex numbers.)
|- NN0 (_ CC
Theorem	nn0ex 6107	The set of nonnegative integers exists.
|- NN0 e. V
Theorem	nnnn0t 6108	A natural number is a nonnegative integer.
|- (A e. NN -> A e. NN0)
Theorem	nnnn0 6109	A natural number is a nonnegative integer.
|- N e. NN   =>   |- N e. NN0
Theorem	nn0ret 6110	A nonnegative integer is a real number.
|- (A e. NN0 -> A e. RR)
Theorem	nn0cnt 6111	A nonnegative integer is a complex number.
|- (A e. NN0 -> A e. CC)
Theorem	nn0re 6112	A nonnegative integer is a real number.
|- A e. NN0   =>   |- A e. RR
Theorem	nn0cn 6113	A nonnegative integer is a complex number.
|- A e. NN0   =>   |- A e. CC
Theorem	dfn2 6114	The set of natural numbers (positive integers) defined in terms of nonnegative integers.
|- NN = (NN0 \ {0})
Theorem	0nn0 6115	0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|- 0 e. NN0
Theorem	1nn0 6116	1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|- 1 e. NN0
Theorem	2nn0 6117	2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
|- 2 e. NN0
Theorem	lt0nnn0 6118	No number less than zero is a nonnegative integer.
|- ((A e. RR /\ A < 0) -> -. A e. NN0)
Theorem	nn0ge0t 6119	A nonnegative integer is greater than or equal to zero.
|- (N e. NN0 -> 0 <_ N)
Theorem	nn0ge0 6120	Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.)
|- N e. NN0   =>   |- 0 <_ N
Theorem	nn0le0eq0t 6121	A nonnegative integer is less than or equal to zero iff it is equal to zero.
|- (N e. NN0 -> (N <_ 0 <-> N = 0))
Theorem	nn0addclt 6122	Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
|- ((M e. NN0 /\ N e. NN0) -> (M + N) e. NN0)
Theorem	nn0addcl 6123	Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)
|- M e. NN0   &   |- N e. NN0   =>   |- (M + N) e. NN0
Theorem	nn0mulcl 6124	Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)
|- M e. NN0   &   |- N e. NN0   =>   |- (M x. N) e. NN0
Theorem	nn0mulclt 6125	Closure of multiplication of nonnegative integers.
|- ((M e. NN0 /\ N e. NN0) -> (M x. N) e. NN0)
Theorem	peano2nn0 6126	Second Peano postulate for nonnegative integers.
|- (N e. NN0 -> (N + 1) e. NN0)
Theorem	nnnn0addclt 6127	A natural number plus a nonnegative integer is a natural number.
|- ((M e. NN /\ N e. NN0) -> (M + N) e. NN)
Theorem	nn0nnaddclt 6128	A nonnegative integer plus a natural number is a natural number.
|- ((M e. NN0 /\ N e. NN) -> (M + N) e. NN)
Theorem	nn0ltp1let 6129	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.)
|- ((M e. NN0 /\ N e. NN0) -> (M < N <-> (M + 1) <_ N))
Theorem	nn0leltp1t 6130	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
|- ((M e. NN0 /\ N e. NN0) -> (M <_ N <-> M < (N + 1)))
Theorem	nn0ltlem1t 6131	Nonnegative integer ordering relation.
|- ((M e. NN0 /\ N e. NN0) -> (M < N <-> M <_ (N - 1)))
Theorem	nn0addge1t 6132	A number is less than or equal to itself plus a nonnegative integer.
|- ((A e. RR /\ N e. NN0) -> A <_ (A + N))
Theorem	nn0addge2t 6133	A number is less than or equal to itself plus a nonnegative integer.
|- ((A e. RR /\ N e. NN0) -> A <_ (N + A))
Theorem	nn0addge1 6134	A number is less than or equal to itself plus a nonnegative integer.
|- A e. RR   &   |- N e. NN0   =>   |- A <_ (A + N)
Theorem	nn0addge2 6135	A number is less than or equal to itself plus a nonnegative integer.
|- A e. RR   &   |- N e. NN0   =>   |- A <_ (N + A)
Theorem	nn0le2x 6136	A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)
|- N e. NN0   =>   |- N <_ (2 x. N)
Theorem	nn0lele2x 6137	'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
|- M e. NN0   &   |- N e. NN0   =>   |- (N <_ M -> N <_ (2 x. M))
Integers (as a subset of complex numbers)
Definition	df-z 6138	Define the set of integers. Definition of integers in [Apostol] p. 22.
|- ZZ = {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}
Theorem	elz 6139	Membership in the set of integers.
|- (N e. ZZ <-> (N e. RR /\ (N = 0 \/ N e. NN \/ -uN e. NN)))
Theorem	nnnegz 6140	The negative of a natural number is an integer.
|- (N e. NN -> -uN e. ZZ)
Theorem	zret 6141	An integer is a real.
|- (N e. ZZ -> N e. RR)
Theorem	zcnt 6142	An integer is a complex number.
|- (N e. ZZ -> N e. CC)
Theorem	zre 6143	An integer is a real number.
|- A e. ZZ   =>   |- A e. RR
Theorem	zssre 6144	The integers are a subset of the reals.
|- ZZ (_ RR
Theorem	zsscn 6145	The integers are a subset of the complex numbers.
|- ZZ (_ CC
Theorem	zex 6146	The set of integers exists.
|- ZZ e. V
Theorem	elnnz 6147	Natural number property expressed in terms of integers.
|- (N e. NN <-> (N e. ZZ /\ 0 < N))
Theorem	0z 6148	Zero is an integer.
|- 0 e. ZZ
Theorem	elnn0z 6149	Nonnegative integer property expressed in terms of integers.
|- (N e. NN0 <-> (N e. ZZ /\ 0 <_ N))
Theorem	elznn0nn 6150	Integer property expressed in terms nonnegative integers and natural numbers.
|- (N e. ZZ <-> (N e. NN0 \/ (N e. RR /\ -uN e. NN)))
Theorem	elznn0 6151	Integer property expressed in terms of nonnegative integers.
|- (N e. ZZ <-> (N e. RR /\ (N e. NN0 \/ -uN e. NN0)))
Theorem	elznn 6152	Integer property expressed in terms natural numbers and nonnegative integers.
|- (N e. ZZ <-> (N e. RR /\ (N e. NN \/ -uN e. NN0)))
Theorem	nnssz 6153	Natural numbers are a subset of integers.
|- NN (_ ZZ
Theorem	nn0ssz 6154	Nonnegative integers are a subset of the integers.
|- NN0 (_ ZZ
Theorem	nnzt 6155	A natural number is an integer.
|- (N e. NN -> N e. ZZ)
Theorem	nn0zt 6156	A nonnegative integer is an integer.
|- (N e. NN0 -> N e. ZZ)
Theorem	elnnz1 6157	Natural number property expressed in terms of integers.
|- (N e. NN <-> (N e. ZZ /\ 1 <_ N))
Theorem	znnnlt1t 6158	An integer is not a natural number iff it is less than one.
|- (N e. ZZ -> (-. N e. NN <-> N < 1))
Theorem	nnzrab 6159	Natural numbers expressed as a subset of integers.
|- NN = {x e. ZZ | 1 <_ x}
Theorem	nn0zrab 6160	Nonnegative integers expressed as a subset of integers.
|- NN0 = {x e. ZZ | 0 <_ x}
Theorem	1z 6161	One is an integer.
|- 1 e. ZZ
Theorem	2z 6162	Two is an integer.
|- 2 e. ZZ
Theorem	nn0subt 6163	Subtraction of nonnegative integers.
|- ((M e. NN0 /\ N e. NN0) -> (M <_ N <-> (N - M) e. NN0))
Theorem	nn0sub2t 6164	Subtraction of nonnegative integers.
|- ((M e. NN0 /\ N e. NN0 /\ M <_ N) -> (N - M) e. NN0)
Theorem	znegclt 6165	Closure law for negative integers.
|- (N e. ZZ -> -uN e. ZZ)
Theorem	nn0negz 6166	The negative of a nonnegative integer is an integer.
|- (N e. NN0 -> -uN e. ZZ)
Theorem	zaddclt 6167	Closure of addition of integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M + N) e. ZZ)
Theorem	peano2z 6168	Second Peano postulate generalized to integers.
|- (N e. ZZ -> (N + 1) e. ZZ)
Theorem	peano2zd 6169	Deduction from second Peano postulate generalized to integers.
|- (ph -> N e. ZZ)   =>   |- (ph -> (N + 1) e. ZZ)
Theorem	zsubclt 6170	Closure of subtraction of integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M - N) e. ZZ)
Theorem	peano2zm 6171	"Reverse" second Peano postulate for integers.
|- (N e. ZZ -> (N - 1) e. ZZ)
Theorem	zrevaddclt 6172	Reverse closure law for addition of integers.
|- (N e. ZZ -> ((M e. CC /\ (M + N) e. ZZ) <-> M e. ZZ))
Theorem	elnn0nn 6173	The nonnegative integer property expressed in terms of natural numbers.
|- (N e. NN0 <-> (N e. CC /\ (N + 1) e. NN))
Theorem	elnnnn0 6174	The natural number property expressed in terms of nonnegative integers.
|- (N e. NN <-> (N e. CC /\ (N - 1) e. NN0))
Theorem	elnnnn0b 6175	The natural number property expressed in terms of nonnegative integers.
|- (N e. NN <-> (N e. NN0 /\ 0 < N))
Theorem	elnnnn0c 6176	The natural number property expressed in terms of nonnegative integers.
|- (N e. NN <-> (N e. NN0 /\ 1 <_ N))
Theorem	nn0p1nnt 6177	A nonnegative integer plus 1 is a natural number. (Contributed by Raph Levien, 30-Jun-2006.)
|- (N e. NN0 -> (N + 1) e. NN)
Theorem	nnm1nn0t 6178	A natural number minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.)
|- (N e. NN -> (N - 1) e. NN0)
Theorem	znnsubt 6179	The positive difference of unequal integers is a natural number. (Generalization of nnsubt 5959.)
|- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> (N - M) e. NN))
Theorem	znn0subt 6180	The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0subt 6163.)
|- ((M e. ZZ /\ N e. ZZ) -> (M <_ N <-> (N - M) e. NN0))
Theorem	znn0sub2t 6181	The nonnegative difference of integers is a nonnegative integer.
|- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> (N - M) e. NN0)
Theorem	zmulclt 6182	Closure of multiplication of integers.
|- ((M e. ZZ /\ N e. ZZ) -> (M x. N) e. ZZ)
Theorem	zltp1let 6183	Integer ordering relation.
|- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> (M + 1) <_ N))
Theorem	zleltp1t 6184	Integer ordering relation.
|- ((M e. ZZ /\ N e. ZZ) -> (M <_ N <-> M < (N + 1)))
Theorem	zlem1ltt 6185	Integer ordering relation.
|- ((M e. ZZ /\ N e. ZZ) -> (M <_ N <-> (M - 1) < N))
Theorem	zltlem1t 6186	Integer ordering relation.
|- ((M e. ZZ /\ N e. ZZ) -> (M < N <-> M <_ (N - 1)))
Theorem	nn0lem1ltt 6187	Nonnegative integer ordering relation.
|- ((M e. NN0 /\ N e. NN0) -> (M <_ N <-> (M - 1) < N))
Theorem	nnlem1ltt 6188	Natural number ordering relation.
|- ((M e. NN /\ N e. NN) -> (M <_ N <-> (M - 1) < N))
Theorem	nnltlem1t 6189	Natural number ordering relation.
|- ((M e. NN /\ N e.