HomeTheorem List (p. 97 of 169)
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. 97 of 169) | < 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 | nnzrab 9601 | Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.) |
           | ||
| Theorem | nn0zrab 9602 | Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.) |
 | ||
| Theorem | 1z 9603 | One is an integer. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | 1zzd 9604 | 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
    | ||
| Theorem | 2z 9605 | Two is an integer. (Contributed by NM, 10-May-2004.) |
 | ||
| Theorem | 3z 9606 | 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.) |
 | ||
| Theorem | 4z 9607 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
 | ||
| Theorem | znegcl 9608 | Closure law for negative integers. (Contributed by NM, 9-May-2004.) |
  | ||
| Theorem | neg1z 9609 | -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
|
| ||
| Theorem | znegclb 9610 | A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
   | ||
| Theorem | nn0negz 9611 | The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.) |
| | ||
| Theorem | nn0negzi 9612 | The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ||
| Theorem | peano2z 9613 | Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.) |
 | ||
| Theorem | zaddcllempos 9614 |
Lemma for zaddcl 9617. Special case in which is a positive integer.
(Contributed by Jim Kingdon, 14-Mar-2020.)
|
 ![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | peano2zm 9615 | "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.) |
 | ||
| Theorem | zaddcllemneg 9616 |
Lemma for zaddcl 9617. Special case in which is a positive
integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
| ||
| Theorem | zaddcl 9617 | Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
|
| ||
| Theorem | zsubcl 9618 | Closure of subtraction of integers. (Contributed by NM, 11-May-2004.) |
|
| ||
| Theorem | ztri3or0 9619 | Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.) |
  | ||
| Theorem | ztri3or 9620 | Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| | ||
| Theorem | zletric 9621 | Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.) |
 | ||
| Theorem | zlelttric 9622 | Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.) |
| | ||
| Theorem | zltnle 9623 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| ||
| Theorem | zleloe 9624 | Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.) |
| | ||
| Theorem | znnnlt1 9625 | An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.) |
| | ||
| Theorem | nnnle0 9626 | A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.) |
| | ||
| Theorem | zletr 9627 | Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
   | ||
| Theorem | zrevaddcl 9628 | Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.) |
|
| ||
| Theorem | znnsub 9629 | The positive difference of unequal integers is a positive integer. (Generalization of nnsub 9276.) (Contributed by NM, 11-May-2004.) |
|
| ||
| Theorem | nzadd 9630 | 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 9631 | Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.) |
| ||
| Theorem | zltp1le 9632 | Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
|
| ||
| Theorem | zleltp1 9633 | Integer ordering relation. (Contributed by NM, 10-May-2004.) |
| | ||
| Theorem | zlem1lt 9634 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
|
| ||
| Theorem | zltlem1 9635 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
| | ||
| Theorem | zgt0ge1 9636 |
An integer greater than
is greater than or equal to .
(Contributed by AV, 14-Oct-2018.)
|
 | ||
| Theorem | nnleltp1 9637 | Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| | ||
| Theorem | nnltp1le 9638 | Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.) |
|
| ||
| Theorem | nnaddm1cl 9639 | Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
|
| ||
| Theorem | nn0ltp1le 9640 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| | ||
| Theorem | nn0leltp1 9641 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.) |
| | ||
| Theorem | nn0ltlem1 9642 | Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
| | ||
| Theorem | znn0sub 9643 | The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 9644.) (Contributed by NM, 14-Jul-2005.) |
|
| ||
| Theorem | nn0sub 9644 | Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.) |
| | ||
| Theorem | ltsubnn0 9645 | 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 9646 | A nonnegative integer is greater than or equal to its negative. (Contributed by AV, 13-Aug-2021.) |
|
| ||
| Theorem | difgtsumgt 9647 | 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 9648 | 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 9649* | 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 9650 | Alternate definition of the integers, based on elz2 9649. (Contributed by Mario Carneiro, 16-May-2014.) |
  | ||
| Theorem | nn0sub2 9651 | Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.) |
| | ||
| Theorem | zapne 9652 | Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| # | ||
| Theorem | zdceq 9653 | Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| DECID
| ||
| Theorem | zdcle 9654 |
Integer is
decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
|
| DECID | ||
| Theorem | zdclt 9655 |
Integer is
decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|
| DECID | ||
| Theorem | zltlen 9656 | Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8906 which is a similar result for real numbers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| | ||
| Theorem | nn0n0n1ge2b 9657 | 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 9658 |
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22-Jun-2011.)
|
|
| ||
| Theorem | nn0lt2 9659 | A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
| | ||
| Theorem | nn0le2is012 9660 | 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 9661 | Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| | ||
| Theorem | nnlem1lt 9662 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
|
| ||
| Theorem | nnltlem1 9663 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
| | ||
| Theorem | nnm1ge0 9664 | A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.) |
|
| ||
| Theorem | nn0ge0div 9665 | Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
 | ||
| Theorem | zdiv 9666* |
Two ways to express " divides .
(Contributed by NM,
3-Oct-2008.)
|
| ||
| Theorem | zdivadd 9667 |
Property of divisibility: if  divides
and then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
| ||
| Theorem | zdivmul 9668 |
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
| ||
| Theorem | zextle 9669* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
| ||
| Theorem | zextlt 9670* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
|
| ||
| Theorem | recnz 9671 | The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.) |
|
| ||
| Theorem | btwnnz 9672 | A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.) |
| | ||
| Theorem | gtndiv 9673 | A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.) |
|
| ||
| Theorem | halfnz 9674 | One-half is not an integer. (Contributed by NM, 31-Jul-2004.) |
| | ||
| Theorem | 3halfnz 9675 | Three halves is not an integer. (Contributed by AV, 2-Jun-2020.) |
| | ||
| Theorem | suprzclex 9676* | The supremum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 20-Dec-2021.) |
    
| ||
| Theorem | prime 9677* |
Two ways to express " is a prime number (or 1)". (Contributed by
NM, 4-May-2005.)
|
|
| ||
| Theorem | msqznn 9678 | The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.) |
|
| ||
| Theorem | zneo 9679 | 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 9680 | A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.) |
|
| ||
| Theorem | nneo 9681 | 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 9682 | A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) |
| | ||
| Theorem | zeo 9683 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) |
|
| ||
| Theorem | zeo2 9684 | An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) |
|
| ||
| Theorem | peano2uz2 9685* | Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.) |
|
| ||
| Theorem | peano5uzti 9686* | Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.) |
|
| ||
| Theorem | peano5uzi 9687* | Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.) |
|
| ||
| Theorem | dfuzi 9688* |
An expression for the upper integers that start at that is
analogous to dfnn2 9239 for positive integers. (Contributed by NM,
6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
|
| ||
| Theorem | uzind 9689* |
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 9690* |
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 9691* |
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 9692* | 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 9693* |
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 9694* |
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 9695* | 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 9696* | 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 9697* | Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.) |
| | ||
| Theorem | nn0zd 9698 | A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | nnzd 9699 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| Theorem | zred 9700 | An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |