HomeTheorem List (p. 95 of 160)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 95 of 160) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 4z 9401 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
    | ||
| Theorem | znegcl 9402 | Closure law for negative integers. (Contributed by NM, 9-May-2004.) |
     | ||
| Theorem | neg1z 9403 | -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
| ||
| Theorem | znegclb 9404 | A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
   | ||
| Theorem | nn0negz 9405 | The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.) |
 | ||
| Theorem | nn0negzi 9406 | The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ||
| Theorem | peano2z 9407 | Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.) |
 | ||
| Theorem | zaddcllempos 9408 |
Lemma for zaddcl 9411. Special case in which is a positive integer.
(Contributed by Jim Kingdon, 14-Mar-2020.)
|
 ![/\](wedge.gif "/\"){kind=small} 
| ||
| Theorem | peano2zm 9409 | "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.) |
 | ||
| Theorem | zaddcllemneg 9410 |
Lemma for zaddcl 9411. Special case in which is a positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
| ||
| Theorem | zaddcl 9411 | Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
|
| ||
| Theorem | zsubcl 9412 | Closure of subtraction of integers. (Contributed by NM, 11-May-2004.) |
|
| ||
| Theorem | ztri3or0 9413 | Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.) |
    | ||
| Theorem | ztri3or 9414 | Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| | ||
| Theorem | zletric 9415 | Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.) |
  | ||
| Theorem | zlelttric 9416 | Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.) |
| | ||
| Theorem | zltnle 9417 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| ||
| Theorem | zleloe 9418 | Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.) |
| | ||
| Theorem | znnnlt1 9419 | An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.) |
| | ||
| Theorem | nnnle0 9420 | A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.) |
| | ||
| Theorem | zletr 9421 | Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
   | ||
| Theorem | zrevaddcl 9422 | Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.) |
|
| ||
| Theorem | znnsub 9423 | The positive difference of unequal integers is a positive integer. (Generalization of nnsub 9074.) (Contributed by NM, 11-May-2004.) |
|
| ||
| Theorem | nzadd 9424 | The sum of a real number not being an integer and an integer is not an integer. Note that "not being an integer" in this case means "the negation of is an integer" rather than "is apart from any integer" (given excluded middle, those two would be equivalent). (Contributed by AV, 19-Jul-2021.) |
![\](setminus.gif "\"){kind=small}
| ||
| Theorem | zmulcl 9425 | Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.) |
| ||
| Theorem | zltp1le 9426 | Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
|
| ||
| Theorem | zleltp1 9427 | Integer ordering relation. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | zlem1lt 9428 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
|
| ||
| Theorem | zltlem1 9429 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
| | ||
| Theorem | zgt0ge1 9430 |
An integer greater than
is greater than or equal to .
(Contributed by AV, 14-Oct-2018.)
|
 | ||
| Theorem | nnleltp1 9431 | Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| | ||
| Theorem | nnltp1le 9432 | Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.) |
|
| ||
| Theorem | nnaddm1cl 9433 | Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
|
| ||
| Theorem | nn0ltp1le 9434 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| | ||
| Theorem | nn0leltp1 9435 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.) |
| | ||
| Theorem | nn0ltlem1 9436 | Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| | ||
| Theorem | znn0sub 9437 | The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 9438.) (Contributed by NM, 14-Jul-2005.) |
|
| ||
| Theorem | nn0sub 9438 | Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.) |
| | ||
| Theorem | ltsubnn0 9439 | Subtracting a nonnegative integer from a nonnegative integer which is greater than the first one results in a nonnegative integer. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
|
| ||
| Theorem | nn0negleid 9440 | A nonnegative integer is greater than or equal to its negative. (Contributed by AV, 13-Aug-2021.) |
|
| ||
| Theorem | difgtsumgt 9441 | If the difference of a real number and a nonnegative integer is greater than another real number, the sum of the real number and the nonnegative integer is also greater than the other real number. (Contributed by AV, 13-Aug-2021.) |
 | ||
| Theorem | nn0n0n1ge2 9442 | A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
 
| ||
| Theorem | elz2 9443* | Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014.) |
 
 | ||
| Theorem | dfz2 9444 | Alternate definition of the integers, based on elz2 9443. (Contributed by Mario Carneiro, 16-May-2014.) |
  | ||
