Type  Label  Description 
Statement 

Definition  dfxadd 9401* 
Define addition over extended real numbers. (Contributed by Mario
Carneiro, 20Aug2015.)



Definition  dfxmul 9402* 
Define multiplication over extended real numbers. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  ltxr 9403 
The 'less than' binary relation on the set of extended reals.
Definition 123.1 of [Gleason] p. 173.
(Contributed by NM,
14Oct2005.)



Theorem  elxr 9404 
Membership in the set of extended reals. (Contributed by NM,
14Oct2005.)



Theorem  xrnemnf 9405 
An extended real other than minus infinity is real or positive infinite.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xrnepnf 9406 
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xrltnr 9407 
The extended real 'less than' is irreflexive. (Contributed by NM,
14Oct2005.)



Theorem  ltpnf 9408 
Any (finite) real is less than plus infinity. (Contributed by NM,
14Oct2005.)



Theorem  0ltpnf 9409 
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  mnflt 9410 
Minus infinity is less than any (finite) real. (Contributed by NM,
14Oct2005.)



Theorem  mnflt0 9411 
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  mnfltpnf 9412 
Minus infinity is less than plus infinity. (Contributed by NM,
14Oct2005.)



Theorem  mnfltxr 9413 
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2Feb2006.)



Theorem  pnfnlt 9414 
No extended real is greater than plus infinity. (Contributed by NM,
15Oct2005.)



Theorem  nltmnf 9415 
No extended real is less than minus infinity. (Contributed by NM,
15Oct2005.)



Theorem  pnfge 9416 
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30Jan2006.)



Theorem  0lepnf 9417 
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  nn0pnfge0 9418 
If a number is a nonnegative integer or positive infinity, it is greater
than or equal to 0. (Contributed by Alexander van der Vekens,
6Jan2018.)



Theorem  mnfle 9419 
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19Jan2006.)



Theorem  xrltnsym 9420 
Ordering on the extended reals is not symmetric. (Contributed by NM,
15Oct2005.)



Theorem  xrltnsym2 9421 
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6Feb2007.)



Theorem  xrlttr 9422 
Ordering on the extended reals is transitive. (Contributed by NM,
15Oct2005.)



Theorem  xrltso 9423 
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15Oct2005.)



Theorem  xrlttri3 9424 
Extended real version of lttri3 7715. (Contributed by NM, 9Feb2006.)



Theorem  xrltle 9425 
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19Jan2006.)



Theorem  xrltled 9426 
'Less than' implies 'less than or equal to' for extended reals.
Deduction form of xrltle 9425. (Contributed by Glauco Siliprandi,
11Dec2019.)



Theorem  xrleid 9427 
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7Feb2007.)



Theorem  xrleidd 9428 
'Less than or equal to' is reflexive for extended reals. Deduction form
of xrleid 9427. (Contributed by Glauco Siliprandi,
26Jun2021.)



Theorem  xrletri3 9429 
Trichotomy law for extended reals. (Contributed by FL, 2Aug2009.)



Theorem  xrlelttr 9430 
Transitive law for ordering on extended reals. (Contributed by NM,
19Jan2006.)



Theorem  xrltletr 9431 
Transitive law for ordering on extended reals. (Contributed by NM,
19Jan2006.)



Theorem  xrletr 9432 
Transitive law for ordering on extended reals. (Contributed by NM,
9Feb2006.)



Theorem  xrlttrd 9433 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrlelttrd 9434 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrltletrd 9435 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrletrd 9436 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrltne 9437 
'Less than' implies not equal for extended reals. (Contributed by NM,
20Jan2006.)



Theorem  nltpnft 9438 
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30Jan2006.)



Theorem  npnflt 9439 
An extended real is less than plus infinity iff they are not equal.
(Contributed by Jim Kingdon, 17Apr2023.)



Theorem  xgepnf 9440 
An extended real which is greater than plus infinity is plus infinity.
(Contributed by Thierry Arnoux, 18Dec2016.)



Theorem  ngtmnft 9441 
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2Feb2006.)



Theorem  nmnfgt 9442 
An extended real is greater than minus infinite iff they are not equal.
(Contributed by Jim Kingdon, 17Apr2023.)



Theorem  xrrebnd 9443 
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2Feb2006.)



Theorem  xrre 9444 
A way of proving that an extended real is real. (Contributed by NM,
9Mar2006.)



Theorem  xrre2 9445 
An extended real between two others is real. (Contributed by NM,
6Feb2007.)



Theorem  xrre3 9446 
A way of proving that an extended real is real. (Contributed by FL,
29May2014.)



Theorem  ge0gtmnf 9447 
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  ge0nemnf 9448 
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xrrege0 9449 
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  z2ge 9450* 
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28Aug2005.)



Theorem  xnegeq 9451 
Equality of two extended numbers with in front of them.
(Contributed by FL, 26Dec2011.) (Proof shortened by Mario Carneiro,
20Aug2015.)



Theorem  xnegpnf 9452 
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26Dec2011.)



Theorem  xnegmnf 9453 
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26Dec2011.) (Revised by Mario Carneiro, 20Aug2015.)



Theorem  rexneg 9454 
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26Dec2011.) (Proof shortened by Mario Carneiro, 20Aug2015.)



Theorem  xneg0 9455 
The negative of zero. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xnegcl 9456 
Closure of extended real negative. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xnegneg 9457 
Extended real version of negneg 7883. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xneg11 9458 
Extended real version of neg11 7884. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xltnegi 9459 
Forward direction of xltneg 9460. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xltneg 9460 
Extended real version of ltneg 8091. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleneg 9461 
Extended real version of leneg 8094. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xlt0neg1 9462 
Extended real version of lt0neg1 8097. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xlt0neg2 9463 
Extended real version of lt0neg2 8098. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xle0neg1 9464 
Extended real version of le0neg1 8099. (Contributed by Mario Carneiro,
9Sep2015.)



Theorem  xle0neg2 9465 
Extended real version of le0neg2 8100. (Contributed by Mario Carneiro,
9Sep2015.)



Theorem  xrpnfdc 9466 
An extended real is or is not plus infinity. (Contributed by Jim Kingdon,
13Apr2023.)

DECID 

Theorem  xrmnfdc 9467 
An extended real is or is not minus infinity. (Contributed by Jim
Kingdon, 13Apr2023.)

DECID 

Theorem  xaddf 9468 
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 21Aug2015.)



Theorem  xaddval 9469 
Value of the extended real addition operation. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  xaddpnf1 9470 
Addition of positive infinity on the right. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  xaddpnf2 9471 
Addition of positive infinity on the left. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  xaddmnf1 9472 
Addition of negative infinity on the right. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  xaddmnf2 9473 
Addition of negative infinity on the left. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  pnfaddmnf 9474 
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, 20Aug2015.)



Theorem  mnfaddpnf 9475 
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, 20Aug2015.)



Theorem  rexadd 9476 
The extended real addition operation when both arguments are real.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  rexsub 9477 
Extended real subtraction when both arguments are real. (Contributed by
Mario Carneiro, 23Aug2015.)



Theorem  rexaddd 9478 
The extended real addition operation when both arguments are real.
Deduction version of rexadd 9476. (Contributed by Glauco Siliprandi,
24Dec2020.)



Theorem  xnegcld 9479 
Closure of extended real negative. (Contributed by Mario Carneiro,
28May2016.)



Theorem  xrex 9480 
The set of extended reals exists. (Contributed by NM, 24Dec2006.)



Theorem  xaddnemnf 9481 
Closure of extended real addition in the subset
.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xaddnepnf 9482 
Closure of extended real addition in the subset
.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xnegid 9483 
Extended real version of negid 7880. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xaddcl 9484 
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xaddcom 9485 
The extended real addition operation is commutative. (Contributed by NM,
26Dec2011.)



Theorem  xaddid1 9486 
Extended real version of addid1 7771. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xaddid2 9487 
Extended real version of addid2 7772. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xaddid1d 9488 
is a right identity for
extended real addition. (Contributed by
Glauco Siliprandi, 17Aug2020.)



Theorem  xnn0lenn0nn0 9489 
An extended nonnegative integer which is less than or equal to a
nonnegative integer is a nonnegative integer. (Contributed by AV,
24Nov2021.)

NN0* 

Theorem  xnn0le2is012 9490 
An extended nonnegative integer which is less than or equal to 2 is either
0 or 1 or 2. (Contributed by AV, 24Nov2021.)

NN0*


Theorem  xnn0xadd0 9491 
The sum of two extended nonnegative integers is iff each of the two
extended nonnegative integers is . (Contributed by AV,
14Dec2020.)

NN0* NN0* 

Theorem  xnegdi 9492 
Extended real version of negdi 7890. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xaddass 9493 
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 9494, where is not present. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  xaddass2 9494 
Associativity of extended real addition. See xaddass 9493 for notes on the
hypotheses. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xpncan 9495 
Extended real version of pncan 7839. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xnpcan 9496 
Extended real version of npcan 7842. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleadd1a 9497 
Extended real version of leadd1 8059; note that the converse implication is
not true, unlike the real version (for example but
).
(Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleadd2a 9498 
Commuted form of xleadd1a 9497. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleadd1 9499 
Weakened version of xleadd1a 9497 under which the reverse implication is
true. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xltadd1 9500 
Extended real version of ltadd1 8058. (Contributed by Mario Carneiro,
23Aug2015.) (Revised by Jim Kingdon, 16Apr2023.)

