Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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

# 

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



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



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



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



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



Theorem  irrmul 8316 
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.12 Complex numbers as pairs of
reals


Theorem  cnref1o 8317* 
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 6677), 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 8318 
Extend class notation to include the class of positive reals.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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

# 

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



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

# 

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



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



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



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



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



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



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



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



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



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



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



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

# 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  ltsubrpd 8385 
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  ltaddrpd 8386 
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  ltaddrp2d 8387 
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28May2016.)



Theorem  ltmulgt11d 8388 
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  ltmulgt12d 8389 
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28May2016.)



Theorem  gt0divd 8390 
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28May2016.)



Theorem  ge0divd 8391 
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28May2016.)



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



Theorem  divge0d 8393 
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  ltmul1d 8394 
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  ltmul2d 8395 
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
28May2016.)



Theorem  lemul1d 8396 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28May2016.)



Theorem  lemul2d 8397 
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28May2016.)



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



Theorem  lediv1d 8399 
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28May2016.)



Theorem  ltmuldivd 8400 
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28May2016.)

