Type  Label  Description 
Statement 

Theorem  eluz 9001 
Membership in an upper set of integers. (Contributed by NM,
2Oct2005.)



Theorem  uzid 9002 
Membership of the least member in an upper set of integers. (Contributed
by NM, 2Sep2005.)



Theorem  uzn0 9003 
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16Jan2014.)



Theorem  uztrn 9004 
Transitive law for sets of upper integers. (Contributed by NM,
20Sep2005.)



Theorem  uztrn2 9005 
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26Dec2013.)



Theorem  uzneg 9006 
Contraposition law for upper integers. (Contributed by NM,
28Nov2005.)



Theorem  uzssz 9007 
An upper set of integers is a subset of all integers. (Contributed by
NM, 2Sep2005.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  uzss 9008 
Subset relationship for two sets of upper integers. (Contributed by NM,
5Sep2005.)



Theorem  uztric 9009 
Trichotomy of the ordering relation on integers, stated in terms of upper
integers. (Contributed by NM, 6Jul2005.) (Revised by Mario Carneiro,
25Jun2013.)



Theorem  uz11 9010 
The upper integers function is onetoone. (Contributed by NM,
12Dec2005.)



Theorem  eluzp1m1 9011 
Membership in the next upper set of integers. (Contributed by NM,
12Sep2005.)



Theorem  eluzp1l 9012 
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12Sep2005.)



Theorem  eluzp1p1 9013 
Membership in the next upper set of integers. (Contributed by NM,
5Oct2005.)



Theorem  eluzaddi 9014 
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22Nov2007.)



Theorem  eluzsubi 9015 
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22Nov2007.)



Theorem  eluzadd 9016 
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  eluzsub 9017 
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2Sep2009.)



Theorem  uzm1 9018 
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  uznn0sub 9019 
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4Sep2005.)



Theorem  uzin 9020 
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24Dec2013.)



Theorem  uzp1 9021 
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  nn0uz 9022 
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2Sep2005.)



Theorem  nnuz 9023 
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2Sep2005.)



Theorem  elnnuz 9024 
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6Jun2006.)



Theorem  elnn0uz 9025 
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6Jun2006.)



Theorem  eluz2nn 9026 
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3Nov2018.)



Theorem  eluzge2nn0 9027 
If an integer is greater than or equal to 2, then it is a nonnegative
integer. (Contributed by AV, 27Aug2018.) (Proof shortened by AV,
3Nov2018.)



Theorem  uzuzle23 9028 
An integer in the upper set of integers starting at 3 is element of the
upper set of integers starting at 2. (Contributed by Alexander van der
Vekens, 17Sep2018.)



Theorem  eluzge3nn 9029 
If an integer is greater than 3, then it is a positive integer.
(Contributed by Alexander van der Vekens, 17Sep2018.)



Theorem  uz3m2nn 9030 
An integer greater than or equal to 3 decreased by 2 is a positive
integer. (Contributed by Alexander van der Vekens, 17Sep2018.)



Theorem  1eluzge0 9031 
1 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.)



Theorem  2eluzge0 9032 
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.) (Proof shortened by OpenAI, 25Mar2020.)



Theorem  2eluzge1 9033 
2 is an integer greater than or equal to 1. (Contributed by Alexander van
der Vekens, 8Jun2018.)



Theorem  uznnssnn 9034 
The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29Jun2013.)



Theorem  raluz 9035* 
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  raluz2 9036* 
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  rexuz 9037* 
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  rexuz2 9038* 
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  2rexuz 9039* 
Double existential quantification in an upper set of integers.
(Contributed by NM, 3Nov2005.)



Theorem  peano2uz 9040 
Second Peano postulate for an upper set of integers. (Contributed by NM,
7Sep2005.)



Theorem  peano2uzs 9041 
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26Dec2013.)



Theorem  peano2uzr 9042 
Reversed second Peano axiom for upper integers. (Contributed by NM,
2Jan2006.)



Theorem  uzaddcl 9043 
Addition closure law for an upper set of integers. (Contributed by NM,
4Jun2006.)



Theorem  nn0pzuz 9044 
The sum of a nonnegative integer and an integer is an integer greater than
or equal to that integer. (Contributed by Alexander van der Vekens,
3Oct2018.)



Theorem  uzind4 9045* 
Induction on the upper set of integers that starts 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, 7Sep2005.)



Theorem  uzind4ALT 9046* 
Induction on the upper set of integers that starts at an integer .
The last four hypotheses give us the substitution instances we need; the
first two are the basis and the induction step. Either uzind4 9045 or
uzind4ALT 9046 may be used; see comment for nnind 8410. (Contributed by NM,
7Sep2005.) (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  uzind4s 9047* 
Induction on the upper set of integers that starts at an integer ,
using explicit substitution. The hypotheses are the basis and the
induction step. (Contributed by NM, 4Nov2005.)



Theorem  uzind4s2 9048* 
Induction on the upper set of integers that starts at an integer ,
using explicit substitution. The hypotheses are the basis and the
induction step. Use this instead of uzind4s 9047 when and
must
be distinct in . (Contributed by NM,
16Nov2005.)



Theorem  uzind4i 9049* 
Induction on the upper integers that start at . The first
hypothesis specifies the lower bound, the next four give us the
substitution instances we need, and the last two are the basis and the
induction step. (Contributed by NM, 4Sep2005.)



Theorem  indstr 9050* 
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17Aug2001.)



Theorem  infrenegsupex 9051* 
The infimum of a set of reals is the negative of the supremum of
the negatives of its elements. (Contributed by Jim Kingdon,
14Jan2022.)

inf 

Theorem  supinfneg 9052* 
If a set of real numbers has a least upper bound, the set of the
negation of those numbers has a greatest lower bound. For a theorem
which is similar but only for the boundedness part, see ublbneg 9067.
(Contributed by Jim Kingdon, 15Jan2022.)



Theorem  infsupneg 9053* 
If a set of real numbers has a greatest lower bound, the set of the
negation of those numbers has a least upper bound. To go in the other
direction see supinfneg 9052. (Contributed by Jim Kingdon,
15Jan2022.)



Theorem  supminfex 9054* 
A supremum is the negation of the infimum of that set's image under
negation. (Contributed by Jim Kingdon, 14Jan2022.)

inf 

Theorem  eluznn0 9055 
Membership in a nonnegative upper set of integers implies membership in
.
(Contributed by Paul Chapman, 22Jun2011.)



Theorem  eluznn 9056 
Membership in a positive upper set of integers implies membership in
. (Contributed
by JJ, 1Oct2018.)



Theorem  eluz2b1 9057 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)



Theorem  eluz2gt1 9058 
An integer greater than or equal to 2 is greater than 1. (Contributed by
AV, 24May2020.)



Theorem  eluz2b2 9059 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)



Theorem  eluz2b3 9060 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)



Theorem  uz2m1nn 9061 
One less than an integer greater than or equal to 2 is a positive integer.
(Contributed by Paul Chapman, 17Nov2012.)



Theorem  1nuz2 9062 
1 is not in . (Contributed by Paul Chapman,
21Nov2012.)



Theorem  elnn1uz2 9063 
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17Nov2012.)



Theorem  uz2mulcl 9064 
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26Oct2012.)



Theorem  indstr2 9065* 
Strong Mathematical Induction for positive integers (inference schema).
The first two hypotheses give us the substitution instances we need; the
last two are the basis and the induction step. (Contributed by Paul
Chapman, 21Nov2012.)



Theorem  eluzdc 9066 
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18Apr2020.)

DECID


Theorem  ublbneg 9067* 
The image under negation of a boundedabove set of reals is bounded
below. For a theorem which is similar but also adds that the bounds
need to be the tightest possible, see supinfneg 9052. (Contributed by
Paul Chapman, 21Mar2011.)



Theorem  eqreznegel 9068* 
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21Mar2011.)



Theorem  negm 9069* 
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10Apr2020.)



