Theorem List for Intuitionistic Logic Explorer - 9501-9600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | rerpdivcl 9501 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
|
|
Theorem | ge0p1rp 9502 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
|
|
Theorem | rpnegap 9503 |
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 9504 |
Elementhood of a negation in the positive real numbers. (Contributed by
Thierry Arnoux, 19-Sep-2018.)
|
|
|
Theorem | negelrpd 9505 |
The negation of a negative number is in the positive real numbers.
(Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
|
|
Theorem | 0nrp 9506 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
|
|
Theorem | ltsubrp 9507 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
|
|
Theorem | ltaddrp 9508 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
|
|
Theorem | difrp 9509 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
|
|
Theorem | elrpd 9510 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | nnrpd 9511 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zgt1rpn0n1 9512 |
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 9513 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpxrd 9514 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpcnd 9515 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpgt0d 9516 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpge0d 9517 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpne0d 9518 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | rpap0d 9519 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
# |
|
Theorem | rpregt0d 9520 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprege0d 9521 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rprene0d 9522 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpcnne0d 9523 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpreccld 9524 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rprecred 9525 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rphalfcld 9526 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | reclt1d 9527 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | recgt1d 9528 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpaddcld 9529 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpmulcld 9530 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | rpdivcld 9531 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrecd 9532 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerecd 9533 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltrec1d 9534 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | lerec2d 9535 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2ad 9536 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv2d 9537 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv2d 9538 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivdivd 9539 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge1 9540 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
|
|
Theorem | divlt1lt 9541 |
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 9542 |
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 9543 |
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 9544 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rerpdivcld 9545 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltsubrpd 9546 |
Subtracting a positive real from another number decreases it.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrpd 9547 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltaddrp2d 9548 |
Adding a positive number to another number increases it. (Contributed
by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt11d 9549 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmulgt12d 9550 |
Multiplication by a number greater than 1. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | gt0divd 9551 |
Division of a positive number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ge0divd 9552 |
Division of a nonnegative number by a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | rpgecld 9553 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | divge0d 9554 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1d 9555 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul2d 9556 |
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 9557 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemul2d 9558 |
Multiplication of both sides of 'less than or equal to' by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv1d 9559 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv1d 9560 |
Division of both sides of a less than or equal to relation by a positive
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmuldivd 9561 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmuldiv2d 9562 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lemuldivd 9563 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lemuldiv2d 9564 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltdivmuld 9565 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdivmul2d 9566 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmuld 9567 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmul2d 9568 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1dd 9569 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltmul2dd 9570 |
Multiplication of both sides of 'less than' by a positive number.
Theorem I.19 of [Apostol] p. 20.
(Contributed by Mario Carneiro,
30-May-2016.)
|
|
|
Theorem | ltdiv1dd 9571 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv1dd 9572 |
Division of both sides of a less than or equal to relation by a
positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv12ad 9573 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv23d 9574 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv23d 9575 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | mul2lt0rlt0 9576 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
|
|
Theorem | mul2lt0rgt0 9577 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
|
|
Theorem | mul2lt0llt0 9578 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
|
|
Theorem | mul2lt0lgt0 9579 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
2-Oct-2018.)
|
|
|
Theorem | mul2lt0np 9580 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
|
|
Theorem | mul2lt0pn 9581 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
|
|
Theorem | lt2mul2divd 9582 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | nnledivrp 9583 |
Division of a positive integer by a positive number is less than or equal
to the integer iff the number is greater than or equal to 1. (Contributed
by AV, 19-Jun-2021.)
|
|
|
Theorem | nn0ledivnn 9584 |
Division of a nonnegative integer by a positive integer is less than or
equal to the integer. (Contributed by AV, 19-Jun-2021.)
|
|
|
Theorem | addlelt 9585 |
If the sum of a real number and a positive real number is less than or
equal to a third real number, the first real number is less than the third
real number. (Contributed by AV, 1-Jul-2021.)
|
|
|
4.5.2 Infinity and the extended real number
system (cont.)
|
|
Syntax | cxne 9586 |
Extend class notation to include the negative of an extended real.
|
|
|
Syntax | cxad 9587 |
Extend class notation to include addition of extended reals.
|
|
|
Syntax | cxmu 9588 |
Extend class notation to include multiplication of extended reals.
|
|
|
Definition | df-xneg 9589 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
|
|
Definition | df-xadd 9590* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Definition | df-xmul 9591* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ltxr 9592 |
The 'less than' binary relation on the set of extended reals.
Definition 12-3.1 of [Gleason] p. 173.
(Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | elxr 9593 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | xrnemnf 9594 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrnepnf 9595 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrltnr 9596 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | ltpnf 9597 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | 0ltpnf 9598 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnflt 9599 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnflt0 9600 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|