P. 101 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10001-10100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nltmnf 10001	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
|- ( A e. RR* -> -. A < -oo )
Theorem	pnfge 10002	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
|- ( A e. RR* -> A <_ +oo )
Theorem	0lepnf 10003	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 <_ +oo
Theorem	nn0pnfge0 10004	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.)
|- ( ( N e. NN0 \/ N = +oo ) -> 0 <_ N )
Theorem	mnfle 10005	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
|- ( A e. RR* -> -oo <_ A )
Theorem	xrltnsym 10006	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> -. B < A ) )
Theorem	xrltnsym2 10007	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
|- ( ( A e. RR* /\ B e. RR* ) -> -. ( A < B /\ B < A ) )
Theorem	xrlttr 10008	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	xrltso 10009	'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
|- < Or RR*
Theorem	xrlttri3 10010	Extended real version of lttri3 8242. (Contributed by NM, 9-Feb-2006.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	xrltle 10011	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> A <_ B ) )
Theorem	xrltled 10012	'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 10011. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A <_ B )
Theorem	xrleid 10013	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
|- ( A e. RR* -> A <_ A )
Theorem	xrleidd 10014	'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 10013. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> A <_ A )
Theorem	xnn0dcle 10015	Decidability of <_ for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> DECID A <_ B )
Theorem	xnn0letri 10016	Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( A <_ B \/ B <_ A ) )
Theorem	xrletri3 10017	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	xrletrid 10018	Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ A )   =>    |- ( ph -> A = B )
Theorem	xrlelttr 10019	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
Theorem	xrltletr 10020	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
Theorem	xrletr 10021	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
Theorem	xrlttrd 10022	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	xrlelttrd 10023	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	xrltletrd 10024	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A < C )
Theorem	xrletrd 10025	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A <_ C )
Theorem	xrltne 10026	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B =/= A )
Theorem	nltpnft 10027	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
|- ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
Theorem	npnflt 10028	An extended real is less than plus infinity iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
|- ( A e. RR* -> ( A < +oo <-> A =/= +oo ) )
Theorem	xgepnf 10029	An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
|- ( A e. RR* -> ( +oo <_ A <-> A = +oo ) )
Theorem	ngtmnft 10030	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
Theorem	nmnfgt 10031	An extended real is greater than minus infinite iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
|- ( A e. RR* -> ( -oo < A <-> A =/= -oo ) )
Theorem	xrrebnd 10032	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
|- ( A e. RR* -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )
Theorem	xrre 10033	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> A e. RR )
Theorem	xrre2 10034	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR )
Theorem	xrre3 10035	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( B <_ A /\ A < +oo ) ) -> A e. RR )
Theorem	ge0gtmnf 10036	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ 0 <_ A ) -> -oo < A )
Theorem	ge0nemnf 10037	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )
Theorem	xrrege0 10038	A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> A e. RR )
Theorem	z2ge 10039*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> E. k e. ZZ ( M <_ k /\ N <_ k ) )
Theorem	xnegeq 10040	Equality of two extended numbers with -e in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|- ( A = B -> -e A = -e B )
Theorem	xnegpnf 10041	Minus +oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
|- -e +oo = -oo
Theorem	xnegmnf 10042	Minus -oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|- -e -oo = +oo
Theorem	rexneg 10043	Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR -> -e A = -u A )
Theorem	xneg0 10044	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- -e 0 = 0
Theorem	xnegcl 10045	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> -e A e. RR* )
Theorem	xnegneg 10046	Extended real version of negneg 8412. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> -e -e A = A )
Theorem	xneg11 10047	Extended real version of neg11 8413. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( -e A = -e B <-> A = B ) )
Theorem	xltnegi 10048	Forward direction of xltneg 10049. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> -e B < -e A )
Theorem	xltneg 10049	Extended real version of ltneg 8625. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -e B < -e A ) )
Theorem	xleneg 10050	Extended real version of leneg 8628. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -e B <_ -e A ) )
Theorem	xlt0neg1 10051	Extended real version of lt0neg1 8631. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( A < 0 <-> 0 < -e A ) )
Theorem	xlt0neg2 10052	Extended real version of lt0neg2 8632. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( 0 < A <-> -e A < 0 ) )
Theorem	xle0neg1 10053	Extended real version of le0neg1 8633. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( A e. RR* -> ( A <_ 0 <-> 0 <_ -e A ) )
Theorem	xle0neg2 10054	Extended real version of le0neg2 8634. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( A e. RR* -> ( 0 <_ A <-> -e A <_ 0 ) )
Theorem	xrpnfdc 10055	An extended real is or is not plus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.)
|- ( A e. RR* -> DECID A = +oo )
Theorem	xrmnfdc 10056	An extended real is or is not minus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.)
|- ( A e. RR* -> DECID A = -oo )
Theorem	xaddf 10057	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- +e : ( RR* X. RR* ) --> RR*
Theorem	xaddval 10058	Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = if ( A = +oo , if ( B = -oo , 0 , +oo ) , if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) ) )
Theorem	xaddpnf1 10059	Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
Theorem	xaddpnf2 10060	Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= -oo ) -> ( +oo +e A ) = +oo )
Theorem	xaddmnf1 10061	Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
Theorem	xaddmnf2 10062	Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= +oo ) -> ( -oo +e A ) = -oo )
Theorem	pnfaddmnf 10063	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.)
|- ( +oo +e -oo ) = 0
Theorem	mnfaddpnf 10064	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.)
|- ( -oo +e +oo ) = 0
Theorem	rexadd 10065	The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )
Theorem	rexsub 10066	Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A +e -e B ) = ( A - B ) )
Theorem	rexaddd 10067	The extended real addition operation when both arguments are real. Deduction version of rexadd 10065. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A +e B ) = ( A + B ) )
Theorem	xnegcld 10068	Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> -e A e. RR* )
Theorem	xrex 10069	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|- RR* e. _V
Theorem	xaddnemnf 10070	Closure of extended real addition in the subset RR* / { -oo }. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )
Theorem	xaddnepnf 10071	Closure of extended real addition in the subset RR* / { +oo }. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= +oo ) /\ ( B e. RR* /\ B =/= +oo ) ) -> ( A +e B ) =/= +oo )
Theorem	xnegid 10072	Extended real version of negid 8409. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( A +e -e A ) = 0 )
Theorem	xaddcl 10073	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )
Theorem	xaddcom 10074	The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )
Theorem	xaddid1 10075	Extended real version of addrid 8300. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( A +e 0 ) = A )
Theorem	xaddid2 10076	Extended real version of addlid 8301. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( 0 +e A ) = A )
Theorem	xaddid1d 10077	0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> ( A +e 0 ) = A )
Theorem	xnn0lenn0nn0 10078	An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021.)
|- ( ( M e. NN0* /\ N e. NN0 /\ M <_ N ) -> M e. NN0 )
Theorem	xnn0le2is012 10079	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.)
|- ( ( N e. NN0* /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
Theorem	xnn0xadd0 10080	The sum of two extended nonnegative integers is 0 iff each of the two extended nonnegative integers is 0. (Contributed by AV, 14-Dec-2020.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( ( A +e B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
Theorem	xnegdi 10081	Extended real version of negdi 8419. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> -e ( A +e B ) = ( -e A +e -e B ) )
Theorem	xaddass 10082	Associativity of extended real addition. The correct condition here is "it is not the case that both +oo and -oo appear as one of A , B , C, i.e. -. { +oo , -oo } C_ { A , B , C }", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -oo is not present in A , B , C, and xaddass2 10083, where +oo is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )
Theorem	xaddass2 10083	Associativity of extended real addition. See xaddass 10082 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= +oo ) /\ ( B e. RR* /\ B =/= +oo ) /\ ( C e. RR* /\ C =/= +oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )
Theorem	xpncan 10084	Extended real version of pncan 8368. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e B ) +e -e B ) = A )
Theorem	xnpcan 10085	Extended real version of npcan 8371. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A )
Theorem	xleadd1a 10086	Extended real version of leadd1 8593; note that the converse implication is not true, unlike the real version (for example 0 < 1 but ( 1 +e +oo ) <_ ( 0 +e +oo )). (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) <_ ( B +e C ) )
Theorem	xleadd2a 10087	Commuted form of xleadd1a 10086. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( C +e A ) <_ ( C +e B ) )
Theorem	xleadd1 10088	Weakened version of xleadd1a 10086 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A <_ B <-> ( A +e C ) <_ ( B +e C ) ) )
Theorem	xltadd1 10089	Extended real version of ltadd1 8592. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A < B <-> ( A +e C ) < ( B +e C ) ) )
Theorem	xltadd2 10090	Extended real version of ltadd2 8582. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A < B <-> ( C +e A ) < ( C +e B ) ) )
Theorem	xaddge0 10091	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A +e B ) )
Theorem	xle2add 10092	Extended real version of le2add 8607. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A <_ C /\ B <_ D ) -> ( A +e B ) <_ ( C +e D ) ) )
Theorem	xlt2add 10093	Extended real version of lt2add 8608. Note that ltleadd 8609, which has weaker assumptions, is not true for the extended reals (since 0 + +oo < 1 + +oo fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A < C /\ B < D ) -> ( A +e B ) < ( C +e D ) ) )
Theorem	xsubge0 10094	Extended real version of subge0 8638. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
Theorem	xposdif 10095	Extended real version of posdif 8618. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
Theorem	xlesubadd 10096	Under certain conditions, the conclusion of lesubadd 8597 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) )
Theorem	xaddcld 10097	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A +e B ) e. RR* )
Theorem	xadd4d 10098	Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 8331. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
|- ( ph -> ( A e. RR* /\ A =/= -oo ) )   &    |- ( ph -> ( B e. RR* /\ B =/= -oo ) )   &    |- ( ph -> ( C e. RR* /\ C =/= -oo ) )   &    |- ( ph -> ( D e. RR* /\ D =/= -oo ) )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xnn0add4d 10099	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 10098. (Contributed by AV, 12-Dec-2020.)
|- ( ph -> A e. NN0* )   &    |- ( ph -> B e. NN0* )   &    |- ( ph -> C e. NN0* )   &    |- ( ph -> D e. NN0* )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xleaddadd 10100	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.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A +e A ) <_ ( B +e B ) ) )