Theorem List for Intuitionistic Logic Explorer - 9601-9700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mnfltpnf 9601 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnfltxr 9602 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | pnfnlt 9603 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | nltmnf 9604 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | pnfge 9605 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
|
|
Theorem | 0lepnf 9606 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | nn0pnfge0 9607 |
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 9608 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltnsym 9609 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltnsym2 9610 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
|
|
Theorem | xrlttr 9611 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltso 9612 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
|
|
Theorem | xrlttri3 9613 |
Extended real version of lttri3 7868. (Contributed by NM, 9-Feb-2006.)
|
|
|
Theorem | xrltle 9614 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltled 9615 |
'Less than' implies 'less than or equal to' for extended reals.
Deduction form of xrltle 9614. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
|
Theorem | xrleid 9616 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
|
|
Theorem | xrleidd 9617 |
'Less than or equal to' is reflexive for extended reals. Deduction form
of xrleid 9616. (Contributed by Glauco Siliprandi,
26-Jun-2021.)
|
|
|
Theorem | xrletri3 9618 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
|
|
Theorem | xrlelttr 9619 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrltletr 9620 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrletr 9621 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
|
|
Theorem | xrlttrd 9622 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrlelttrd 9623 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltletrd 9624 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrletrd 9625 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltne 9626 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
|
|
Theorem | nltpnft 9627 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
|
|
Theorem | npnflt 9628 |
An extended real is less than plus infinity iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xgepnf 9629 |
An extended real which is greater than plus infinity is plus infinity.
(Contributed by Thierry Arnoux, 18-Dec-2016.)
|
|
|
Theorem | ngtmnft 9630 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | nmnfgt 9631 |
An extended real is greater than minus infinite iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xrrebnd 9632 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | xrre 9633 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
|
|
Theorem | xrre2 9634 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
|
|
Theorem | xrre3 9635 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
|
|
Theorem | ge0gtmnf 9636 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ge0nemnf 9637 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrrege0 9638 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | z2ge 9639* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
|
|
Theorem | xnegeq 9640 |
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 9641 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.)
|
|
|
Theorem | xnegmnf 9642 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexneg 9643 |
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 9644 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xnegcl 9645 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnegneg 9646 |
Extended real version of negneg 8036. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xneg11 9647 |
Extended real version of neg11 8037. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltnegi 9648 |
Forward direction of xltneg 9649. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltneg 9649 |
Extended real version of ltneg 8248. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleneg 9650 |
Extended real version of leneg 8251. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg1 9651 |
Extended real version of lt0neg1 8254. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg2 9652 |
Extended real version of lt0neg2 8255. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xle0neg1 9653 |
Extended real version of le0neg1 8256. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xle0neg2 9654 |
Extended real version of le0neg2 8257. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xrpnfdc 9655 |
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13-Apr-2023.)
|
DECID |
|
Theorem | xrmnfdc 9656 |
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13-Apr-2023.)
|
DECID |
|
Theorem | xaddf 9657 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 21-Aug-2015.)
|
|
|
Theorem | xaddval 9658 |
Value of the extended real addition operation. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddpnf1 9659 |
Addition of positive infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddpnf2 9660 |
Addition of positive infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddmnf1 9661 |
Addition of negative infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddmnf2 9662 |
Addition of negative infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | pnfaddmnf 9663 |
Addition of positive and negative infinity. This is often taken to be a
"null" value or out of the domain, but we define it (somewhat
arbitrarily)
to be zero so that the resulting function is total, which simplifies
proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | mnfaddpnf 9664 |
Addition of negative and positive infinity. This is often taken to be a
"null" value or out of the domain, but we define it (somewhat
arbitrarily)
to be zero so that the resulting function is total, which simplifies
proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexadd 9665 |
The extended real addition operation when both arguments are real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexsub 9666 |
Extended real subtraction when both arguments are real. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | rexaddd 9667 |
The extended real addition operation when both arguments are real.
Deduction version of rexadd 9665. (Contributed by Glauco Siliprandi,
24-Dec-2020.)
|
|
|
Theorem | xnegcld 9668 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | xrex 9669 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
|
|
Theorem | xaddnemnf 9670 |
Closure of extended real addition in the subset
.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddnepnf 9671 |
Closure of extended real addition in the subset
.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xnegid 9672 |
Extended real version of negid 8033. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddcl 9673 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddcom 9674 |
The extended real addition operation is commutative. (Contributed by NM,
26-Dec-2011.)
|
|
|
Theorem | xaddid1 9675 |
Extended real version of addid1 7924. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddid2 9676 |
Extended real version of addid2 7925. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddid1d 9677 |
is a right identity for
extended real addition. (Contributed by
Glauco Siliprandi, 17-Aug-2020.)
|
|
|
Theorem | xnn0lenn0nn0 9678 |
An extended nonnegative integer which is less than or equal to a
nonnegative integer is a nonnegative integer. (Contributed by AV,
24-Nov-2021.)
|
NN0* |
|
Theorem | xnn0le2is012 9679 |
An extended nonnegative integer which is less than or equal to 2 is either
0 or 1 or 2. (Contributed by AV, 24-Nov-2021.)
|
NN0*
|
|
Theorem | xnn0xadd0 9680 |
The sum of two extended nonnegative integers is iff each of the two
extended nonnegative integers is . (Contributed by AV,
14-Dec-2020.)
|
NN0* NN0* |
|
Theorem | xnegdi 9681 |
Extended real version of negdi 8043. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddass 9682 |
Associativity of extended real addition. The correct condition here is
"it is not the case that both and appear as one of
,
i.e. ", but this
condition is difficult to work with, so we break the theorem into two
parts: this one, where is not present in , and
xaddass2 9683, where is not present. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddass2 9683 |
Associativity of extended real addition. See xaddass 9682 for notes on the
hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xpncan 9684 |
Extended real version of pncan 7992. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnpcan 9685 |
Extended real version of npcan 7995. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleadd1a 9686 |
Extended real version of leadd1 8216; note that the converse implication is
not true, unlike the real version (for example but
).
(Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleadd2a 9687 |
Commuted form of xleadd1a 9686. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleadd1 9688 |
Weakened version of xleadd1a 9686 under which the reverse implication is
true. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xltadd1 9689 |
Extended real version of ltadd1 8215. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
|
|
|
Theorem | xltadd2 9690 |
Extended real version of ltadd2 8205. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
|
|
Theorem | xaddge0 9691 |
The sum of nonnegative extended reals is nonnegative. (Contributed by
Mario Carneiro, 21-Aug-2015.)
|
|
|
Theorem | xle2add 9692 |
Extended real version of le2add 8230. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
|
|
Theorem | xlt2add 9693 |
Extended real version of lt2add 8231. Note that ltleadd 8232, which has
weaker assumptions, is not true for the extended reals (since
fails). (Contributed by Mario
Carneiro,
23-Aug-2015.)
|
|
|
Theorem | xsubge0 9694 |
Extended real version of subge0 8261. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
|
|
Theorem | xposdif 9695 |
Extended real version of posdif 8241. (Contributed by Mario Carneiro,
24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xlesubadd 9696 |
Under certain conditions, the conclusion of lesubadd 8220 is true even in the
extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
|
|
Theorem | xaddcld 9697 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | xadd4d 9698 |
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 7955. (Contributed by Alexander van der Vekens,
21-Dec-2017.)
|
|
|
Theorem | xnn0add4d 9699 |
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9698. (Contributed by AV,
12-Dec-2020.)
|
NN0* NN0* NN0* NN0* |
|
Theorem | xleaddadd 9700 |
Cancelling a factor of two in (expressed as addition rather than
as a factor to avoid extended real multiplication). (Contributed by Jim
Kingdon, 18-Apr-2023.)
|
|