Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



Theorem  recexpr 6610* 
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 6611 
Lemma for aptipr 6613. (Contributed by Jim Kingdon, 28Jan2020.)



Theorem  aptiprlemu 6612 
Lemma for aptipr 6613. (Contributed by Jim Kingdon, 28Jan2020.)



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



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



Theorem  archpr 6615* 
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 6534. (Contributed by Jim
Kingdon, 22Apr2020.)



Theorem  cauappcvgprlemcan 6616* 
Lemma for cauappcvgprlemladdrl 6629. Cancelling a term from both sides.
(Contributed by Jim Kingdon, 15Aug2020.)



Theorem  cauappcvgprlemm 6617* 
Lemma for cauappcvgpr 6634. The putative limit is inhabited.
(Contributed by Jim Kingdon, 18Jul2020.)



Theorem  cauappcvgprlemopl 6618* 
Lemma for cauappcvgpr 6634. The lower cut of the putative limit is
open. (Contributed by Jim Kingdon, 4Aug2020.)



Theorem  cauappcvgprlemlol 6619* 
Lemma for cauappcvgpr 6634. The lower cut of the putative limit is
lower. (Contributed by Jim Kingdon, 4Aug2020.)



Theorem  cauappcvgprlemopu 6620* 
Lemma for cauappcvgpr 6634. The upper cut of the putative limit is
open. (Contributed by Jim Kingdon, 4Aug2020.)



Theorem  cauappcvgprlemupu 6621* 
Lemma for cauappcvgpr 6634. The upper cut of the putative limit is
upper. (Contributed by Jim Kingdon, 4Aug2020.)



Theorem  cauappcvgprlemrnd 6622* 
Lemma for cauappcvgpr 6634. The putative limit is rounded.
(Contributed by Jim Kingdon, 18Jul2020.)



Theorem  cauappcvgprlemdisj 6623* 
Lemma for cauappcvgpr 6634. The putative limit is disjoint.
(Contributed by Jim Kingdon, 18Jul2020.)



Theorem  cauappcvgprlemloc 6624* 
Lemma for cauappcvgpr 6634. The putative limit is located.
(Contributed by Jim Kingdon, 18Jul2020.)



Theorem  cauappcvgprlemcl 6625* 
Lemma for cauappcvgpr 6634. The putative limit is a positive real.
(Contributed by Jim Kingdon, 20Jun2020.)



Theorem  cauappcvgprlemladdfu 6626* 
Lemma for cauappcvgprlemladd 6630. The forward subset relationship
for the upper cut. (Contributed by Jim Kingdon, 11Jul2020.)



Theorem  cauappcvgprlemladdfl 6627* 
Lemma for cauappcvgprlemladd 6630. The forward subset relationship
for the lower cut. (Contributed by Jim Kingdon, 11Jul2020.)



Theorem  cauappcvgprlemladdru 6628* 
Lemma for cauappcvgprlemladd 6630. The reverse subset relationship
for the upper cut. (Contributed by Jim Kingdon, 11Jul2020.)



Theorem  cauappcvgprlemladdrl 6629* 
Lemma for cauappcvgprlemladd 6630. The forward subset relationship
for the lower cut. (Contributed by Jim Kingdon, 11Jul2020.)



Theorem  cauappcvgprlemladd 6630* 
Lemma for cauappcvgpr 6634. This takes and offsets it by the
positive fraction . (Contributed by Jim Kingdon,
23Jun2020.)



Theorem  cauappcvgprlem1 6631* 
Lemma for cauappcvgpr 6634. Part of showing the putative limit to be
a limit. (Contributed by Jim Kingdon, 23Jun2020.)



Theorem  cauappcvgprlem2 6632* 
Lemma for cauappcvgpr 6634. Part of showing the putative limit to be
a limit. (Contributed by Jim Kingdon, 23Jun2020.)



Theorem  cauappcvgprlemlim 6633* 
Lemma for cauappcvgpr 6634. The putative limit is a limit.
(Contributed by Jim Kingdon, 20Jun2020.)



Theorem  cauappcvgpr 6634* 
A Cauchy approximation has a limit. A Cauchy approximation, here
, is similar
to a Cauchy sequence but is indexed by the desired
tolerance (that is, how close together terms needs to be) rather than
by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p.
(varies) with a few differences such as that we are proving the
existence of a limit without anything about how fast it converges
(that is, mere existence instead of existence, in HoTT terms), and
that the codomain of is
rather than . We
also
specify that every term needs to be larger than a fraction , to
avoid the case where we have positive fractions which converge to zero
(which is not a positive real). (Contributed by Jim Kingdon,
19Jun2020.)



Theorem  archrecnq 6635* 
Archimedean principle for fractions (reciprocal version). (Contributed
by Jim Kingdon, 27Sep2020.)



Theorem  caucvgprlemk 6636 
Lemma for caucvgpr 6653. Reciprocals of positive integers decrease
as the
positive integers increase. (Contributed by Jim Kingdon,
9Oct2020.)



Theorem  caucvgprlemnkj 6637* 
Lemma for caucvgpr 6653. Part of disjointness. (Contributed by Jim
Kingdon, 23Oct2020.)



Theorem  caucvgprlemnbj 6638* 
Lemma for caucvgpr 6653. Nonexistence of two elements of the
sequence
which are too far from each other. (Contributed by Jim Kingdon,
18Oct2020.)



Theorem  caucvgprlemm 6639* 
Lemma for caucvgpr 6653. The putative limit is inhabited.
(Contributed by Jim Kingdon, 27Sep2020.)



Theorem  caucvgprlemopl 6640* 
Lemma for caucvgpr 6653. The lower cut of the putative limit is
open. (Contributed by Jim Kingdon, 20Oct2020.)



Theorem  caucvgprlemlol 6641* 
Lemma for caucvgpr 6653. The lower cut of the putative limit is
lower. (Contributed by Jim Kingdon, 20Oct2020.)



Theorem  caucvgprlemopu 6642* 
Lemma for caucvgpr 6653. The upper cut of the putative limit is
open. (Contributed by Jim Kingdon, 20Oct2020.)



Theorem  caucvgprlemupu 6643* 
Lemma for caucvgpr 6653. The upper cut of the putative limit is
upper. (Contributed by Jim Kingdon, 20Oct2020.)



Theorem  caucvgprlemrnd 6644* 
Lemma for caucvgpr 6653. The putative limit is rounded.
(Contributed
by Jim Kingdon, 27Sep2020.)



Theorem  caucvgprlemdisj 6645* 
Lemma for caucvgpr 6653. The putative limit is disjoint.
(Contributed by Jim Kingdon, 27Sep2020.)



Theorem  caucvgprlemloc 6646* 
Lemma for caucvgpr 6653. The putative limit is located.
(Contributed
by Jim Kingdon, 27Sep2020.)



Theorem  caucvgprlemcl 6647* 
Lemma for caucvgpr 6653. The putative limit is a positive real.
(Contributed by Jim Kingdon, 26Sep2020.)



Theorem  caucvgprlemladdfu 6648* 
Lemma for caucvgpr 6653. Adding after embedding in positive
reals, or adding it as a rational. (Contributed by Jim Kingdon,
9Oct2020.)



Theorem  caucvgprlemladdrl 6649* 
Lemma for caucvgpr 6653. Adding after embedding in positive
reals, or adding it as a rational. (Contributed by Jim Kingdon,
8Oct2020.)



Theorem  caucvgprlem1 6650* 
Lemma for caucvgpr 6653. Part of showing the putative limit to be a
limit. (Contributed by Jim Kingdon, 3Oct2020.)



Theorem  caucvgprlem2 6651* 
Lemma for caucvgpr 6653. Part of showing the putative limit to be a
limit. (Contributed by Jim Kingdon, 3Oct2020.)



Theorem  caucvgprlemlim 6652* 
Lemma for caucvgpr 6653. The putative limit is a limit.
(Contributed
by Jim Kingdon, 1Oct2020.)



Theorem  caucvgpr 6653* 
A Cauchy sequence of positive fractions with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
of the nth term (it should later be able
to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a fraction , to avoid the case
where we have positive fractions which converge to zero (which is not
a positive real). (Contributed by Jim Kingdon, 18Jun2020.)



Definition  dfenr 6654* 
Define equivalence relation for signed reals. This is a "temporary"
set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 94.1 of [Gleason] p. 126.
(Contributed by NM, 25Jul1995.)



Definition  dfnr 6655 
Define class of signed reals. This is a "temporary" set used in the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.2 of [Gleason] p. 126. (Contributed
by NM, 25Jul1995.)



Definition  dfplr 6656* 
Define addition on signed reals. This is a "temporary" set used in
the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.3 of [Gleason] p. 126. (Contributed
by NM, 25Aug1995.)



Definition  dfmr 6657* 
Define multiplication on signed reals. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. From Proposition 94.3 of [Gleason] p. 126.
(Contributed by NM, 25Aug1995.)



Definition  dfltr 6658* 
Define ordering relation on signed reals. This is a "temporary" set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 94.4 of [Gleason] p. 127.
(Contributed by NM, 14Feb1996.)



Definition  df0r 6659 
Define signed real constant 0. This is a "temporary" set used in the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.2 of [Gleason] p. 126. (Contributed
by NM, 9Aug1995.)



Definition  df1r 6660 
Define signed real constant 1. This is a "temporary" set used in the
construction of complex numbers, and is intended to be used only by the
construction. From Proposition 94.2 of [Gleason] p. 126. (Contributed
by NM, 9Aug1995.)



Definition  dfm1r 6661 
Define signed real constant 1. This is a "temporary" set used in
the
construction of complex numbers, and is intended to be used only by the
construction. (Contributed by NM, 9Aug1995.)



Theorem  enrbreq 6662 
Equivalence relation for signed reals in terms of positive reals.
(Contributed by NM, 3Sep1995.)



Theorem  enrer 6663 
The equivalence relation for signed reals is an equivalence relation.
Proposition 94.1 of [Gleason] p. 126.
(Contributed by NM,
3Sep1995.) (Revised by Mario Carneiro, 6Jul2015.)



Theorem  enreceq 6664 
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29Nov1995.)



