Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elnn1uz2 9401 |
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17-Nov-2012.)
|
|
|
Theorem | uz2mulcl 9402 |
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26-Oct-2012.)
|
|
|
Theorem | indstr2 9403* |
Strong Mathematical Induction for positive integers (inference schema).
The first two hypotheses give us the substitution instances we need; the
last two are the basis and the induction step. (Contributed by Paul
Chapman, 21-Nov-2012.)
|
|
|
Theorem | eluzdc 9404 |
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18-Apr-2020.)
|
DECID
|
|
Theorem | ublbneg 9405* |
The image under negation of a bounded-above set of reals is bounded
below. For a theorem which is similar but also adds that the bounds
need to be the tightest possible, see supinfneg 9390. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | eqreznegel 9406* |
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | negm 9407* |
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10-Apr-2020.)
|
|
|
Theorem | lbzbi 9408* |
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | nn01to3 9409 |
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13-Sep-2018.)
|
|
|
Theorem | nn0ge2m1nnALT 9410 |
Alternate proof of nn0ge2m1nn 9037: 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 9332, 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 9037. (Contributed by Alexander van der Vekens,
1-Aug-2018.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
|
4.4.12 Rational numbers (as a subset of complex
numbers)
|
|
Syntax | cq 9411 |
Extend class notation to include the class of rationals.
|
|
|
Definition | df-q 9412 |
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 9414
for the relation "is rational." (Contributed
by NM, 8-Jan-2002.)
|
|
|
Theorem | divfnzn 9413 |
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 9414* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
|
|
Theorem | qmulz 9415* |
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 9416 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
|
|
Theorem | qre 9417 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
|
|
Theorem | zq 9418 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
|
|
Theorem | zssq 9419 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
|
|
Theorem | nn0ssq 9420 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
|
|
Theorem | nnssq 9421 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
|
|
Theorem | qssre 9422 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
|
|
Theorem | qsscn 9423 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | qex 9424 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | nnq 9425 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
|
|
Theorem | qcn 9426 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | qaddcl 9427 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
|
|
Theorem | qnegcl 9428 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
|
|
Theorem | qmulcl 9429 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
|
|
Theorem | qsubcl 9430 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
|
|
Theorem | qapne 9431 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
# |
|
Theorem | qltlen 9432 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8394 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
|
|
Theorem | qlttri2 9433 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
|
|
Theorem | qreccl 9434 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
|
|
Theorem | qdivcl 9435 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
|
|
Theorem | qrevaddcl 9436 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
|
|
Theorem | nnrecq 9437 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
|
|
Theorem | irradd 9438 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
|
|
Theorem | irrmul 9439 |
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.)
|
|
|
4.4.13 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 9440* |
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 7626), 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 9441 |
Extend class notation to include the class of positive reals.
|
|
|
Definition | df-rp 9442 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | elrp 9443 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | elrpii 9444 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
|
|
Theorem | 1rp 9445 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
|
|
Theorem | 2rp 9446 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | 3rp 9447 |
3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | rpre 9448 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpxr 9449 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
|
|
Theorem | rpcn 9450 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|
|
|
Theorem | nnrp 9451 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
|
|
Theorem | rpssre 9452 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
|
|
Theorem | rpgt0 9453 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpge0 9454 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|
|
|
Theorem | rpregt0 9455 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
|
|
Theorem | rprege0 9456 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
|
|
Theorem | rpne0 9457 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
|
|
Theorem | rpap0 9458 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
# |
|
Theorem | rprene0 9459 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpreap0 9460 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | rpcnne0 9461 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
|
|
Theorem | rpcnap0 9462 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
# |
|
Theorem | ralrp 9463 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
|
|
Theorem | rexrp 9464 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
|
|
Theorem | rpaddcl 9465 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
|
|
Theorem | rpmulcl 9466 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
|
|
Theorem | rpdivcl 9467 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
|
|
Theorem | rpreccl 9468 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
|
|
Theorem | rphalfcl 9469 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
|
|
Theorem | rpgecl 9470 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalflt 9471 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
|
|
Theorem | rerpdivcl 9472 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
|
|
Theorem | ge0p1rp 9473 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
|
|
Theorem | rpnegap 9474 |
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 9475 |
Elementhood of a negation in the positive real numbers. (Contributed by
Thierry Arnoux, 19-Sep-2018.)
|
|
|
Theorem | negelrpd 9476 |
The negation of a negative number is in the positive real numbers.
(Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
|
|
Theorem | 0nrp 9477 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
|
|
Theorem | ltsubrp 9478 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
|
|
Theorem | ltaddrp 9479 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
|
|
Theorem | difrp 9480 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
|
|
Theorem | elrpd 9481 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | nnrpd 9482 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpred 9483 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpxrd 9484 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpcnd 9485 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpgt0d 9486 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpge0d 9487 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpne0d 9488 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpap0d 9489 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
# |
|
Theorem | rpregt0d 9490 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprege0d 9491 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rprene0d 9492 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpcnne0d 9493 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpreccld 9494 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprecred 9495 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalfcld 9496 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reclt1d 9497 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | recgt1d 9498 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpaddcld 9499 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpmulcld 9500 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|