Type  Label  Description 
Statement 

Theorem  nqprloc 6701* 
A cut produced from a rational is located. Lemma for nqprlu 6703.
(Contributed by Jim Kingdon, 8Dec2019.)



Theorem  nqprxx 6702* 
The canonical embedding of the rationals into the reals, expressed with
the same variable for the lower and upper cuts. (Contributed by Jim
Kingdon, 8Dec2019.)



Theorem  nqprlu 6703* 
The canonical embedding of the rationals into the reals. (Contributed
by Jim Kingdon, 24Jun2020.)



Theorem  recnnpr 6704* 
The reciprocal of a positive integer, as a positive real. (Contributed
by Jim Kingdon, 27Feb2021.)



Theorem  ltnqex 6705 
The class of rationals less than a given rational is a set.
(Contributed by Jim Kingdon, 13Dec2019.)



Theorem  gtnqex 6706 
The class of rationals greater than a given rational is a set.
(Contributed by Jim Kingdon, 13Dec2019.)



Theorem  nqprl 6707* 
Comparing a fraction to a real can be done by whether it is an element
of the lower cut, or by . (Contributed by Jim Kingdon,
8Jul2020.)



Theorem  nqpru 6708* 
Comparing a fraction to a real can be done by whether it is an element
of the upper cut, or by . (Contributed by Jim Kingdon,
29Nov2020.)



Theorem  nnprlu 6709* 
The canonical embedding of positive integers into the positive reals.
(Contributed by Jim Kingdon, 23Apr2020.)



Theorem  1pr 6710 
The positive real number 'one'. (Contributed by NM, 13Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)



Theorem  1prl 6711 
The lower cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28Dec2019.)



Theorem  1pru 6712 
The upper cut of the positive real number 'one'. (Contributed by Jim
Kingdon, 28Dec2019.)



Theorem  addnqprlemrl 6713* 
Lemma for addnqpr 6717. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19Aug2020.)



Theorem  addnqprlemru 6714* 
Lemma for addnqpr 6717. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 19Aug2020.)



Theorem  addnqprlemfl 6715* 
Lemma for addnqpr 6717. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 19Aug2020.)



Theorem  addnqprlemfu 6716* 
Lemma for addnqpr 6717. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 19Aug2020.)



Theorem  addnqpr 6717* 
Addition of fractions embedded into positive reals. One can either add
the fractions as fractions, or embed them into positive reals and add
them as positive reals, and get the same result. (Contributed by Jim
Kingdon, 19Aug2020.)



Theorem  addnqpr1 6718* 
Addition of one to a fraction embedded into a positive real. One can
either add the fraction one to the fraction, or the positive real one to
the positive real, and get the same result. Special case of addnqpr 6717.
(Contributed by Jim Kingdon, 26Apr2020.)



Theorem  appdivnq 6719* 
Approximate division for positive rationals. Proposition 12.7 of
[BauerTaylor], p. 55 (a special case
where and are positive,
as well as ).
Our proof is simpler than the one in BauerTaylor
because we have reciprocals. (Contributed by Jim Kingdon,
8Dec2019.)



Theorem  appdiv0nq 6720* 
Approximate division for positive rationals. This can be thought of as
a variation of appdivnq 6719 in which is zero, although it can be
stated and proved in terms of positive rationals alone, without zero as
such. (Contributed by Jim Kingdon, 9Dec2019.)



Theorem  prmuloclemcalc 6721 
Calculations for prmuloc 6722. (Contributed by Jim Kingdon,
9Dec2019.)



Theorem  prmuloc 6722* 
Positive reals are multiplicatively located. Lemma 12.8 of
[BauerTaylor], p. 56. (Contributed
by Jim Kingdon, 8Dec2019.)



Theorem  prmuloc2 6723* 
Positive reals are multiplicatively located. This is a variation of
prmuloc 6722 which only constructs one (named) point and
is therefore often
easier to work with. It states that given a ratio , there are
elements of the lower and upper cut which have exactly that ratio
between them. (Contributed by Jim Kingdon, 28Dec2019.)



Theorem  mulnqprl 6724 
Lemma to prove downward closure in positive real multiplication.
(Contributed by Jim Kingdon, 10Dec2019.)



Theorem  mulnqpru 6725 
Lemma to prove upward closure in positive real multiplication.
(Contributed by Jim Kingdon, 10Dec2019.)



Theorem  mullocprlem 6726 
Calculations for mullocpr 6727. (Contributed by Jim Kingdon,
10Dec2019.)



Theorem  mullocpr 6727* 
Locatedness of multiplication on positive reals. Lemma 12.9 in
[BauerTaylor], p. 56 (but where both
and are positive, not
just ).
(Contributed by Jim Kingdon, 8Dec2019.)



Theorem  mulclpr 6728 
Closure of multiplication on positive reals. First statement of
Proposition 93.7 of [Gleason] p. 124.
(Contributed by NM,
13Mar1996.)



Theorem  mulnqprlemrl 6729* 
Lemma for mulnqpr 6733. The reverse subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 18Jul2021.)



Theorem  mulnqprlemru 6730* 
Lemma for mulnqpr 6733. The reverse subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 18Jul2021.)



Theorem  mulnqprlemfl 6731* 
Lemma for mulnqpr 6733. The forward subset relationship for the
lower
cut. (Contributed by Jim Kingdon, 18Jul2021.)



Theorem  mulnqprlemfu 6732* 
Lemma for mulnqpr 6733. The forward subset relationship for the
upper
cut. (Contributed by Jim Kingdon, 18Jul2021.)



Theorem  mulnqpr 6733* 
Multiplication of fractions embedded into positive reals. One can
either multiply the fractions as fractions, or embed them into positive
reals and multiply them as positive reals, and get the same result.
(Contributed by Jim Kingdon, 18Jul2021.)



Theorem  addcomprg 6734 
Addition of positive reals is commutative. Proposition 93.5(ii) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 11Dec2019.)



Theorem  addassprg 6735 
Addition of positive reals is associative. Proposition 93.5(i) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 11Dec2019.)



Theorem  mulcomprg 6736 
Multiplication of positive reals is commutative. Proposition 93.7(ii)
of [Gleason] p. 124. (Contributed by
Jim Kingdon, 11Dec2019.)



Theorem  mulassprg 6737 
Multiplication of positive reals is associative. Proposition 93.7(i)
of [Gleason] p. 124. (Contributed by
Jim Kingdon, 11Dec2019.)



Theorem  distrlem1prl 6738 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)



Theorem  distrlem1pru 6739 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)



Theorem  distrlem4prl 6740* 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)



Theorem  distrlem4pru 6741* 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)



Theorem  distrlem5prl 6742 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)



Theorem  distrlem5pru 6743 
Lemma for distributive law for positive reals. (Contributed by Jim
Kingdon, 12Dec2019.)



Theorem  distrprg 6744 
Multiplication of positive reals is distributive. Proposition
93.7(iii) of [Gleason] p. 124.
(Contributed by Jim Kingdon,
12Dec2019.)



Theorem  ltprordil 6745 
If a positive real is less than a second positive real, its lower cut is
a subset of the second's lower cut. (Contributed by Jim Kingdon,
23Dec2019.)



Theorem  1idprl 6746 
Lemma for 1idpr 6748. (Contributed by Jim Kingdon, 13Dec2019.)



Theorem  1idpru 6747 
Lemma for 1idpr 6748. (Contributed by Jim Kingdon, 13Dec2019.)



Theorem  1idpr 6748 
1 is an identity element for positive real multiplication. Theorem
93.7(iv) of [Gleason] p. 124.
(Contributed by NM, 2Apr1996.)



Theorem  ltnqpr 6749* 
We can order fractions via or . (Contributed by Jim
Kingdon, 19Jun2021.)



Theorem  ltnqpri 6750* 
We can order fractions via or . (Contributed by Jim
Kingdon, 8Jan2021.)



Theorem  ltpopr 6751 
Positive real 'less than' is a partial ordering. Remark ("< is
transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p.
(varies). Lemma for ltsopr 6752. (Contributed by Jim Kingdon,
15Dec2019.)



Theorem  ltsopr 6752 
Positive real 'less than' is a weak linear order (in the sense of
dfiso 4062). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed
by Jim Kingdon, 16Dec2019.)



Theorem  ltaddpr 6753 
The sum of two positive reals is greater than one of them. Proposition
93.5(iii) of [Gleason] p. 123.
(Contributed by NM, 26Mar1996.)
(Revised by Mario Carneiro, 12Jun2013.)



Theorem  ltexprlemell 6754* 
Element in lower cut of the constructed difference. Lemma for
ltexpri 6769. (Contributed by Jim Kingdon, 21Dec2019.)



Theorem  ltexprlemelu 6755* 
Element in upper cut of the constructed difference. Lemma for
ltexpri 6769. (Contributed by Jim Kingdon, 21Dec2019.)



Theorem  ltexprlemm 6756* 
Our constructed difference is inhabited. Lemma for ltexpri 6769.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemopl 6757* 
The lower cut of our constructed difference is open. Lemma for
ltexpri 6769. (Contributed by Jim Kingdon, 21Dec2019.)



Theorem  ltexprlemlol 6758* 
The lower cut of our constructed difference is lower. Lemma for
ltexpri 6769. (Contributed by Jim Kingdon, 21Dec2019.)



Theorem  ltexprlemopu 6759* 
The upper cut of our constructed difference is open. Lemma for
ltexpri 6769. (Contributed by Jim Kingdon, 21Dec2019.)



Theorem  ltexprlemupu 6760* 
The upper cut of our constructed difference is upper. Lemma for
ltexpri 6769. (Contributed by Jim Kingdon, 21Dec2019.)



Theorem  ltexprlemrnd 6761* 
Our constructed difference is rounded. Lemma for ltexpri 6769.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemdisj 6762* 
Our constructed difference is disjoint. Lemma for ltexpri 6769.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemloc 6763* 
Our constructed difference is located. Lemma for ltexpri 6769.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlempr 6764* 
Our constructed difference is a positive real. Lemma for ltexpri 6769.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemfl 6765* 
Lemma for ltexpri 6769. One directon of our result for lower cuts.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemrl 6766* 
Lemma for ltexpri 6769. Reverse directon of our result for lower
cuts.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemfu 6767* 
Lemma for ltexpri 6769. One direction of our result for upper cuts.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexprlemru 6768* 
Lemma for ltexpri 6769. One direction of our result for upper cuts.
(Contributed by Jim Kingdon, 17Dec2019.)



Theorem  ltexpri 6769* 
Proposition 93.5(iv) of [Gleason] p. 123.
(Contributed by NM,
13May1996.) (Revised by Mario Carneiro, 14Jun2013.)



Theorem  addcanprleml 6770 
Lemma for addcanprg 6772. (Contributed by Jim Kingdon, 25Dec2019.)



Theorem  addcanprlemu 6771 
Lemma for addcanprg 6772. (Contributed by Jim Kingdon, 25Dec2019.)



Theorem  addcanprg 6772 
Addition cancellation law for positive reals. Proposition 93.5(vi) of
[Gleason] p. 123. (Contributed by Jim
Kingdon, 24Dec2019.)



Theorem  lteupri 6773* 
The difference from ltexpri 6769 is unique. (Contributed by Jim Kingdon,
7Jul2021.)



Theorem  ltaprlem 6774 
Lemma for Proposition 93.5(v) of [Gleason] p.
123. (Contributed by NM,
8Apr1996.)



Theorem  ltaprg 6775 
Ordering property of addition. Proposition 93.5(v) of [Gleason]
p. 123. (Contributed by Jim Kingdon, 26Dec2019.)



Theorem  prplnqu 6776* 
Membership in the upper cut of a sum of a positive real and a fraction.
(Contributed by Jim Kingdon, 16Jun2021.)



Theorem  addextpr 6777 
Strong extensionality of addition (ordering version). This is similar
to addext 7675 but for positive reals and based on lessthan
rather than
apartness. (Contributed by Jim Kingdon, 17Feb2020.)