Theorem  lbzbi 9070* 
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21Mar2011.)



Theorem  nn01to3 9071 
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13Sep2018.)



Theorem  nn0ge2m1nnALT 9072 
Alternate proof of nn0ge2m1nn 8703: If a nonnegative integer is greater
than or equal to two, the integer decreased by 1 is a positive integer.
This version is proved using eluz2 8994, a theorem for upper sets of
integers, which are defined later than the positive and nonnegative
integers. This proof is, however, much shorter than the proof of
nn0ge2m1nn 8703. (Contributed by Alexander van der Vekens,
1Aug2018.)
(New usage is discouraged.) (Proof modification is discouraged.)



3.4.12 Rational numbers (as a subset of complex
numbers)


Syntax  cq 9073 
Extend class notation to include the class of rationals.



Definition  dfq 9074 
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 9076
for the relation "is rational." (Contributed
by NM, 8Jan2002.)



Theorem  divfnzn 9075 
Division restricted to is a function. Given
excluded
middle, it would be easy to prove this for .
The key difference is that an element of is apart from zero,
whereas being an element of
implies being not equal to
zero. (Contributed by Jim Kingdon, 19Mar2020.)



Theorem  elq 9076* 
Membership in the set of rationals. (Contributed by NM, 8Jan2002.)
(Revised by Mario Carneiro, 28Jan2014.)



Theorem  qmulz 9077* 
If is rational, then
some integer multiple of it is an integer.
(Contributed by NM, 7Nov2008.) (Revised by Mario Carneiro,
22Jul2014.)



Theorem  znq 9078 
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12Jan2002.)



Theorem  qre 9079 
A rational number is a real number. (Contributed by NM,
14Nov2002.)



Theorem  zq 9080 
An integer is a rational number. (Contributed by NM, 9Jan2002.)



Theorem  zssq 9081 
The integers are a subset of the rationals. (Contributed by NM,
9Jan2002.)



Theorem  nn0ssq 9082 
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31Jul2004.)



Theorem  nnssq 9083 
The positive integers are a subset of the rationals. (Contributed by NM,
31Jul2004.)



Theorem  qssre 9084 
The rationals are a subset of the reals. (Contributed by NM,
9Jan2002.)



Theorem  qsscn 9085 
The rationals are a subset of the complex numbers. (Contributed by NM,
2Aug2004.)



Theorem  qex 9086 
The set of rational numbers exists. (Contributed by NM, 30Jul2004.)
(Revised by Mario Carneiro, 17Nov2014.)



Theorem  nnq 9087 
A positive integer is rational. (Contributed by NM, 17Nov2004.)



Theorem  qcn 9088 
A rational number is a complex number. (Contributed by NM,
2Aug2004.)



Theorem  qaddcl 9089 
Closure of addition of rationals. (Contributed by NM, 1Aug2004.)



Theorem  qnegcl 9090 
Closure law for the negative of a rational. (Contributed by NM,
2Aug2004.) (Revised by Mario Carneiro, 15Sep2014.)



Theorem  qmulcl 9091 
Closure of multiplication of rationals. (Contributed by NM,
1Aug2004.)



Theorem  qsubcl 9092 
Closure of subtraction of rationals. (Contributed by NM, 2Aug2004.)



Theorem  qapne 9093 
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20Mar2020.)

# 

Theorem  qltlen 9094 
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8083 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11Oct2021.)



Theorem  qlttri2 9095 
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9Nov2021.)



Theorem  qreccl 9096 
Closure of reciprocal of rationals. (Contributed by NM, 3Aug2004.)



Theorem  qdivcl 9097 
Closure of division of rationals. (Contributed by NM, 3Aug2004.)



Theorem  qrevaddcl 9098 
Reverse closure law for addition of rationals. (Contributed by NM,
2Aug2004.)



Theorem  nnrecq 9099 
The reciprocal of a positive integer is rational. (Contributed by NM,
17Nov2004.)



Theorem  irradd 9100 
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7Nov2008.)

