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	min1 13201	The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐴)
Theorem	min2 13202	The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐴, 𝐵) ≤ 𝐵)
Theorem	maxle 13203	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 13204	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 13205	Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (if(𝐴 ≤ 𝐵, 𝐵, 𝐴) < 𝐶 ↔ (𝐴 < 𝐶 ∧ 𝐵 < 𝐶)))
Theorem	ltmin 13206	Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < if(𝐵 ≤ 𝐶, 𝐵, 𝐶) ↔ (𝐴 < 𝐵 ∧ 𝐴 < 𝐶)))
Theorem	lemaxle 13207	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 13208	Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) − if(0 ≤ -𝐴, -𝐴, 0)) = 𝐴)
Theorem	ifle 13209	An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴) ∧ (𝜑 → 𝜓)) → if(𝜑, 𝐴, 𝐵) ≤ if(𝜓, 𝐴, 𝐵))
Theorem	z2ge 13210*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑘 ∈ ℤ (𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘))
Theorem	qbtwnre 13211*	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 13212*	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 13213*	If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ ℚ (0 < 𝑥 → 𝐴 < 𝑥)) → 𝐴 = 0)
Theorem	qextltlem 13214*	Lemma for qextlt 13215 and qextle . (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ∃𝑥 ∈ ℚ (¬ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵) ∧ ¬ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵))))
Theorem	qextlt 13215*	An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 < 𝐴 ↔ 𝑥 < 𝐵)))
Theorem	qextle 13216*	An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℚ (𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵)))
Theorem	xralrple 13217*	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 13218*	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 13219	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 13220	A negative extended real exists as a set. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒𝐴 ∈ V
Theorem	xnegpnf 13221	Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
⊢ -𝑒+∞ = -∞
Theorem	xnegmnf 13222	Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒-∞ = +∞
Theorem	rexneg 13223	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 13224	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ -𝑒0 = 0
Theorem	xnegcl 13225	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → -𝑒𝐴 ∈ ℝ*)
Theorem	xnegneg 13226	Extended real version of negneg 11541. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → -𝑒-𝑒𝐴 = 𝐴)
Theorem	xneg11 13227	Extended real version of neg11 11542. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 = -𝑒𝐵 ↔ 𝐴 = 𝐵))
Theorem	xltnegi 13228	Forward direction of xltneg 13229. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → -𝑒𝐵 < -𝑒𝐴)
Theorem	xltneg 13229	Extended real version of ltneg 11745. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ -𝑒𝐵 < -𝑒𝐴))
Theorem	xleneg 13230	Extended real version of leneg 11748. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ -𝑒𝐵 ≤ -𝑒𝐴))
Theorem	xlt0neg1 13231	Extended real version of lt0neg1 11751. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 < 0 ↔ 0 < -𝑒𝐴))
Theorem	xlt0neg2 13232	Extended real version of lt0neg2 11752. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 < 𝐴 ↔ -𝑒𝐴 < 0))
Theorem	xle0neg1 13233	Extended real version of le0neg1 11753. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ 0 ↔ 0 ≤ -𝑒𝐴))
Theorem	xle0neg2 13234	Extended real version of le0neg2 11754. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ≤ 𝐴 ↔ -𝑒𝐴 ≤ 0))
Theorem	xaddval 13235	Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = if(𝐴 = +∞, if(𝐵 = -∞, 0, +∞), if(𝐴 = -∞, if(𝐵 = +∞, 0, -∞), if(𝐵 = +∞, +∞, if(𝐵 = -∞, -∞, (𝐴 + 𝐵))))))
Theorem	xaddf 13236	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ +𝑒 :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulval 13237	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 13238	Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
Theorem	xaddpnf2 13239	Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → (+∞ +𝑒 𝐴) = +∞)
Theorem	xaddmnf1 13240	Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
Theorem	xaddmnf2 13241	Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞)
Theorem	pnfaddmnf 13242	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 13243	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 13244	The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
Theorem	rexsub 13245	Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 -𝑒𝐵) = (𝐴 − 𝐵))
Theorem	rexaddd 13246	The extended real addition operation when both arguments are real. Deduction version of rexadd 13244. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
Theorem	xnn0xaddcl 13247	The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020.)
⊢ ((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) → (𝐴 +𝑒 𝐵) ∈ ℕ0*)
Theorem	xaddnemnf 13248	Closure of extended real addition in the subset ℝ* / {-∞}. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞)
Theorem	xaddnepnf 13249	Closure of extended real addition in the subset ℝ* / {+∞}. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞)
Theorem	xnegid 13250	Extended real version of negid 11538. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 -𝑒𝐴) = 0)
Theorem	xaddcl 13251	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
Theorem	xaddcom 13252	The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴))
Theorem	xaddrid 13253	Extended real version of addrid 11425. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴)
Theorem	xaddlid 13254	Extended real version of addlid 11428. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴)
Theorem	xaddridd 13255	0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴)
Theorem	xnn0lem1lt 13256	Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	xnn0lenn0nn0 13257	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 13258	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 13259	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 13260	Extended real version of negdi 11548. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
Theorem	xaddass 13261	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 13262, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xaddass2 13262	Associativity of extended real addition. See xaddass 13261 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xpncan 13263	Extended real version of pncan 11497. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴)
Theorem	xnpcan 13264	Extended real version of npcan 11500. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	xleadd1a 13265	Extended real version of leadd1 11713; 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 13266	Commuted form of xleadd1a 13265. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵))
Theorem	xleadd1 13267	Weakened version of xleadd1a 13265 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)))
Theorem	xltadd1 13268	Extended real version of ltadd1 11712. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
Theorem	xltadd2 13269	Extended real version of ltadd2 11349. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵)))
Theorem	xaddge0 13270	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +𝑒 𝐵))
Theorem	xle2add 13271	Extended real version of le2add 11727. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)))
Theorem	xlt2add 13272	Extended real version of lt2add 11730. Note that ltleadd 11728, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷)))
Theorem	xsubge0 13273	Extended real version of subge0 11758. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	xposdif 13274	Extended real version of posdif 11738. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
Theorem	xlesubadd 13275	Under certain conditions, the conclusion of lesubadd 11717 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
Theorem	xmullem 13276	Lemma for rexmul 13283. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)
Theorem	xmullem2 13277	Lemma for xmulneg1 13281. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
Theorem	xmulcom 13278	Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = (𝐵 ·e 𝐴))
Theorem	xmul01 13279	Extended real version of mul01 11424. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0)
Theorem	xmul02 13280	Extended real version of mul02 11423. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ·e 𝐴) = 0)
Theorem	xmulneg1 13281	Extended real version of mulneg1 11681. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵))
Theorem	xmulneg2 13282	Extended real version of mulneg2 11682. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e -𝑒𝐵) = -𝑒(𝐴 ·e 𝐵))
Theorem	rexmul 13283	The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵))
Theorem	xmulf 13284	The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulcl 13285	Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) ∈ ℝ*)
Theorem	xmulpnf1 13286	Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e +∞) = +∞)
Theorem	xmulpnf2 13287	Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (+∞ ·e 𝐴) = +∞)
Theorem	xmulmnf1 13288	Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e -∞) = -∞)
Theorem	xmulmnf2 13289	Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (-∞ ·e 𝐴) = -∞)
Theorem	xmulpnf1n 13290	Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (𝐴 ·e +∞) = -∞)
Theorem	xmulrid 13291	Extended real version of mulrid 11243. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 1) = 𝐴)
Theorem	xmullid 13292	Extended real version of mullid 11244. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (1 ·e 𝐴) = 𝐴)
Theorem	xmulm1 13293	Extended real version of mulm1 11686. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (-1 ·e 𝐴) = -𝑒𝐴)
Theorem	xmulasslem2 13294	Lemma for xmulass 13299. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((0 < 𝐴 ∧ 𝐴 = -∞) → 𝜑)
Theorem	xmulgt0 13295	Extended real version of mulgt0 11322. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵))
Theorem	xmulge0 13296	Extended real version of mulge0 11763. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵))
Theorem	xmulasslem 13297*	Lemma for xmulass 13299. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝑥 = 𝐷 → (𝜓 ↔ 𝑋 = 𝑌))    &   ⊢ (𝑥 = -𝑒𝐷 → (𝜓 ↔ 𝐸 = 𝐹))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 0 < 𝑥)) → 𝜓)    &   ⊢ (𝜑 → (𝑥 = 0 → 𝜓))    &   ⊢ (𝜑 → 𝐸 = -𝑒𝑋)    &   ⊢ (𝜑 → 𝐹 = -𝑒𝑌)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	xmulasslem3 13298	Lemma for xmulass 13299. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → ((𝐴 ·e 𝐵) ·e 𝐶) = (𝐴 ·e (𝐵 ·e 𝐶)))
Theorem	xmulass 13299	Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 13261 which has to avoid the "undefined" combinations +∞ +𝑒 -∞ and -∞ +𝑒 +∞. The equivalent "undefined" expression here would be 0 ·e +∞, but since this is defined to equal 0 any zeroes in the expression make the whole thing evaluate to zero (on both sides), thus establishing the identity in this case. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ·e 𝐵) ·e 𝐶) = (𝐴 ·e (𝐵 ·e 𝐶)))
Theorem	xlemul1a 13300	Extended real version of lemul1a 12099. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))