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	xaddrid 13201	Extended real version of addrid 11354. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴)
Theorem	xaddlid 13202	Extended real version of addlid 11357. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 +𝑒 𝐴) = 𝐴)
Theorem	xaddridd 13203	0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 0) = 𝐴)
Theorem	xnn0lem1lt 13204	Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	xnn0lenn0nn0 13205	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 13206	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 13207	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 13208	Extended real version of negdi 11479. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
Theorem	xaddass 13209	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 13210, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xaddass2 13210	Associativity of extended real addition. See xaddass 13209 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))
Theorem	xpncan 13211	Extended real version of pncan 11427. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 -𝑒𝐵) = 𝐴)
Theorem	xnpcan 13212	Extended real version of npcan 11430. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴)
Theorem	xleadd1a 13213	Extended real version of leadd1 11646; 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 13214	Commuted form of xleadd1a 13213. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +𝑒 𝐴) ≤ (𝐶 +𝑒 𝐵))
Theorem	xleadd1 13215	Weakened version of xleadd1a 13213 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +𝑒 𝐶) ≤ (𝐵 +𝑒 𝐶)))
Theorem	xltadd1 13216	Extended real version of ltadd1 11645. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
Theorem	xltadd2 13217	Extended real version of ltadd2 11278. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +𝑒 𝐴) < (𝐶 +𝑒 𝐵)))
Theorem	xaddge0 13218	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +𝑒 𝐵))
Theorem	xle2add 13219	Extended real version of le2add 11660. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷)))
Theorem	xlt2add 13220	Extended real version of lt2add 11663. Note that ltleadd 11661, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷)))
Theorem	xsubge0 13221	Extended real version of subge0 11691. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	xposdif 13222	Extended real version of posdif 11671. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
Theorem	xlesubadd 13223	Under certain conditions, the conclusion of lesubadd 11650 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵)))
Theorem	xmullem 13224	Lemma for rexmul 13231. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)
Theorem	xmullem2 13225	Lemma for xmulneg1 13229. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
Theorem	xmulcom 13226	Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = (𝐵 ·e 𝐴))
Theorem	xmul01 13227	Extended real version of mul01 11353. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0)
Theorem	xmul02 13228	Extended real version of mul02 11352. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ·e 𝐴) = 0)
Theorem	xmulneg1 13229	Extended real version of mulneg1 11614. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵))
Theorem	xmulneg2 13230	Extended real version of mulneg2 11615. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e -𝑒𝐵) = -𝑒(𝐴 ·e 𝐵))
Theorem	rexmul 13231	The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵))
Theorem	xmulf 13232	The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulcl 13233	Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) ∈ ℝ*)
Theorem	xmulpnf1 13234	Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e +∞) = +∞)
Theorem	xmulpnf2 13235	Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (+∞ ·e 𝐴) = +∞)
Theorem	xmulmnf1 13236	Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e -∞) = -∞)
Theorem	xmulmnf2 13237	Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (-∞ ·e 𝐴) = -∞)
Theorem	xmulpnf1n 13238	Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (𝐴 ·e +∞) = -∞)
Theorem	xmulrid 13239	Extended real version of mulrid 11172. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 1) = 𝐴)
Theorem	xmullid 13240	Extended real version of mullid 11173. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (1 ·e 𝐴) = 𝐴)
Theorem	xmulm1 13241	Extended real version of mulm1 11619. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (-1 ·e 𝐴) = -𝑒𝐴)
Theorem	xmulasslem2 13242	Lemma for xmulass 13247. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((0 < 𝐴 ∧ 𝐴 = -∞) → 𝜑)
Theorem	xmulgt0 13243	Extended real version of mulgt0 11251. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵))
Theorem	xmulge0 13244	Extended real version of mulge0 11696. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵))
Theorem	xmulasslem 13245*	Lemma for xmulass 13247. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝑥 = 𝐷 → (𝜓 ↔ 𝑋 = 𝑌))    &   ⊢ (𝑥 = -𝑒𝐷 → (𝜓 ↔ 𝐸 = 𝐹))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 0 < 𝑥)) → 𝜓)    &   ⊢ (𝜑 → (𝑥 = 0 → 𝜓))    &   ⊢ (𝜑 → 𝐸 = -𝑒𝑋)    &   ⊢ (𝜑 → 𝐹 = -𝑒𝑌)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	xmulasslem3 13246	Lemma for xmulass 13247. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → ((𝐴 ·e 𝐵) ·e 𝐶) = (𝐴 ·e (𝐵 ·e 𝐶)))
Theorem	xmulass 13247	Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 13209 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 13248	Extended real version of lemul1a 12036. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))
Theorem	xlemul2a 13249	Extended real version of lemul2a 12037. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵))
Theorem	xlemul1 13250	Extended real version of lemul1 12034. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))
Theorem	xlemul2 13251	Extended real version of lemul2 12035. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵)))
Theorem	xltmul1 13252	Extended real version of ltmul1 12032. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴 ·e 𝐶) < (𝐵 ·e 𝐶)))
Theorem	xltmul2 13253	Extended real version of ltmul2 12033. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐶 ·e 𝐴) < (𝐶 ·e 𝐵)))
Theorem	xadddilem 13254	Lemma for xadddi 13255. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
Theorem	xadddi 13255	Distributive property for extended real addition and multiplication. Like xaddass 13209, this has an unusual domain of correctness due to counterexamples like (+∞ · (2 − 1)) = -∞ ≠ ((+∞ · 2) − (+∞ · 1)) = (+∞ − +∞) = 0. In this theorem we show that if the multiplier is real then everything works as expected. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
Theorem	xadddir 13256	Commuted version of xadddi 13255. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)))
Theorem	xadddi2 13257	The assumption that the multiplier be real in xadddi 13255 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))
Theorem	xadddi2r 13258	Commuted version of xadddi2 13257. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ*) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶)))
Theorem	x2times 13259	Extended real version of 2times 12317. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (2 ·e 𝐴) = (𝐴 +𝑒 𝐴))
Theorem	xnegcld 13260	Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ*)
Theorem	xaddcld 13261	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*)
Theorem	xmulcld 13262	Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 ·e 𝐵) ∈ ℝ*)
Theorem	xadd4d 13263	Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 11403. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞))    &   ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞))    &   ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞))    &   ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞))    ⇒   ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷)))
Theorem	xnn0add4d 13264	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 13263. (Contributed by AV, 12-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0*)    ⇒   ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷)))
5.5.3  Supremum and infimum on the extended reals
Theorem	xrsupexmnf 13265*	Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.)
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {-∞}) ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ (𝐴 ∪ {-∞})𝑦 < 𝑧)))
Theorem	xrinfmexpnf 13266*	Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.)
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)))
Theorem	xrsupsslem 13267*	Lemma for xrsupss 13269. (Contributed by NM, 25-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	xrinfmsslem 13268*	Lemma for xrinfmss 13270. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	xrsupss 13269*	Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.)
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	xrinfmss 13270*	Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.)
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	xrinfmss2 13271*	Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥◡ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡ < 𝑧)))
Theorem	xrub 13272*	By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦) ↔ ∀𝑥 ∈ ℝ* (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦)))
Theorem	supxr 13273*	The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.)
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵)
Theorem	supxr2 13274*	The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.)
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵)
Theorem	supxrcl 13275	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.)
⊢ (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	supxrun 13276	The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ∧ sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) → sup((𝐴 ∪ 𝐵), ℝ*, < ) = sup(𝐵, ℝ*, < ))
Theorem	supxrmnf 13277	Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∪ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < ))
Theorem	supxrpnf 13278	The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) = +∞)
Theorem	supxrunb1 13279*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	supxrunb2 13280*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	supxrbnd1 13281*	The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞))
Theorem	supxrbnd2 13282*	The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞))
Theorem	xrsup0 13283	The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ sup(∅, ℝ*, < ) = -∞
Theorem	supxrub 13284	A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ*, < ))
Theorem	supxrlub 13285*	The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐵 < sup(𝐴, ℝ*, < ) ↔ ∃𝑥 ∈ 𝐴 𝐵 < 𝑥))
Theorem	supxrleub 13286*	The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (sup(𝐴, ℝ*, < ) ≤ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵))
Theorem	supxrre 13287*	The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005.) (Proof shortened by Mario Carneiro, 7-Sep-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) = sup(𝐴, ℝ, < ))
Theorem	supxrbnd 13288	The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup(𝐴, ℝ*, < ) < +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
Theorem	supxrgtmnf 13289	The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < ))
Theorem	supxrre1 13290	The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ sup(𝐴, ℝ*, < ) < +∞))
Theorem	supxrre2 13291	The supremum of a nonempty set of reals is real iff it is not plus infinity. (Contributed by NM, 5-Feb-2006.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ sup(𝐴, ℝ*, < ) ≠ +∞))
Theorem	supxrss 13292	Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
Theorem	xrsupssd 13293	Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐶 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → sup(𝐵, ℝ*, < ) ≤ sup(𝐶, ℝ*, < ))
Theorem	infxrcl 13294	The infimum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 19-Jan-2006.) (Revised by AV, 5-Sep-2020.)
⊢ (𝐴 ⊆ ℝ* → inf(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	infxrlb 13295	A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝐵)
Theorem	infxrgelb 13296*	The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐵 ≤ inf(𝐴, ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥))
Theorem	infxrre 13297*	The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 5-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < ))
Theorem	infxrmnf 13298	The infinimum of a set of extended reals containing minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴) → inf(𝐴, ℝ*, < ) = -∞)
Theorem	xrinf0 13299	The infimum of the empty set under the extended reals is positive infinity. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 5-Sep-2020.)
⊢ inf(∅, ℝ*, < ) = +∞
Theorem	infxrss 13300	Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → inf(𝐵, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ))