Home | Metamath
Proof Explorer Theorem List (p. 115 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnzi 11401 | A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | nn0zi 11402 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | elnnz1 11403 | Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | znnnlt1 11404 | An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.) |
Theorem | nnzrab 11405 | Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.) |
Theorem | nn0zrab 11406 | Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.) |
Theorem | 1z 11407 | One is an integer. (Contributed by NM, 10-May-2004.) |
Theorem | 1zzd 11408 | 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 2z 11409 | 2 is an integer. (Contributed by NM, 10-May-2004.) |
Theorem | 3z 11410 | 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | 4z 11411 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
Theorem | znegcl 11412 | Closure law for negative integers. (Contributed by NM, 9-May-2004.) |
Theorem | neg1z 11413 | -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
Theorem | znegclb 11414 | A complex number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
Theorem | nn0negz 11415 | The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.) |
Theorem | nn0negzi 11416 | The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | zaddcl 11417 | Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | peano2z 11418 | Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.) |
Theorem | zsubcl 11419 | Closure of subtraction of integers. (Contributed by NM, 11-May-2004.) |
Theorem | peano2zm 11420 | "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.) |
Theorem | zletr 11421 | Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.) |
Theorem | zrevaddcl 11422 | Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.) |
Theorem | znnsub 11423 | The positive difference of unequal integers is a positive integer. (Generalization of nnsub 11059.) (Contributed by NM, 11-May-2004.) |
Theorem | znn0sub 11424 | The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 11343.) (Contributed by NM, 14-Jul-2005.) |
Theorem | nzadd 11425 | The sum of a real number not being an integer and an integer is not an integer. (Contributed by AV, 19-Jul-2021.) |
Theorem | zmulcl 11426 | Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.) |
Theorem | zltp1le 11427 | Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | zleltp1 11428 | Integer ordering relation. (Contributed by NM, 10-May-2004.) |
Theorem | zlem1lt 11429 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
Theorem | zltlem1 11430 | Integer ordering relation. (Contributed by NM, 13-Nov-2004.) |
Theorem | zgt0ge1 11431 | An integer greater than is greater than or equal to . (Contributed by AV, 14-Oct-2018.) |
Theorem | nnleltp1 11432 | Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | nnltp1le 11433 | Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.) |
Theorem | nnaddm1cl 11434 | Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | nn0ltp1le 11435 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | nn0leltp1 11436 | Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.) |
Theorem | nn0ltlem1 11437 | Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
Theorem | nn0sub2 11438 | Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.) |
Theorem | nn0lt10b 11439 | A nonnegative integer less than is . (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | nn0lt2 11440 | A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
Theorem | nn0le2is012 11441 | 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 11442 | Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
Theorem | nnlem1lt 11443 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
Theorem | nnltlem1 11444 | Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.) |
Theorem | nnm1ge0 11445 | A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.) |
Theorem | nn0ge0div 11446 | Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
Theorem | zdiv 11447* | Two ways to express " divides . (Contributed by NM, 3-Oct-2008.) |
Theorem | zdivadd 11448 | Property of divisibility: if divides and then it divides . (Contributed by NM, 3-Oct-2008.) |
Theorem | zdivmul 11449 | Property of divisibility: if divides then it divides . (Contributed by NM, 3-Oct-2008.) |
Theorem | zextle 11450* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
Theorem | zextlt 11451* | An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.) |
Theorem | recnz 11452 | The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.) |
Theorem | btwnnz 11453 | A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.) |
Theorem | gtndiv 11454 | A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.) |
Theorem | halfnz 11455 | One-half is not an integer. (Contributed by NM, 31-Jul-2004.) |
Theorem | 3halfnz 11456 | Three halves is not an integer. (Contributed by AV, 2-Jun-2020.) |
Theorem | suprzcl 11457* | The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
Theorem | prime 11458* | Two ways to express " is a prime number (or 1)." See also isprm 15387. (Contributed by NM, 4-May-2005.) |
Theorem | msqznn 11459 | The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.) |
Theorem | zneo 11460 | 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 | nneo 11461 | 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 11462 | A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) |
Theorem | zeo 11463 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) |
Theorem | zeo2 11464 | An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) |
Theorem | peano2uz2 11465* | Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.) |
Theorem | peano5uzi 11466* | Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.) |
Theorem | peano5uzti 11467* | Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.) |
Theorem | dfuzi 11468* | An expression for the upper integers that start at that is analogous to dfnn2 11033 for positive integers. (Contributed by NM, 6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.) |
Theorem | uzind 11469* | 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 11470* | 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 11471* | 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 11472* | 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 | nn0indALT 11473* | Principle of Mathematical Induction (inference schema) on nonnegative integers. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either nn0ind 11472 or nn0indALT 11473 may be used; see comment for nnind 11038. (Contributed by NM, 28-Nov-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | nn0indd 11474* | Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
Theorem | fzind 11475* | 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 11476* | 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 11477* | 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 11478* | 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 11479* | Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.) |
Theorem | nn0zd 11480 | A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nnzd 11481 | A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | zred 11482 | An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | zcnd 11483 | An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | znegcld 11484 | Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | peano2zd 11485 | Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | zaddcld 11486 | Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | zsubcld 11487 | Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | zmulcld 11488 | Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | znnn0nn 11489 | The negative of a negative integer, is a natural number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | zadd2cl 11490 | Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
Theorem | zriotaneg 11491* | The negative of the unique integer such that . (Contributed by AV, 1-Dec-2018.) |
Theorem | suprfinzcl 11492 | The supremum of a nonempty finite set of integers is a member of the set. (Contributed by AV, 1-Oct-2019.) |
Syntax | cdc 11493 | Constant used for decimal constructor. |
; | ||
Definition | df-dec 11494 | Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base . For example, ;;; ;;; ;;; 1kp2ke3k 27303. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.) |
; | ||
Theorem | dfdecOLD 11495 | Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base . Obsolete version of df-dec 11494 as of 1-Aug-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | 9p1e10 11496 | 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.) |
; | ||
Theorem | dfdec10 11497 | Version of the definition of the "decimal constructor" using ; instead of the symbol 10. Of course, this statement cannot be used as definition, because it uses the "decimal constructor". (Contributed by AV, 1-Aug-2021.) |
; ; | ||
Theorem | decex 11498 | A decimal number is a set. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | decexOLD 11499 | Obsolete proof of decex 11498 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | deceq1 11500 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; ; |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |