Type  Label  Description 
Statement 

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



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



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



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



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



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



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



Theorem  nn0pzuz 9408 
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 9409* 
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 9410* 
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 9409 or
uzind4ALT 9410 may be used; see comment for nnind 8759. (Contributed by NM,
7Sep2005.) (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  uzind4s 9411* 
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 9412* 
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 9411 when and
must
be distinct in . (Contributed by NM,
16Nov2005.)



Theorem  uzind4i 9413* 
Induction on the upper integers that start at . The first four
give us the substitution instances we need, and the last two are the
basis and the induction step. This is a stronger version of uzind4 9409
assuming that holds unconditionally. Notice that
implies that the lower bound
is an integer
( , see eluzel2 9354). (Contributed by NM, 4Sep2005.)
(Revised by AV, 13Jul2022.)



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



Theorem  infrenegsupex 9415* 
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 9416* 
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 9431.
(Contributed by Jim Kingdon, 15Jan2022.)



Theorem  infsupneg 9417* 
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 9416. (Contributed by Jim Kingdon,
15Jan2022.)



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

inf 

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



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



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



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



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



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



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



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



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



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



Theorem  indstr2 9429* 
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 9430 
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18Apr2020.)

DECID


Theorem  ublbneg 9431* 
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 9416. (Contributed by
Paul Chapman, 21Mar2011.)



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



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



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



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



Theorem  nn0ge2m1nnALT 9436 
Alternate proof of nn0ge2m1nn 9060: 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 9355, 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 9060. (Contributed by Alexander van der Vekens,
1Aug2018.)
(New usage is discouraged.) (Proof modification is discouraged.)



4.4.12 Rational numbers (as a subset of complex
numbers)


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



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



Theorem  divfnzn 9439 
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 9440* 
Membership in the set of rationals. (Contributed by NM, 8Jan2002.)
(Revised by Mario Carneiro, 28Jan2014.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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



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



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



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



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



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



Theorem  irrmul 9465 
The product of a real which is not rational with a nonzero rational is not
rational. Note that by "not rational" we mean the negation of
"is
rational" (whereas "irrational" is often defined to mean
apart from any
rational number  given excluded middle these two definitions would be
equivalent). (Contributed by NM, 7Nov2008.)



Theorem  elpq 9466* 
A positive rational is the quotient of two positive integers.
(Contributed by AV, 29Dec2022.)



Theorem  elpqb 9467* 
A class is a positive rational iff it is the quotient of two positive
integers. (Contributed by AV, 30Dec2022.)



4.4.13 Complex numbers as pairs of
reals


Theorem  cnref1o 9468* 
There is a natural onetoone mapping from
to ,
where we map to . In our
construction of the complex numbers, this is in fact our
definition of
(see dfc 7649), but in the axiomatic treatment we can only
show
that there is the expected mapping between these two sets. (Contributed
by Mario Carneiro, 16Jun2013.) (Revised by Mario Carneiro,
17Feb2014.)



4.5 Order sets


4.5.1 Positive reals (as a subset of complex
numbers)


Syntax  crp 9469 
Extend class notation to include the class of positive reals.



Definition  dfrp 9470 
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27Oct2007.)



Theorem  elrp 9471 
Membership in the set of positive reals. (Contributed by NM,
27Oct2007.)



Theorem  elrpii 9472 
Membership in the set of positive reals. (Contributed by NM,
23Feb2008.)



Theorem  1rp 9473 
1 is a positive real. (Contributed by Jeff Hankins, 23Nov2008.)



Theorem  2rp 9474 
2 is a positive real. (Contributed by Mario Carneiro, 28May2016.)



Theorem  3rp 9475 
3 is a positive real. (Contributed by Glauco Siliprandi, 11Dec2019.)



Theorem  rpre 9476 
A positive real is a real. (Contributed by NM, 27Oct2007.)



Theorem  rpxr 9477 
A positive real is an extended real. (Contributed by Mario Carneiro,
21Aug2015.)



Theorem  rpcn 9478 
A positive real is a complex number. (Contributed by NM, 11Nov2008.)



Theorem  nnrp 9479 
A positive integer is a positive real. (Contributed by NM,
28Nov2008.)



Theorem  rpssre 9480 
The positive reals are a subset of the reals. (Contributed by NM,
24Feb2008.)



Theorem  rpgt0 9481 
A positive real is greater than zero. (Contributed by FL,
27Dec2007.)



Theorem  rpge0 9482 
A positive real is greater than or equal to zero. (Contributed by NM,
22Feb2008.)



Theorem  rpregt0 9483 
A positive real is a positive real number. (Contributed by NM,
11Nov2008.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  rprege0 9484 
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31Jan2014.)



Theorem  rpne0 9485 
A positive real is nonzero. (Contributed by NM, 18Jul2008.)



Theorem  rpap0 9486 
A positive real is apart from zero. (Contributed by Jim Kingdon,
22Mar2020.)

# 

Theorem  rprene0 9487 
A positive real is a nonzero real number. (Contributed by NM,
11Nov2008.)



Theorem  rpreap0 9488 
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22Mar2020.)

# 

Theorem  rpcnne0 9489 
A positive real is a nonzero complex number. (Contributed by NM,
11Nov2008.)



Theorem  rpcnap0 9490 
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22Mar2020.)

# 

Theorem  ralrp 9491 
Quantification over positive reals. (Contributed by NM, 12Feb2008.)



Theorem  rexrp 9492 
Quantification over positive reals. (Contributed by Mario Carneiro,
21May2014.)



Theorem  rpaddcl 9493 
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27Oct2007.)



Theorem  rpmulcl 9494 
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27Oct2007.)



Theorem  rpdivcl 9495 
Closure law for division of positive reals. (Contributed by FL,
27Dec2007.)



Theorem  rpreccl 9496 
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23Nov2008.)



Theorem  rphalfcl 9497 
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31Jan2014.)



Theorem  rpgecl 9498 
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  rphalflt 9499 
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21May2014.)



Theorem  rerpdivcl 9500 
Closure law for division of a real by a positive real. (Contributed by
NM, 10Nov2008.)

