P. 133 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xgepnf 13201	An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ* → (+∞ ≤ 𝐴 ↔ 𝐴 = +∞))
Theorem	ngtmnft 13202	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
Theorem	xlemnf 13203	An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ -∞ ↔ 𝐴 = -∞))
Theorem	xrrebnd 13204	An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞)))
Theorem	xrre 13205	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
Theorem	xrre2 13206	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ)
Theorem	xrre3 13207	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < +∞)) → 𝐴 ∈ ℝ)
Theorem	ge0gtmnf 13208	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
Theorem	ge0nemnf 13209	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≠ -∞)
Theorem	xrrege0 13210	A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
Theorem	xrmax1 13211	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	xrmax2 13212	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	xrmin1 13213	The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	xrmin2 13214	The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	xrmaxeq 13215	The maximum of two extended reals is equal to the first if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = 𝐴)
Theorem	xrmineq 13216	The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ≤ 𝐴) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) = 𝐵)
Theorem	xrmaxlt 13217	Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	xrltmin 13218	Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	xrmaxle 13219	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
Theorem	xrlemin 13220	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ≤ if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶)))
Theorem	max1 13221	A number is less than or equal to the maximum of it and another. See also max1ALT 13222. (Contributed by NM, 3-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	max1ALT 13222	A number is less than or equal to the maximum of it and another. This version of max1 13221 omits the 𝐵 ∈ ℝ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 13221 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	max2 13223	A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	2resupmax 13224	The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	min1 13225	The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	min2 13226	The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	maxle 13227	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by NM, 29-Sep-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) ≤ 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐶)))
Theorem	lemin 13228	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐶)))
Theorem	maxlt 13229	Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	ltmin 13230	Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	lemaxle 13231	A real number which is less than or equal to a second real number is less than or equal to the maximum/supremum of the second real number and a third real number. (Contributed by AV, 8-Jun-2021.)
⊢ (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ if(𝐶 ≤ 𝐵, 𝐵, 𝐶))
Theorem	max0sub 13232	Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴)
Theorem	ifle 13233	An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵))
Theorem	z2ge 13234*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘))
Theorem	qbtwnre 13235*	The rational numbers are dense in ℝ: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28. (Contributed by NM, 18-Nov-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
Theorem	qbtwnxr 13236*	The rational numbers are dense in ℝ*: any two extended real numbers have a rational between them. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ∃𝑥 ∈ ℚ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
Theorem	qsqueeze 13237*	If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0)
Theorem	qextltlem 13238*	Lemma for qextlt 13239 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))))
Theorem	qextlt 13239*	An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)))
Theorem	qextle 13240*	An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))
Theorem	xralrple 13241*	Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥)))
Theorem	alrple 13242*	Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + 𝑥)))
Theorem	xnegeq 13243	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	xnegex 13244	A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒𝐴 ∈ V
Theorem	xnegpnf 13245	Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒+∞ = -∞
Theorem	xnegmnf 13246	Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒-∞ = +∞
Theorem	rexneg 13247	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 13248	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒0 = 0
Theorem	xnegcl 13249	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*)
Theorem	xnegneg 13250	Extended real version of negneg 11518. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴)
Theorem	xneg11 13251	Extended real version of neg11 11519. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵))
Theorem	xltnegi 13252	Forward direction of xltneg 13253. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴)
Theorem	xltneg 13253	Extended real version of ltneg 11724. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴))
Theorem	xleneg 13254	Extended real version of leneg 11727. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴))
Theorem	xlt0neg1 13255	Extended real version of lt0neg1 11730. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴))
Theorem	xlt0neg2 13256	Extended real version of lt0neg2 11731. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0))
Theorem	xle0neg1 13257	Extended real version of le0neg1 11732. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴))
Theorem	xle0neg2 13258	Extended real version of le0neg2 11733. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0))
Theorem	xaddval 13259	Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞), if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞), if(𝐵 = +∞, +∞, if(𝐵 = -∞, -∞, (𝐴 + 𝐵))))))
Theorem	xaddf 13260	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulval 13261	Value of the extended real multiplication operation. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = if((𝐴 = 0 ∨ 𝐵 = 0), 0, if((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))), +∞, if((((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))), -∞, (𝐴 · 𝐵)))))
Theorem	xaddpnf1 13262	Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
Theorem	xaddpnf2 13263	Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞)
Theorem	xaddmnf1 13264	Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
Theorem	xaddmnf2 13265	Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞)
Theorem	pnfaddmnf 13266	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.)
⊢ (+∞ +𝑒 -∞) = 0
Theorem	mnfaddpnf 13267	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.)
⊢ (-∞ +𝑒 +∞) = 0
Theorem	rexadd 13268	The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
Theorem	rexsub 13269	Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 − 𝐵))
Theorem	rexaddd 13270	The extended real addition operation when both arguments are real. Deduction version of rexadd 13268. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
Theorem	xnn0xaddcl 13271	The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.)
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 +𝑒 𝐵) ∈ ℕ0*)
Theorem	xaddnemnf 13272	Closure of extended real addition in the subset ℝ* / {-∞}. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞)
Theorem	xaddnepnf 13273	Closure of extended real addition in the subset ℝ* / {+∞}. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞)
Theorem	xnegid 13274	Extended real version of negid 11515. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 -𝑒𝐴) = 0)
Theorem	xaddcl 13275	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
Theorem	xaddcom 13276	The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴))
Theorem	xaddrid 13277	Extended real version of addrid 11400. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴)
Theorem	xaddlid 13278	Extended real version of addlid 11403. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴)
Theorem	xaddridd 13279	0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴)
Theorem	xnn0lem1lt 13280	Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	xnn0lenn0nn0 13281	An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021.)
⊢ ((𝑀 ∈ ℕ0* ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℕ0)
Theorem	xnn0le2is012 13282	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.)
⊢ ((𝑁 ∈ ℕ0* ∧ 𝑁 ≤ 2) → (𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2))
Theorem	xnn0xadd0 13283	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.)
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → ((𝐴 +𝑒 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
Theorem	xnegdi 13284	Extended real version of negdi 11525. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
Theorem	xaddass 13285	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 13286, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xaddass2 13286	Associativity of extended real addition. See xaddass 13285 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xpncan 13287	Extended real version of pncan 11473. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴)
Theorem	xnpcan 13288	Extended real version of npcan 11476. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	xleadd1a 13289	Extended real version of leadd1 11692; note that the converse implication is not true, unlike the real version (for example 0 < 1 but (1 +𝑒 +∞) ≤ (0 +𝑒 +∞)). (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶))
Theorem	xleadd2a 13290	Commuted form of xleadd1a 13289. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵))
Theorem	xleadd1 13291	Weakened version of xleadd1a 13289 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)))
Theorem	xltadd1 13292	Extended real version of ltadd1 11691. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
Theorem	xltadd2 13293	Extended real version of ltadd2 11324. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵)))
Theorem	xaddge0 13294	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +𝑒 𝐵))
Theorem	xle2add 13295	Extended real version of le2add 11706. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)))
Theorem	xlt2add 13296	Extended real version of lt2add 11709. Note that ltleadd 11707, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷)))
Theorem	xsubge0 13297	Extended real version of subge0 11737. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	xposdif 13298	Extended real version of posdif 11717. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
Theorem	xlesubadd 13299	Under certain conditions, the conclusion of lesubadd 11696 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
Theorem	xmullem 13300	Lemma for rexmul 13307. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)