Type  Label  Description 
Statement 

Theorem  zmulcl 8901 
Closure of multiplication of integers. (Contributed by NM,
30Jul2004.)



Theorem  zltp1le 8902 
Integer ordering relation. (Contributed by NM, 10May2004.) (Proof
shortened by Mario Carneiro, 16May2014.)



Theorem  zleltp1 8903 
Integer ordering relation. (Contributed by NM, 10May2004.)



Theorem  zlem1lt 8904 
Integer ordering relation. (Contributed by NM, 13Nov2004.)



Theorem  zltlem1 8905 
Integer ordering relation. (Contributed by NM, 13Nov2004.)



Theorem  zgt0ge1 8906 
An integer greater than
is greater than or equal to .
(Contributed by AV, 14Oct2018.)



Theorem  nnleltp1 8907 
Positive integer ordering relation. (Contributed by NM, 13Aug2001.)
(Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nnltp1le 8908 
Positive integer ordering relation. (Contributed by NM, 19Aug2001.)



Theorem  nnaddm1cl 8909 
Closure of addition of positive integers minus one. (Contributed by NM,
6Aug2003.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nn0ltp1le 8910 
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10Dec2002.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nn0leltp1 8911 
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10Apr2004.)



Theorem  nn0ltlem1 8912 
Nonnegative integer ordering relation. (Contributed by NM, 10May2004.)
(Proof shortened by Mario Carneiro, 16May2014.)



Theorem  znn0sub 8913 
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 8914.) (Contributed by NM, 14Jul2005.)



Theorem  nn0sub 8914 
Subtraction of nonnegative integers. (Contributed by NM, 9May2004.)



Theorem  nn0n0n1ge2 8915 
A nonnegative integer which is neither 0 nor 1 is greater than or equal to
2. (Contributed by Alexander van der Vekens, 6Dec2017.)



Theorem  elz2 8916* 
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, 16May2014.)



Theorem  dfz2 8917 
Alternate definition of the integers, based on elz2 8916.
(Contributed by
Mario Carneiro, 16May2014.)



Theorem  nn0sub2 8918 
Subtraction of nonnegative integers. (Contributed by NM, 4Sep2005.)



Theorem  zapne 8919 
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14Mar2020.)

# 

Theorem  zdceq 8920 
Equality of integers is decidable. (Contributed by Jim Kingdon,
14Mar2020.)

DECID


Theorem  zdcle 8921 
Integer is
decidable. (Contributed by Jim Kingdon, 7Apr2020.)

DECID 

Theorem  zdclt 8922 
Integer is
decidable. (Contributed by Jim Kingdon, 1Jun2020.)

DECID 

Theorem  zltlen 8923 
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8204 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 14Mar2020.)



Theorem  nn0n0n1ge2b 8924 
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, 17Jan2018.)



Theorem  nn0lt10b 8925 
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22Jun2011.)



Theorem  nn0lt2 8926 
A nonnegative integer less than 2 must be 0 or 1. (Contributed by
Alexander van der Vekens, 16Sep2018.)



Theorem  nn0le2is012 8927 
A nonnegative integer which is less than or equal to 2 is either 0 or 1 or
2. (Contributed by AV, 16Mar2019.)



Theorem  nn0lem1lt 8928 
Nonnegative integer ordering relation. (Contributed by NM,
21Jun2005.)



Theorem  nnlem1lt 8929 
Positive integer ordering relation. (Contributed by NM, 21Jun2005.)



Theorem  nnltlem1 8930 
Positive integer ordering relation. (Contributed by NM, 21Jun2005.)



Theorem  nnm1ge0 8931 
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30Oct2018.)



Theorem  nn0ge0div 8932 
Division of a nonnegative integer by a positive number is not negative.
(Contributed by Alexander van der Vekens, 14Apr2018.)



Theorem  zdiv 8933* 
Two ways to express " divides .
(Contributed by NM,
3Oct2008.)



