Theorem List for Intuitionistic Logic Explorer - 9701-9800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lt2mul2divd 9701 |
The ratio of nonnegative and positive numbers is nonnegative.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | nnledivrp 9702 |
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 9703 |
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 9704 |
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 9705 |
Extend class notation to include the negative of an extended real.
|
|
|
Syntax | cxad 9706 |
Extend class notation to include addition of extended reals.
|
|
|
Syntax | cxmu 9707 |
Extend class notation to include multiplication of extended reals.
|
|
|
Definition | df-xneg 9708 |
Define the negative of an extended real number. (Contributed by FL,
26-Dec-2011.)
|
|
|
Definition | df-xadd 9709* |
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Definition | df-xmul 9710* |
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ltxr 9711 |
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 9712 |
Membership in the set of extended reals. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | xrnemnf 9713 |
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrnepnf 9714 |
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrltnr 9715 |
The extended real 'less than' is irreflexive. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | ltpnf 9716 |
Any (finite) real is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | ltpnfd 9717 |
Any (finite) real is less than plus infinity. (Contributed by Glauco
Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | 0ltpnf 9718 |
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnflt 9719 |
Minus infinity is less than any (finite) real. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnflt0 9720 |
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | mnfltpnf 9721 |
Minus infinity is less than plus infinity. (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mnfltxr 9722 |
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | pnfnlt 9723 |
No extended real is greater than plus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | nltmnf 9724 |
No extended real is less than minus infinity. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | pnfge 9725 |
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30-Jan-2006.)
|
|
|
Theorem | 0lepnf 9726 |
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8-Dec-2018.)
|
|
|
Theorem | nn0pnfge0 9727 |
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 9728 |
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltnsym 9729 |
Ordering on the extended reals is not symmetric. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltnsym2 9730 |
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6-Feb-2007.)
|
|
|
Theorem | xrlttr 9731 |
Ordering on the extended reals is transitive. (Contributed by NM,
15-Oct-2005.)
|
|
|
Theorem | xrltso 9732 |
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15-Oct-2005.)
|
|
|
Theorem | xrlttri3 9733 |
Extended real version of lttri3 7978. (Contributed by NM, 9-Feb-2006.)
|
|
|
Theorem | xrltle 9734 |
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19-Jan-2006.)
|
|
|
Theorem | xrltled 9735 |
'Less than' implies 'less than or equal to' for extended reals.
Deduction form of xrltle 9734. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
|
Theorem | xrleid 9736 |
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7-Feb-2007.)
|
|
|
Theorem | xrleidd 9737 |
'Less than or equal to' is reflexive for extended reals. Deduction form
of xrleid 9736. (Contributed by Glauco Siliprandi,
26-Jun-2021.)
|
|
|
Theorem | xnn0dcle 9738 |
Decidability of for extended nonnegative integers. (Contributed by
Jim Kingdon, 13-Oct-2024.)
|
NN0* NN0* DECID |
|
Theorem | xnn0letri 9739 |
Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon,
13-Oct-2024.)
|
NN0* NN0*
|
|
Theorem | xrletri3 9740 |
Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|
|
|
Theorem | xrletrid 9741 |
Trichotomy law for extended reals. (Contributed by Glauco Siliprandi,
17-Aug-2020.)
|
|
|
Theorem | xrlelttr 9742 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrltletr 9743 |
Transitive law for ordering on extended reals. (Contributed by NM,
19-Jan-2006.)
|
|
|
Theorem | xrletr 9744 |
Transitive law for ordering on extended reals. (Contributed by NM,
9-Feb-2006.)
|
|
|
Theorem | xrlttrd 9745 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrlelttrd 9746 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltletrd 9747 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrletrd 9748 |
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xrltne 9749 |
'Less than' implies not equal for extended reals. (Contributed by NM,
20-Jan-2006.)
|
|
|
Theorem | nltpnft 9750 |
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30-Jan-2006.)
|
|
|
Theorem | npnflt 9751 |
An extended real is less than plus infinity iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xgepnf 9752 |
An extended real which is greater than plus infinity is plus infinity.
(Contributed by Thierry Arnoux, 18-Dec-2016.)
|
|
|
Theorem | ngtmnft 9753 |
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | nmnfgt 9754 |
An extended real is greater than minus infinite iff they are not equal.
(Contributed by Jim Kingdon, 17-Apr-2023.)
|
|
|
Theorem | xrrebnd 9755 |
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2-Feb-2006.)
|
|
|
Theorem | xrre 9756 |
A way of proving that an extended real is real. (Contributed by NM,
9-Mar-2006.)
|
|
|
Theorem | xrre2 9757 |
An extended real between two others is real. (Contributed by NM,
6-Feb-2007.)
|
|
|
Theorem | xrre3 9758 |
A way of proving that an extended real is real. (Contributed by FL,
29-May-2014.)
|
|
|
Theorem | ge0gtmnf 9759 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ge0nemnf 9760 |
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xrrege0 9761 |
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | z2ge 9762* |
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28-Aug-2005.)
|
|
|
Theorem | xnegeq 9763 |
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 9764 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.)
|
|
|
Theorem | xnegmnf 9765 |
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexneg 9766 |
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 9767 |
The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xnegcl 9768 |
Closure of extended real negative. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xnegneg 9769 |
Extended real version of negneg 8148. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xneg11 9770 |
Extended real version of neg11 8149. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltnegi 9771 |
Forward direction of xltneg 9772. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltneg 9772 |
Extended real version of ltneg 8360. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleneg 9773 |
Extended real version of leneg 8363. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg1 9774 |
Extended real version of lt0neg1 8366. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg2 9775 |
Extended real version of lt0neg2 8367. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xle0neg1 9776 |
Extended real version of le0neg1 8368. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xle0neg2 9777 |
Extended real version of le0neg2 8369. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xrpnfdc 9778 |
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13-Apr-2023.)
|
DECID |
|
Theorem | xrmnfdc 9779 |
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13-Apr-2023.)
|
DECID |
|
Theorem | xaddf 9780 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 21-Aug-2015.)
|
|
|
Theorem | xaddval 9781 |
Value of the extended real addition operation. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddpnf1 9782 |
Addition of positive infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddpnf2 9783 |
Addition of positive infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddmnf1 9784 |
Addition of negative infinity on the right. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddmnf2 9785 |
Addition of negative infinity on the left. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | pnfaddmnf 9786 |
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 9787 |
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 9788 |
The extended real addition operation when both arguments are real.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | rexsub 9789 |
Extended real subtraction when both arguments are real. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | rexaddd 9790 |
The extended real addition operation when both arguments are real.
Deduction version of rexadd 9788. (Contributed by Glauco Siliprandi,
24-Dec-2020.)
|
|
|
Theorem | xnegcld 9791 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | xrex 9792 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
|
|
Theorem | xaddnemnf 9793 |
Closure of extended real addition in the subset
.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddnepnf 9794 |
Closure of extended real addition in the subset
.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xnegid 9795 |
Extended real version of negid 8145. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddcl 9796 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xaddcom 9797 |
The extended real addition operation is commutative. (Contributed by NM,
26-Dec-2011.)
|
|
|
Theorem | xaddid1 9798 |
Extended real version of addid1 8036. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddid2 9799 |
Extended real version of addid2 8037. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xaddid1d 9800 |
is a right identity for
extended real addition. (Contributed by
Glauco Siliprandi, 17-Aug-2020.)
|
|