Theorem  enrex 6665 
The equivalence relation for signed reals exists. (Contributed by NM,
25Jul1995.)



Theorem  ltrelsr 6666 
Signed real 'less than' is a relation on signed reals. (Contributed by
NM, 14Feb1996.)



Theorem  addcmpblnr 6667 
Lemma showing compatibility of addition. (Contributed by NM,
3Sep1995.)



Theorem  mulcmpblnrlemg 6668 
Lemma used in lemma showing compatibility of multiplication.
(Contributed by Jim Kingdon, 1Jan2020.)



Theorem  mulcmpblnr 6669 
Lemma showing compatibility of multiplication. (Contributed by NM,
5Sep1995.)



Theorem  prsrlem1 6670* 
Decomposing signed reals into positive reals. Lemma for addsrpr 6673 and
mulsrpr 6674. (Contributed by Jim Kingdon, 30Dec2019.)



Theorem  addsrmo 6671* 
There is at most one result from adding signed reals. (Contributed by
Jim Kingdon, 30Dec2019.)



Theorem  mulsrmo 6672* 
There is at most one result from multiplying signed reals. (Contributed
by Jim Kingdon, 30Dec2019.)



Theorem  addsrpr 6673 
Addition of signed reals in terms of positive reals. (Contributed by
NM, 3Sep1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  mulsrpr 6674 
Multiplication of signed reals in terms of positive reals. (Contributed
by NM, 3Sep1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ltsrprg 6675 
Ordering of signed reals in terms of positive reals. (Contributed by
Jim Kingdon, 2Jan2019.)



Theorem  gt0srpr 6676 
Greater than zero in terms of positive reals. (Contributed by NM,
13May1996.)



Theorem  0nsr 6677 
The empty set is not a signed real. (Contributed by NM, 25Aug1995.)
(Revised by Mario Carneiro, 10Jul2014.)



Theorem  0r 6678 
The constant is a
signed real. (Contributed by NM, 9Aug1995.)



Theorem  1sr 6679 
The constant is a
signed real. (Contributed by NM, 9Aug1995.)



Theorem  m1r 6680 
The constant is
a signed real. (Contributed by NM,
9Aug1995.)



Theorem  addclsr 6681 
Closure of addition on signed reals. (Contributed by NM,
25Jul1995.)



Theorem  mulclsr 6682 
Closure of multiplication on signed reals. (Contributed by NM,
10Aug1995.)



Theorem  addcomsrg 6683 
Addition of signed reals is commutative. (Contributed by Jim Kingdon,
3Jan2020.)



Theorem  addasssrg 6684 
Addition of signed reals is associative. (Contributed by Jim Kingdon,
3Jan2020.)



Theorem  mulcomsrg 6685 
Multiplication of signed reals is commutative. (Contributed by Jim
Kingdon, 3Jan2020.)



Theorem  mulasssrg 6686 
Multiplication of signed reals is associative. (Contributed by Jim
Kingdon, 3Jan2020.)



Theorem  distrsrg 6687 
Multiplication of signed reals is distributive. (Contributed by Jim
Kingdon, 4Jan2020.)



Theorem  m1p1sr 6688 
Minus one plus one is zero for signed reals. (Contributed by NM,
5May1996.)



Theorem  m1m1sr 6689 
Minus one times minus one is plus one for signed reals. (Contributed by
NM, 14May1996.)



Theorem  lttrsr 6690* 
Signed real 'less than' is a transitive relation. (Contributed by Jim
Kingdon, 4Jan2019.)



Theorem  ltposr 6691 
Signed real 'less than' is a partial order. (Contributed by Jim
Kingdon, 4Jan2019.)



Theorem  ltsosr 6692 
Signed real 'less than' is a strict ordering. (Contributed by NM,
19Feb1996.)



Theorem  0lt1sr 6693 
0 is less than 1 for signed reals. (Contributed by NM, 26Mar1996.)



Theorem  1ne0sr 6694 
1 and 0 are distinct for signed reals. (Contributed by NM,
26Mar1996.)



Theorem  0idsr 6695 
The signed real number 0 is an identity element for addition of signed
reals. (Contributed by NM, 10Apr1996.)



Theorem  1idsr 6696 
1 is an identity element for multiplication. (Contributed by Jim
Kingdon, 5Jan2020.)



Theorem  00sr 6697 
A signed real times 0 is 0. (Contributed by NM, 10Apr1996.)



Theorem  ltasrg 6698 
Ordering property of addition. (Contributed by NM, 10May1996.)



Theorem  pn0sr 6699 
A signed real plus its negative is zero. (Contributed by NM,
14May1996.)



Theorem  negexsr 6700* 
Existence of negative signed real. Part of Proposition 94.3 of
[Gleason] p. 126. (Contributed by NM,
2May1996.)

