Theorem List for Intuitionistic Logic Explorer - 9601-9700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | qreccl 9601 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
|
|
Theorem | qdivcl 9602 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
|
|
Theorem | qrevaddcl 9603 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | nnrecq 9604 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
|
|
Theorem | irradd 9605 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
|
|
Theorem | irrmul 9606 |
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.)
|
|
|
Theorem | elpq 9607* |
A positive rational is the quotient of two positive integers.
(Contributed by AV, 29-Dec-2022.)
|
|
|
Theorem | elpqb 9608* |
A class is a positive rational iff it is the quotient of two positive
integers. (Contributed by AV, 30-Dec-2022.)
|
|
|
4.4.13 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 9609* |
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 7780), 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.)
|
|
|
4.5 Order sets
|
|
4.5.1 Positive reals (as a subset of complex
numbers)
|
|
Syntax | crp 9610 |
Extend class notation to include the class of positive reals.
|
|
|
Definition | df-rp 9611 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | elrp 9612 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | elrpii 9613 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
|
|
Theorem | 1rp 9614 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
|
|
Theorem | 2rp 9615 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | 3rp 9616 |
3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | rpre 9617 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpxr 9618 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
|
|
Theorem | rpcn 9619 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
|
|
Theorem | nnrp 9620 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
|
|
Theorem | rpssre 9621 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
|
|
Theorem | rpgt0 9622 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpge0 9623 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | rpregt0 9624 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
|
|
Theorem | rprege0 9625 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
|
|
Theorem | rpne0 9626 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
|
|
Theorem | rpap0 9627 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
# |
|
Theorem | rprene0 9628 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpreap0 9629 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | rpcnne0 9630 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpcnap0 9631 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | ralrp 9632 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
|
|
Theorem | rexrp 9633 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
|
|
Theorem | rpaddcl 9634 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpmulcl 9635 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | rpdivcl 9636 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpreccl 9637 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
|
|
Theorem | rphalfcl 9638 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
|
|
Theorem | rpgecl 9639 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalflt 9640 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
|
|
Theorem | rerpdivcl 9641 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
|
|
Theorem | ge0p1rp 9642 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
|
|
Theorem | rpnegap 9643 |
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|
#
|
|
Theorem | negelrp 9644 |
Elementhood of a negation in the positive real numbers. (Contributed by
Thierry Arnoux, 19-Sep-2018.)
|
|
|
Theorem | negelrpd 9645 |
The negation of a negative number is in the positive real numbers.
(Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
|
|
Theorem | 0nrp 9646 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
|
|
Theorem | ltsubrp 9647 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
|
|
Theorem | ltaddrp 9648 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
|
|
Theorem | difrp 9649 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
|
|
Theorem | elrpd 9650 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | nnrpd 9651 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zgt1rpn0n1 9652 |
An integer greater than 1 is a positive real number not equal to 0 or 1.
Useful for working with integer logarithm bases (which is a common case,
e.g., base 2, base 3, or base 10). (Contributed by Thierry Arnoux,
26-Sep-2017.) (Proof shortened by AV, 9-Jul-2022.)
|
|
|
Theorem | rpred 9653 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpxrd 9654 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpcnd 9655 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpgt0d 9656 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpge0d 9657 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpne0d 9658 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpap0d 9659 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
# |
|
Theorem | rpregt0d 9660 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprege0d 9661 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rprene0d 9662 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpcnne0d 9663 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpreccld 9664 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprecred 9665 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalfcld 9666 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reclt1d 9667 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | recgt1d 9668 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpaddcld 9669 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpmulcld 9670 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpdivcld 9671 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrecd 9672 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerecd 9673 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrec1d 9674 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerec2d 9675 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2ad 9676 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv2d 9677 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2d 9678 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivdivd 9679 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge1 9680 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | divlt1lt 9681 |
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,
25-May-2020.)
|
|
|
Theorem | divle1le 9682 |
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, 29-Jun-2021.)
|
|
|
Theorem | ledivge1le 9683 |
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, 29-Jun-2021.)
|
|
|
Theorem | ge0p1rpd 9684 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rerpdivcld 9685 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltsubrpd 9686 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrpd 9687 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrp2d 9688 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt11d 9689 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt12d 9690 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | gt0divd 9691 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ge0divd 9692 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpgecld 9693 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge0d 9694 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1d 9695 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul2d 9696 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | lemul1d 9697 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul2d 9698 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv1d 9699 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv1d 9700 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|