| Theorem | nn0sub2 9445 | Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.) |
| | ||
| Theorem | zapne 9446 | Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| # | ||
| Theorem | zdceq 9447 | Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| DECID
| ||
| Theorem | zdcle 9448 |
Integer is
decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
|
| DECID | ||
| Theorem | zdclt 9449 |
Integer is
decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|
| DECID | ||
| Theorem | zltlen 9450 | Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8704 which is a similar result for real numbers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| | ||
| Theorem | nn0n0n1ge2b 9451 | A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.) |
|
| ||
| Theorem | nn0lt10b 9452 |
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22-Jun-2011.)
|
|
| ||
| Theorem | nn0lt2 9453 | A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
| | ||
| Theorem | nn0le2is012 9454 | A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019.) |
|
| ||
| Theorem | nn0lem1lt 9455 | Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| | ||
| Theorem | nnlem1lt 9456 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
|
| ||
| Theorem | nnltlem1 9457 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| | ||
| Theorem | nnm1ge0 9458 | A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.) |
|
| ||
| Theorem | nn0ge0div 9459 | Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
 | ||
| Theorem | zdiv 9460* |
Two ways to express " divides .
(Contributed by NM,
3-Oct-2008.)
|
| ||
| Theorem | zdivadd 9461 |
Property of divisibility: if  divides
and then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
| ||
| Theorem | zdivmul 9462 |
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
| ||
| Theorem | zextle 9463* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
| ||
| Theorem | zextlt 9464* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
|
| ||
| Theorem | recnz 9465 | The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.) |
|
| ||
| Theorem | btwnnz 9466 | A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.) |
| | ||
| Theorem | gtndiv 9467 | A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.) |
|
| ||
| Theorem | halfnz 9468 | One-half is not an integer. (Contributed by NM, 31-Jul-2004.) |
| | ||
| Theorem | 3halfnz 9469 | Three halves is not an integer. (Contributed by AV, 2-Jun-2020.) |
 | ||
| Theorem | suprzclex 9470* | The supremum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 20-Dec-2021.) |
    
| ||
| Theorem | prime 9471* |
Two ways to express " is a prime number (or 1)". (Contributed by
NM, 4-May-2005.)
|
|
| ||
| Theorem | msqznn 9472 | The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.) |
|
| ||
| Theorem | zneo 9473 | No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 18-May-2014.) |
|
| ||
| Theorem | nneoor 9474 | A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.) |
|
| ||
| Theorem | nneo 9475 | A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 18-May-2014.) |
|
| ||
| Theorem | nneoi 9476 | A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) |
| | ||
| Theorem | zeo 9477 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) |
|
| ||
| Theorem | zeo2 9478 | An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) |
|
| ||
| Theorem | peano2uz2 9479* | Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.) |
 
| ||
| Theorem | peano5uzti 9480* | Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.) |
|
| ||
| Theorem | peano5uzi 9481* | Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.) |
|
| ||
| Theorem | dfuzi 9482* |
An expression for the upper integers that start at that is
analogous to dfnn2 9037 for positive integers. (Contributed by NM,
6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
|
| ||
| Theorem | uzind 9483* |
Induction on the upper integers that start at . The first four
hypotheses give us the substitution instances we need; the last two are
the basis and the induction step. (Contributed by NM, 5-Jul-2005.)
|
    
| ||
| Theorem | uzind2 9484* |
Induction on the upper integers that start after an integer .
The first four hypotheses give us the substitution instances we need;
the last two are the basis and the induction step. (Contributed by NM,
25-Jul-2005.)
|
|
| ||
| Theorem | uzind3 9485* |
Induction on the upper integers that start at an integer . The
first four hypotheses give us the substitution instances we need, and
the last two are the basis and the induction step. (Contributed by NM,
26-Jul-2005.)
|
| ||
| Theorem | nn0ind 9486* | Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 13-May-2004.) |
|
| ||
| Theorem | fzind 9487* |
Induction on the integers from to
inclusive . The first
four hypotheses give us the substitution instances we need; the last two
are the basis and the induction step. (Contributed by Paul Chapman,
31-Mar-2011.)
|
|
| ||
| Theorem | fnn0ind 9488* |
Induction on the integers from to
inclusive . The first
four hypotheses give us the substitution instances we need; the last two
are the basis and the induction step. (Contributed by Paul Chapman,
31-Mar-2011.)
|
|
| ||
| Theorem | nn0ind-raph 9489* | Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004.) |
|
| ||
| Theorem | zindd 9490* | Principle of Mathematical Induction on all integers, deduction version. The first five hypotheses give the substitutions; the last three are the basis, the induction, and the extension to negative numbers. (Contributed by Paul Chapman, 17-Apr-2009.) (Proof shortened by Mario Carneiro, 4-Jan-2017.) |
 
| ||
| Theorem | btwnz 9491* | Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.) |
| | ||
| Theorem | nn0zd 9492 | A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | nnzd 9493 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | zred 9494 | An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | zcnd 9495 | An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | znegcld 9496 | Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | peano2zd 9497 | Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
|
| ||
| Theorem | zaddcld 9498 | Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | zsubcld 9499 | Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | zmulcld 9500 | Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |