Type  Label  Description 
Statement 

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



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



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



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



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

DECID


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



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



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



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



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



Theorem  nn0ge2m1nnALT 9312 
Alternate proof of nn0ge2m1nn 8941: 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 9234, 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 8941. (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 9313 
Extend class notation to include the class of rationals.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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



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



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



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



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



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



Theorem  irrmul 9341 
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.)



4.4.13 Complex numbers as pairs of
reals


Theorem  cnref1o 9342* 
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 7553), 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 9343 
Extend class notation to include the class of positive reals.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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

# 

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



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

# 

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



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



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



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



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



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



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



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



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



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



Theorem  ge0p1rp 9374 
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5Oct2015.)



Theorem  rpnegap 9375 
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23Mar2020.)

#


Theorem  0nrp 9376 
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27Oct2007.)



Theorem  ltsubrp 9377 
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27Dec2007.)



Theorem  ltaddrp 9378 
Adding a positive number to another number increases it. (Contributed by
FL, 27Dec2007.)



Theorem  difrp 9379 
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21May2014.)



Theorem  elrpd 9380 
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  nnrpd 9381 
A positive integer is a positive real. (Contributed by Mario Carneiro,
28May2016.)



Theorem  rpred 9382 
A positive real is a real. (Contributed by Mario Carneiro,
28May2016.)



Theorem  rpxrd 9383 
A positive real is an extended real. (Contributed by Mario Carneiro,
28May2016.)



Theorem  rpcnd 9384 
A positive real is a complex number. (Contributed by Mario Carneiro,
28May2016.)



Theorem  rpgt0d 9385 
A positive real is greater than zero. (Contributed by Mario Carneiro,
28May2016.)



Theorem  rpge0d 9386 
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rpne0d 9387 
A positive real is nonzero. (Contributed by Mario Carneiro,
28May2016.)



Theorem  rpap0d 9388 
A positive real is apart from zero. (Contributed by Jim Kingdon,
28Jul2021.)

# 

Theorem  rpregt0d 9389 
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rprege0d 9390 
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  rprene0d 9391 
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rpcnne0d 9392 
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rpreccld 9393 
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rprecred 9394 
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rphalfcld 9395 
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  reclt1d 9396 
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  recgt1d 9397 
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  rpaddcld 9398 
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rpmulcld 9399 
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  rpdivcld 9400 
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28May2016.)

