Theorem List for Intuitionistic Logic Explorer - 9501-9600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lemuldivd 9501 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lemuldiv2d 9502 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltdivmuld 9503 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdivmul2d 9504 |
'Less than' relationship between division and multiplication.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmuld 9505 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ledivmul2d 9506 |
'Less than or equal to' relationship between division and
multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | ltmul1dd 9507 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | ltmul2dd 9508 |
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 9509 |
Division of both sides of 'less than' by a positive number.
(Contributed by Mario Carneiro, 30-May-2016.)
|
|
|
Theorem | lediv1dd 9510 |
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 9511 |
Comparison of ratio of two nonnegative numbers. (Contributed by Mario
Carneiro, 28-May-2016.)
|
|
|
Theorem | ltdiv23d 9512 |
Swap denominator with other side of 'less than'. (Contributed by
Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | lediv23d 9513 |
Swap denominator with other side of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | mul2lt0rlt0 9514 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
|
|
Theorem | mul2lt0rgt0 9515 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
|
|
Theorem | mul2lt0llt0 9516 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
19-Sep-2018.)
|
|
|
Theorem | mul2lt0lgt0 9517 |
If the result of a multiplication is strictly negative, then
multiplicands are of different signs. (Contributed by Thierry Arnoux,
2-Oct-2018.)
|
|
|
Theorem | mul2lt0np 9518 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
|
|
Theorem | mul2lt0pn 9519 |
The product of multiplicands of different signs is negative.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
|
|
Theorem | lt2mul2divd 9520 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | nnledivrp 9521 |
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 9522 |
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 9523 |
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 9524 |
Extend class notation to include the negative of an extended real.
|
|
|
Syntax | cxad 9525 |
Extend class notation to include addition of extended reals.
|
|
|
Syntax | cxmu 9526 |
Extend class notation to include multiplication of extended reals.
|
|
|
Definition | df-xneg 9527 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
|
|
Definition | df-xadd 9528* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Definition | df-xmul 9529* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ltxr 9530 |
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 9531 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | xrnemnf 9532 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrnepnf 9533 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrltnr 9534 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | ltpnf 9535 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | 0ltpnf 9536 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnflt 9537 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnflt0 9538 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnfltpnf 9539 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnfltxr 9540 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | pnfnlt 9541 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | nltmnf 9542 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | pnfge 9543 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
|
|
Theorem | 0lepnf 9544 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | nn0pnfge0 9545 |
If a number is a nonnegative integer or positive infinity, it is greater
than or equal to 0. (Contributed by Alexander van der Vekens,
6-Jan-2018.)
|
|
|
Theorem | mnfle 9546 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltnsym 9547 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltnsym2 9548 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
|
|
Theorem | xrlttr 9549 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltso 9550 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
|
|
Theorem | xrlttri3 9551 |
Extended real version of lttri3 7812. (Contributed by NM, 9-Feb-2006.)
|
|
|
Theorem | xrltle 9552 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltled 9553 |
'Less than' implies 'less than or equal to' for extended reals.
Deduction form of xrltle 9552. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
|
Theorem | xrleid 9554 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
|
|
Theorem | xrleidd 9555 |
'Less than or equal to' is reflexive for extended reals. Deduction form
of xrleid 9554. (Contributed by Glauco Siliprandi,
26-Jun-2021.)
|
|
|
Theorem | xrletri3 9556 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
|
|
Theorem | xrlelttr 9557 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrltletr 9558 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrletr 9559 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
|
|
Theorem | xrlttrd 9560 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrlelttrd 9561 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltletrd 9562 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrletrd 9563 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltne 9564 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
|
|
Theorem | nltpnft 9565 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
|
|
Theorem | npnflt 9566 |
An extended real is less than plus infinity iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xgepnf 9567 |
An extended real which is greater than plus infinity is plus infinity.
(Contributed by Thierry Arnoux, 18-Dec-2016.)
|
|
|
Theorem | ngtmnft 9568 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | nmnfgt 9569 |
An extended real is greater than minus infinite iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xrrebnd 9570 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | xrre 9571 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
|
|
Theorem | xrre2 9572 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
|
|
Theorem | xrre3 9573 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
|
|
Theorem | ge0gtmnf 9574 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ge0nemnf 9575 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrrege0 9576 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | z2ge 9577* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
|
|
Theorem | xnegeq 9578 |
Equality of two extended numbers with in front of them.
(Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnegpnf 9579 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.)
|
|
|
Theorem | xnegmnf 9580 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexneg 9581 |
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xneg0 9582 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xnegcl 9583 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnegneg 9584 |
Extended real version of negneg 7980. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xneg11 9585 |
Extended real version of neg11 7981. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltnegi 9586 |
Forward direction of xltneg 9587. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltneg 9587 |
Extended real version of ltneg 8192. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleneg 9588 |
Extended real version of leneg 8195. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg1 9589 |
Extended real version of lt0neg1 8198. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg2 9590 |
Extended real version of lt0neg2 8199. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xle0neg1 9591 |
Extended real version of le0neg1 8200. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xle0neg2 9592 |
Extended real version of le0neg2 8201. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xrpnfdc 9593 |
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13-Apr-2023.)
|
DECID |
|
Theorem | xrmnfdc 9594 |
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13-Apr-2023.)
|
DECID |
|
Theorem | xaddf 9595 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 21-Aug-2015.)
|
|
|
Theorem | xaddval 9596 |
Value of the extended real addition operation. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddpnf1 9597 |
Addition of positive infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddpnf2 9598 |
Addition of positive infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddmnf1 9599 |
Addition of negative infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddmnf2 9600 |
Addition of negative infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|