Theorem  recexprlemell 6778* 
Membership in the lower cut of . Lemma for recexpr 6794.
(Contributed by Jim Kingdon, 27Dec2019.)



Theorem  recexprlemelu 6779* 
Membership in the upper cut of . Lemma for recexpr 6794.
(Contributed by Jim Kingdon, 27Dec2019.)



Theorem  recexprlemm 6780* 
is inhabited. Lemma
for recexpr 6794. (Contributed by Jim Kingdon,
27Dec2019.)



Theorem  recexprlemopl 6781* 
The lower cut of is
open. Lemma for recexpr 6794. (Contributed by
Jim Kingdon, 28Dec2019.)



Theorem  recexprlemlol 6782* 
The lower cut of is
lower. Lemma for recexpr 6794. (Contributed by
Jim Kingdon, 28Dec2019.)



Theorem  recexprlemopu 6783* 
The upper cut of is
open. Lemma for recexpr 6794. (Contributed by
Jim Kingdon, 28Dec2019.)



Theorem  recexprlemupu 6784* 
The upper cut of is
upper. Lemma for recexpr 6794. (Contributed by
Jim Kingdon, 28Dec2019.)



Theorem  recexprlemrnd 6785* 
is rounded. Lemma
for recexpr 6794. (Contributed by Jim Kingdon,
27Dec2019.)



Theorem  recexprlemdisj 6786* 
is disjoint. Lemma
for recexpr 6794. (Contributed by Jim Kingdon,
27Dec2019.)



Theorem  recexprlemloc 6787* 
is located. Lemma
for recexpr 6794. (Contributed by Jim Kingdon,
27Dec2019.)



Theorem  recexprlempr 6788* 
is a positive real.
Lemma for recexpr 6794. (Contributed by Jim
Kingdon, 27Dec2019.)



Theorem  recexprlem1ssl 6789* 
The lower cut of one is a subset of the lower cut of .
Lemma for recexpr 6794. (Contributed by Jim Kingdon, 27Dec2019.)



Theorem  recexprlem1ssu 6790* 
The upper cut of one is a subset of the upper cut of .
Lemma for recexpr 6794. (Contributed by Jim Kingdon, 27Dec2019.)



Theorem  recexprlemss1l 6791* 
The lower cut of is a subset of the lower cut of one.
Lemma
for recexpr 6794. (Contributed by Jim Kingdon, 27Dec2019.)



Theorem  recexprlemss1u 6792* 
The upper cut of is a subset of the upper cut of one.
Lemma
for recexpr 6794. (Contributed by Jim Kingdon, 27Dec2019.)



Theorem  recexprlemex 6793* 
is the reciprocal of
. Lemma for recexpr 6794. (Contributed
by Jim Kingdon, 27Dec2019.)



Theorem  recexpr 6794* 
The reciprocal of a positive real exists. Part of Proposition 93.7(v)
of [Gleason] p. 124. (Contributed by
NM, 15May1996.) (Revised by
Mario Carneiro, 12Jun2013.)



Theorem  aptiprleml 6795 
Lemma for aptipr 6797. (Contributed by Jim Kingdon, 28Jan2020.)



Theorem  aptiprlemu 6796 
Lemma for aptipr 6797. (Contributed by Jim Kingdon, 28Jan2020.)



Theorem  aptipr 6797 
Apartness of positive reals is tight. (Contributed by Jim Kingdon,
28Jan2020.)



Theorem  ltmprr 6798 
Ordering property of multiplication. (Contributed by Jim Kingdon,
18Feb2020.)



Theorem  archpr 6799* 
For any positive real, there is an integer that is greater than it.
This is also known as the "archimedean property". The integer
is
embedded into the reals as described at nnprlu 6709. (Contributed by Jim
Kingdon, 22Apr2020.)



Theorem  caucvgprlemcanl 6800* 
Lemma for cauappcvgprlemladdrl 6813. Cancelling a term from both sides.
(Contributed by Jim Kingdon, 15Aug2020.)

