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	max1 13201	A number is less than or equal to the maximum of it and another. See also max1ALT 13202. (Contributed by NM, 3-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	max1ALT 13202	A number is less than or equal to the maximum of it and another. This version of max1 13201 omits the 𝐵 ∈ ℝ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 13201 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	max2 13203	A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	2resupmax 13204	The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → sup({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
Theorem	min1 13205	The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	min2 13206	The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	maxle 13207	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 13208	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 13209	Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	ltmin 13210	Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	lemaxle 13211	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 13212	Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴)
Theorem	ifle 13213	An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵))
Theorem	z2ge 13214*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘))
Theorem	qbtwnre 13215*	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 13216*	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 13217*	If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0)
Theorem	qextltlem 13218*	Lemma for qextlt 13219 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))))
Theorem	qextlt 13219*	An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)))
Theorem	qextle 13220*	An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))
Theorem	xralrple 13221*	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 13222*	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 13223	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 13224	A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒𝐴 ∈ V
Theorem	xnegpnf 13225	Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒+∞ = -∞
Theorem	xnegmnf 13226	Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒-∞ = +∞
Theorem	rexneg 13227	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 13228	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒0 = 0
Theorem	xnegcl 13229	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*)
Theorem	xnegneg 13230	Extended real version of negneg 11533. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴)
Theorem	xneg11 13231	Extended real version of neg11 11534. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵))
Theorem	xltnegi 13232	Forward direction of xltneg 13233. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴)
Theorem	xltneg 13233	Extended real version of ltneg 11737. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴))
Theorem	xleneg 13234	Extended real version of leneg 11740. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴))
Theorem	xlt0neg1 13235	Extended real version of lt0neg1 11743. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴))
Theorem	xlt0neg2 13236	Extended real version of lt0neg2 11744. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0))
Theorem	xle0neg1 13237	Extended real version of le0neg1 11745. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴))
Theorem	xle0neg2 13238	Extended real version of le0neg2 11746. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0))
Theorem	xaddval 13239	Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞), if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞), if(𝐵 = +∞, +∞, if(𝐵 = -∞, -∞, (𝐴 + 𝐵))))))
Theorem	xaddf 13240	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulval 13241	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 13242	Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
Theorem	xaddpnf2 13243	Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞)
Theorem	xaddmnf1 13244	Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
Theorem	xaddmnf2 13245	Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞)
Theorem	pnfaddmnf 13246	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 13247	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 13248	The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
Theorem	rexsub 13249	Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 − 𝐵))
Theorem	rexaddd 13250	The extended real addition operation when both arguments are real. Deduction version of rexadd 13248. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
Theorem	xnn0xaddcl 13251	The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.)
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 +𝑒 𝐵) ∈ ℕ0*)
Theorem	xaddnemnf 13252	Closure of extended real addition in the subset ℝ* / {-∞}. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞)
Theorem	xaddnepnf 13253	Closure of extended real addition in the subset ℝ* / {+∞}. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞)
Theorem	xnegid 13254	Extended real version of negid 11530. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 -𝑒𝐴) = 0)
Theorem	xaddcl 13255	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
Theorem	xaddcom 13256	The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴))
Theorem	xaddrid 13257	Extended real version of addrid 11415. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴)
Theorem	xaddlid 13258	Extended real version of addlid 11418. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴)
Theorem	xaddridd 13259	0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴)
Theorem	xnn0lem1lt 13260	Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	xnn0lenn0nn0 13261	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 13262	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 13263	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 13264	Extended real version of negdi 11540. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
Theorem	xaddass 13265	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 13266, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xaddass2 13266	Associativity of extended real addition. See xaddass 13265 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xpncan 13267	Extended real version of pncan 11488. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴)
Theorem	xnpcan 13268	Extended real version of npcan 11491. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	xleadd1a 13269	Extended real version of leadd1 11705; 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 13270	Commuted form of xleadd1a 13269. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵))
Theorem	xleadd1 13271	Weakened version of xleadd1a 13269 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)))
Theorem	xltadd1 13272	Extended real version of ltadd1 11704. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
Theorem	xltadd2 13273	Extended real version of ltadd2 11339. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵)))
Theorem	xaddge0 13274	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +𝑒 𝐵))
Theorem	xle2add 13275	Extended real version of le2add 11719. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)))
Theorem	xlt2add 13276	Extended real version of lt2add 11722. Note that ltleadd 11720, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷)))
Theorem	xsubge0 13277	Extended real version of subge0 11750. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	xposdif 13278	Extended real version of posdif 11730. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
Theorem	xlesubadd 13279	Under certain conditions, the conclusion of lesubadd 11709 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
Theorem	xmullem 13280	Lemma for rexmul 13287. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)
Theorem	xmullem2 13281	Lemma for xmulneg1 13285. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
Theorem	xmulcom 13282	Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = (𝐵 ·e 𝐴))
Theorem	xmul01 13283	Extended real version of mul01 11414. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0)
Theorem	xmul02 13284	Extended real version of mul02 11413. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ·e 𝐴) = 0)
Theorem	xmulneg1 13285	Extended real version of mulneg1 11673. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵))
Theorem	xmulneg2 13286	Extended real version of mulneg2 11674. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e -𝑒𝐵) = -𝑒(𝐴 ·e 𝐵))
Theorem	rexmul 13287	The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵))
Theorem	xmulf 13288	The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulcl 13289	Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) ∈ ℝ*)
Theorem	xmulpnf1 13290	Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e +∞) = +∞)
Theorem	xmulpnf2 13291	Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (+∞ ·e 𝐴) = +∞)
Theorem	xmulmnf1 13292	Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e -∞) = -∞)
Theorem	xmulmnf2 13293	Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (-∞ ·e 𝐴) = -∞)
Theorem	xmulpnf1n 13294	Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (𝐴 ·e +∞) = -∞)
Theorem	xmulrid 13295	Extended real version of mulrid 11233. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 1) = 𝐴)
Theorem	xmullid 13296	Extended real version of mullid 11234. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (1 ·e 𝐴) = 𝐴)
Theorem	xmulm1 13297	Extended real version of mulm1 11678. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (-1 ·e 𝐴) = -𝑒𝐴)
Theorem	xmulasslem2 13298	Lemma for xmulass 13303. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((0 < 𝐴 ∧ 𝐴 = -∞) → 𝜑)
Theorem	xmulgt0 13299	Extended real version of mulgt0 11312. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵))
Theorem	xmulge0 13300	Extended real version of mulge0 11755. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵))