Theorem List for Intuitionistic Logic Explorer - 8201-8300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 5nn0 8201 |
5 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 6nn0 8202 |
6 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 7nn0 8203 |
7 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 8nn0 8204 |
8 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 9nn0 8205 |
9 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | 10nn0 8206 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.)
|
|
|
Theorem | nn0ge0 8207 |
A nonnegative integer is greater than or equal to zero. (Contributed by
NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nn0nlt0 8208 |
A nonnegative integer is not less than zero. (Contributed by NM,
9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0ge0i 8209 |
Nonnegative integers are nonnegative. (Contributed by Raph Levien,
10-Dec-2002.)
|
|
|
Theorem | nn0le0eq0 8210 |
A nonnegative integer is less than or equal to zero iff it is equal to
zero. (Contributed by NM, 9-Dec-2005.)
|
|
|
Theorem | nn0p1gt0 8211 |
A nonnegative integer increased by 1 is greater than 0. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
|
|
Theorem | nnnn0addcl 8212 |
A positive integer plus a nonnegative integer is a positive integer.
(Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro,
16-May-2014.)
|
|
|
Theorem | nn0nnaddcl 8213 |
A nonnegative integer plus a positive integer is a positive integer.
(Contributed by NM, 22-Dec-2005.)
|
|
|
Theorem | 0mnnnnn0 8214 |
The result of subtracting a positive integer from 0 is not a nonnegative
integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
|
|
|
Theorem | un0addcl 8215 |
If is closed under
addition, then so is
.
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | un0mulcl 8216 |
If is closed under
multiplication, then so is .
(Contributed by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | nn0addcl 8217 |
Closure of addition of nonnegative integers. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | nn0mulcl 8218 |
Closure of multiplication of nonnegative integers. (Contributed by NM,
22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|
|
|
Theorem | nn0addcli 8219 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0mulcli 8220 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0p1nn 8221 |
A nonnegative integer plus 1 is a positive integer. (Contributed by Raph
Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | peano2nn0 8222 |
Second Peano postulate for nonnegative integers. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nnm1nn0 8223 |
A positive integer minus 1 is a nonnegative integer. (Contributed by
Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro,
16-May-2014.)
|
|
|
Theorem | elnn0nn 8224 |
The nonnegative integer property expressed in terms of positive integers.
(Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro,
16-May-2014.)
|
|
|
Theorem | elnnnn0 8225 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-May-2004.)
|
|
|
Theorem | elnnnn0b 8226 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 1-Sep-2005.)
|
|
|
Theorem | elnnnn0c 8227 |
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10-Jan-2006.)
|
|
|
Theorem | nn0addge1 8228 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0addge2 8229 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0addge1i 8230 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0addge2i 8231 |
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10-Mar-2005.)
|
|
|
Theorem | nn0le2xi 8232 |
A nonnegative integer is less than or equal to twice itself.
(Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0lele2xi 8233 |
'Less than or equal to' implies 'less than or equal to twice' for
nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
|
|
|
Theorem | nn0supp 8234 |
Two ways to write the support of a function on . (Contributed by
Mario Carneiro, 29-Dec-2014.)
|
|
|
Theorem | nnnn0d 8235 |
A positive integer is a nonnegative integer. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0red 8236 |
A nonnegative integer is a real number. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nn0cnd 8237 |
A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0ge0d 8238 |
A nonnegative integer is greater than or equal to zero. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0addcld 8239 |
Closure of addition of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0mulcld 8240 |
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nn0readdcl 8241 |
Closure law for addition of reals, restricted to nonnegative integers.
(Contributed by Alexander van der Vekens, 6-Apr-2018.)
|
|
|
Theorem | nn0ge2m1nn 8242 |
If a nonnegative integer is greater than or equal to two, the integer
decreased by 1 is a positive integer. (Contributed by Alexander van der
Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.)
|
|
|
Theorem | nn0ge2m1nn0 8243 |
If a nonnegative integer is greater than or equal to two, the integer
decreased by 1 is also a nonnegative integer. (Contributed by Alexander
van der Vekens, 1-Aug-2018.)
|
|
|
Theorem | nn0nndivcl 8244 |
Closure law for dividing of a nonnegative integer by a positive integer.
(Contributed by Alexander van der Vekens, 14-Apr-2018.)
|
|
|
3.4.8 Integers (as a subset of complex
numbers)
|
|
Syntax | cz 8245 |
Extend class notation to include the class of integers.
|
|
|
Definition | df-z 8246 |
Define the set of integers, which are the positive and negative integers
together with zero. Definition of integers in [Apostol] p. 22. The
letter Z abbreviates the German word Zahlen meaning "numbers."
(Contributed by NM, 8-Jan-2002.)
|
|
|
Theorem | elz 8247 |
Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
|
|
|
Theorem | nnnegz 8248 |
The negative of a positive integer is an integer. (Contributed by NM,
12-Jan-2002.)
|
|
|
Theorem | zre 8249 |
An integer is a real. (Contributed by NM, 8-Jan-2002.)
|
|
|
Theorem | zcn 8250 |
An integer is a complex number. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | zrei 8251 |
An integer is a real number. (Contributed by NM, 14-Jul-2005.)
|
|
|
Theorem | zssre 8252 |
The integers are a subset of the reals. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | zsscn 8253 |
The integers are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | zex 8254 |
The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised
by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | elnnz 8255 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 8-Jan-2002.)
|
|
|
Theorem | 0z 8256 |
Zero is an integer. (Contributed by NM, 12-Jan-2002.)
|
|
|
Theorem | 0zd 8257 |
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | elnn0z 8258 |
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9-May-2004.)
|
|
|
Theorem | elznn0nn 8259 |
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10-May-2004.)
|
|
|
Theorem | elznn0 8260 |
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9-May-2004.)
|
|
|
Theorem | elznn 8261 |
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12-Jul-2005.)
|
|
|
Theorem | nnssz 8262 |
Positive integers are a subset of integers. (Contributed by NM,
9-Jan-2002.)
|
|
|
Theorem | nn0ssz 8263 |
Nonnegative integers are a subset of the integers. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nnz 8264 |
A positive integer is an integer. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | nn0z 8265 |
A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | nnzi 8266 |
A positive integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | nn0zi 8267 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | elnnz1 8268 |
Positive integer property expressed in terms of integers. (Contributed by
NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nnzrab 8269 |
Positive integers expressed as a subset of integers. (Contributed by NM,
3-Oct-2004.)
|
|
|
Theorem | nn0zrab 8270 |
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3-Oct-2004.)
|
|
|
Theorem | 1z 8271 |
One is an integer. (Contributed by NM, 10-May-2004.)
|
|
|
Theorem | 1zzd 8272 |
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6-Dec-2018.)
|
|
|
Theorem | 2z 8273 |
Two is an integer. (Contributed by NM, 10-May-2004.)
|
|
|
Theorem | 3z 8274 |
3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | 4z 8275 |
4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|
|
|
Theorem | znegcl 8276 |
Closure law for negative integers. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | neg1z 8277 |
-1 is an integer (common case). (Contributed by David A. Wheeler,
5-Dec-2018.)
|
|
|
Theorem | znegclb 8278 |
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
|
|
Theorem | nn0negz 8279 |
The negative of a nonnegative integer is an integer. (Contributed by NM,
9-May-2004.)
|
|
|
Theorem | nn0negzi 8280 |
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | peano2z 8281 |
Second Peano postulate generalized to integers. (Contributed by NM,
13-Feb-2005.)
|
|
|
Theorem | zaddcllempos 8282 |
Lemma for zaddcl 8285. Special case in which is a positive integer.
(Contributed by Jim Kingdon, 14-Mar-2020.)
|
|
|
Theorem | peano2zm 8283 |
"Reverse" second Peano postulate for integers. (Contributed by NM,
12-Sep-2005.)
|
|
|
Theorem | zaddcllemneg 8284 |
Lemma for zaddcl 8285. Special case in which is a positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
|
|
Theorem | zaddcl 8285 |
Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | zsubcl 8286 |
Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
|
|
|
Theorem | ztri3or0 8287 |
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14-Mar-2020.)
|
|
|
Theorem | ztri3or 8288 |
Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
|
|
Theorem | zletric 8289 |
Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|
|
|
Theorem | zlelttric 8290 |
Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|
|
|
Theorem | zltnle 8291 |
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14-Mar-2020.)
|
|
|
Theorem | zleloe 8292 |
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|
|
|
Theorem | znnnlt1 8293 |
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13-Jul-2005.)
|
|
|
Theorem | zletr 8294 |
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3-Apr-2018.)
|
|
|
Theorem | zrevaddcl 8295 |
Reverse closure law for addition of integers. (Contributed by NM,
11-May-2004.)
|
|
|
Theorem | znnsub 8296 |
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 7952.) (Contributed by NM, 11-May-2004.)
|
|
|
Theorem | zmulcl 8297 |
Closure of multiplication of integers. (Contributed by NM,
30-Jul-2004.)
|
|
|
Theorem | zltp1le 8298 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | zleltp1 8299 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
|
|
Theorem | zlem1lt 8300 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
|