Theorem List for Intuitionistic Logic Explorer - 8701-8800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lbzbi 8701* |
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | nn01to3 8702 |
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13-Sep-2018.)
|
|
|
Theorem | nn0ge2m1nnALT 8703 |
Alternate proof of nn0ge2m1nn 8348: 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 8625, 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 8348. (Contributed by Alexander van der Vekens,
1-Aug-2018.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
|
3.4.11 Rational numbers (as a subset of complex
numbers)
|
|
Syntax | cq 8704 |
Extend class notation to include the class of rationals.
|
|
|
Definition | df-q 8705 |
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 8707
for the relation "is rational." (Contributed
by NM, 8-Jan-2002.)
|
|
|
Theorem | divfnzn 8706 |
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, 19-Mar-2020.)
|
|
|
Theorem | elq 8707* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
|
|
Theorem | qmulz 8708* |
If is rational, then
some integer multiple of it is an integer.
(Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro,
22-Jul-2014.)
|
|
|
Theorem | znq 8709 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
|
|
Theorem | qre 8710 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
|
|
Theorem | zq 8711 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
|
|
Theorem | zssq 8712 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
|
|
Theorem | nn0ssq 8713 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
|
|
Theorem | nnssq 8714 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
|
|
Theorem | qssre 8715 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
|
|
Theorem | qsscn 8716 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | qex 8717 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nnq 8718 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
|
|
Theorem | qcn 8719 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | qaddcl 8720 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
|
|
Theorem | qnegcl 8721 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
|
|
Theorem | qmulcl 8722 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
|
|
Theorem | qsubcl 8723 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
|
|
Theorem | qapne 8724 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
# |
|
Theorem | qltlen 8725 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7730 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
|
|
Theorem | qlttri2 8726 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
|
|
Theorem | qreccl 8727 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
|
|
Theorem | qdivcl 8728 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
|
|
Theorem | qrevaddcl 8729 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | nnrecq 8730 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
|
|
Theorem | irradd 8731 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
|
|
Theorem | irrmul 8732 |
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, 7-Nov-2008.)
|
|
|
3.4.12 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 8733* |
There is a natural one-to-one mapping from
to ,
where we map to . In our
construction of the complex numbers, this is in fact our
definition of
(see df-c 6987), but in the axiomatic treatment we can only
show
that there is the expected mapping between these two sets. (Contributed
by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro,
17-Feb-2014.)
|
|
|
3.5 Order sets
|
|
3.5.1 Positive reals (as a subset of complex
numbers)
|
|
Syntax | crp 8734 |
Extend class notation to include the class of positive reals.
|
|
|
Definition | df-rp 8735 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | elrp 8736 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | elrpii 8737 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
|
|
Theorem | 1rp 8738 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
|
|
Theorem | 2rp 8739 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpre 8740 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpxr 8741 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
|
|
Theorem | rpcn 8742 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
|
|
Theorem | nnrp 8743 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
|
|
Theorem | rpssre 8744 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
|
|
Theorem | rpgt0 8745 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpge0 8746 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | rpregt0 8747 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
|
|
Theorem | rprege0 8748 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
|
|
Theorem | rpne0 8749 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
|
|
Theorem | rpap0 8750 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
# |
|
Theorem | rprene0 8751 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpreap0 8752 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | rpcnne0 8753 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpcnap0 8754 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | ralrp 8755 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
|
|
Theorem | rexrp 8756 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
|
|
Theorem | rpaddcl 8757 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpmulcl 8758 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | rpdivcl 8759 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpreccl 8760 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
|
|
Theorem | rphalfcl 8761 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
|
|
Theorem | rpgecl 8762 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalflt 8763 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
|
|
Theorem | rerpdivcl 8764 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
|
|
Theorem | ge0p1rp 8765 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
|
|
Theorem | rpnegap 8766 |
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|
#
|
|
Theorem | 0nrp 8767 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
|
|
Theorem | ltsubrp 8768 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
|
|
Theorem | ltaddrp 8769 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
|
|
Theorem | difrp 8770 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
|
|
Theorem | elrpd 8771 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | nnrpd 8772 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpred 8773 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpxrd 8774 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpcnd 8775 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpgt0d 8776 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpge0d 8777 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpne0d 8778 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpap0d 8779 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
# |
|
Theorem | rpregt0d 8780 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprege0d 8781 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rprene0d 8782 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpcnne0d 8783 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpreccld 8784 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprecred 8785 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalfcld 8786 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reclt1d 8787 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | recgt1d 8788 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpaddcld 8789 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpmulcld 8790 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpdivcld 8791 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrecd 8792 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerecd 8793 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrec1d 8794 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerec2d 8795 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2ad 8796 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv2d 8797 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2d 8798 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivdivd 8799 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge1 8800 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|