Theorem  zdivadd 8934 
Property of divisibility: if divides
and then it divides
. (Contributed by NM, 3Oct2008.)



Theorem  zdivmul 8935 
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3Oct2008.)



Theorem  zextle 8936* 
An extensionalitylike property for integer ordering. (Contributed by
NM, 29Oct2005.)



Theorem  zextlt 8937* 
An extensionalitylike property for integer ordering. (Contributed by
NM, 29Oct2005.)



Theorem  recnz 8938 
The reciprocal of a number greater than 1 is not an integer. (Contributed
by NM, 3May2005.)



Theorem  btwnnz 8939 
A number between an integer and its successor is not an integer.
(Contributed by NM, 3May2005.)



Theorem  gtndiv 8940 
A larger number does not divide a smaller positive integer. (Contributed
by NM, 3May2005.)



Theorem  halfnz 8941 
Onehalf is not an integer. (Contributed by NM, 31Jul2004.)



Theorem  3halfnz 8942 
Three halves is not an integer. (Contributed by AV, 2Jun2020.)



Theorem  suprzclex 8943* 
The supremum of a set of integers is an element of the set.
(Contributed by Jim Kingdon, 20Dec2021.)



Theorem  prime 8944* 
Two ways to express " is a prime number (or 1)." (Contributed by
NM, 4May2005.)



Theorem  msqznn 8945 
The square of a nonzero integer is a positive integer. (Contributed by
NM, 2Aug2004.)



Theorem  zneo 8946 
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,
31Jul2004.) (Proof shortened by Mario Carneiro, 18May2014.)



Theorem  nneoor 8947 
A positive integer is even or odd. (Contributed by Jim Kingdon,
15Mar2020.)



Theorem  nneo 8948 
A positive integer is even or odd but not both. (Contributed by NM,
1Jan2006.) (Proof shortened by Mario Carneiro, 18May2014.)



Theorem  nneoi 8949 
A positive integer is even or odd but not both. (Contributed by NM,
20Aug2001.)



Theorem  zeo 8950 
An integer is even or odd. (Contributed by NM, 1Jan2006.)



Theorem  zeo2 8951 
An integer is even or odd but not both. (Contributed by Mario Carneiro,
12Sep2015.)



Theorem  peano2uz2 8952* 
Second Peano postulate for upper integers. (Contributed by NM,
3Oct2004.)



Theorem  peano5uzti 8953* 
Peano's inductive postulate for upper integers. (Contributed by NM,
6Jul2005.) (Revised by Mario Carneiro, 25Jul2013.)



Theorem  peano5uzi 8954* 
Peano's inductive postulate for upper integers. (Contributed by NM,
6Jul2005.) (Revised by Mario Carneiro, 3May2014.)



Theorem  dfuzi 8955* 
An expression for the upper integers that start at that is
analogous to dfnn2 8522 for positive integers. (Contributed by NM,
6Jul2005.) (Proof shortened by Mario Carneiro, 3May2014.)



Theorem  uzind 8956* 
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, 5Jul2005.)



Theorem  uzind2 8957* 
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,
25Jul2005.)



Theorem  uzind3 8958* 
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,
26Jul2005.)



Theorem  nn0ind 8959* 
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, 13May2004.)



Theorem  fzind 8960* 
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,
31Mar2011.)



Theorem  fnn0ind 8961* 
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,
31Mar2011.)



Theorem  nn0indraph 8962* 
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,
10Apr2004.)



Theorem  zindd 8963* 
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, 17Apr2009.) (Proof shortened by Mario
Carneiro, 4Jan2017.)



Theorem  btwnz 8964* 
Any real number can be sandwiched between two integers. Exercise 2 of
[Apostol] p. 28. (Contributed by NM,
10Nov2004.)



Theorem  nn0zd 8965 
A positive integer is an integer. (Contributed by Mario Carneiro,
28May2016.)



