Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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



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



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



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



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



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



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



3.4.13 Complex numbers as pairs of
reals


Theorem  cnref1o 9028* 
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 7259), 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.)



3.5 Order sets


3.5.1 Positive reals (as a subset of complex
numbers)


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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

# 

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



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

# 

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



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



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



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



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



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



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



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



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



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



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



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

#


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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ltrecd 9087 
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  lerecd 9088 
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  ltrec1d 9089 
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  lerec2d 9090 
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  lediv2ad 9091 
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28May2016.)



Theorem  ltdiv2d 9092 
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  lediv2d 9093 
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  ledivdivd 9094 
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  divge1 9095 
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5Apr2020.)



Theorem  divlt1lt 9096 
A real number divided by a positive real number is less than 1 iff the
real number is less than the positive real number. (Contributed by AV,
25May2020.)



Theorem  divle1le 9097 
A real number divided by a positive real number is less than or equal to 1
iff the real number is less than or equal to the positive real number.
(Contributed by AV, 29Jun2021.)



Theorem  ledivge1le 9098 
If a number is less than or equal to another number, the number divided by
a positive number greater than or equal to one is less than or equal to
the other number. (Contributed by AV, 29Jun2021.)



Theorem  ge0p1rpd 9099 
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  rerpdivcld 9100 
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28May2016.)