Theorem  nnzd 8966 
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zred 8967 
An integer is a real number. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zcnd 8968 
An integer is a complex number. (Contributed by Mario Carneiro,
28May2016.)



Theorem  znegcld 8969 
Closure law for negative integers. (Contributed by Mario Carneiro,
28May2016.)



Theorem  peano2zd 8970 
Deduction from second Peano postulate generalized to integers.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  zaddcld 8971 
Closure of addition of integers. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zsubcld 8972 
Closure of subtraction of integers. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zmulcld 8973 
Closure of multiplication of integers. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zadd2cl 8974 
Increasing an integer by 2 results in an integer. (Contributed by
Alexander van der Vekens, 16Sep2018.)



Theorem  btwnapz 8975 
A number between an integer and its successor is apart from any integer.
(Contributed by Jim Kingdon, 6Jan2023.)

# 

3.4.10 Decimal arithmetic


Syntax  cdc 8976 
Constant used for decimal constructor.

; 

Definition  dfdec 8977 
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base . For example,
;;; ;;; ;;; 1kp2ke3k 12363.
(Contributed by Mario Carneiro, 17Apr2015.) (Revised by AV,
1Aug2021.)

; 

Theorem  9p1e10 8978 
9 + 1 = 10. (Contributed by Mario Carneiro, 18Apr2015.) (Revised by
Stanislas Polu, 7Apr2020.) (Revised by AV, 1Aug2021.)

; 

Theorem  dfdec10 8979 
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, 1Aug2021.)

; ;


Theorem  deceq1 8980 
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17Apr2015.) (Revised by AV, 6Sep2021.)

;
; 

Theorem  deceq2 8981 
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17Apr2015.) (Revised by AV, 6Sep2021.)

;
; 

Theorem  deceq1i 8982 
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17Apr2015.)

; ; 

Theorem  deceq2i 8983 
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17Apr2015.)

; ; 

Theorem  deceq12i 8984 
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17Apr2015.)

; ; 

Theorem  numnncl 8985 
Closure for a numeral (with units place). (Contributed by Mario
Carneiro, 18Feb2014.)



Theorem  num0u 8986 
Add a zero in the units place. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  num0h 8987 
Add a zero in the higher places. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  numcl 8988 
Closure for a decimal integer (with units place). (Contributed by Mario
Carneiro, 18Feb2014.)



Theorem  numsuc 8989 
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 18Feb2014.)



Theorem  deccl 8990 
Closure for a numeral. (Contributed by Mario Carneiro, 17Apr2015.)
(Revised by AV, 6Sep2021.)

; 

Theorem  10nn 8991 
10 is a positive integer. (Contributed by NM, 8Nov2012.) (Revised by
AV, 6Sep2021.)

; 

Theorem  10pos 8992 
The number 10 is positive. (Contributed by NM, 5Feb2007.) (Revised by
AV, 8Sep2021.)

; 

Theorem  10nn0 8993 
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.) (Revised by AV, 6Sep2021.)

; 

Theorem  10re 8994 
The number 10 is real. (Contributed by NM, 5Feb2007.) (Revised by AV,
8Sep2021.)

; 

Theorem  decnncl 8995 
Closure for a numeral. (Contributed by Mario Carneiro, 17Apr2015.)
(Revised by AV, 6Sep2021.)

; 

Theorem  dec0u 8996 
Add a zero in the units place. (Contributed by Mario Carneiro,
17Apr2015.) (Revised by AV, 6Sep2021.)

;
; 

Theorem  dec0h 8997 
Add a zero in the higher places. (Contributed by Mario Carneiro,
17Apr2015.) (Revised by AV, 6Sep2021.)

; 

Theorem  numnncl2 8998 
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9Mar2015.)



Theorem  decnncl2 8999 
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17Apr2015.) (Revised by AV, 6Sep2021.)

; 

Theorem  numlt 9000 
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18Feb2014.)

