P. 135 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xnn0lem1lt 13401	Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0*) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁))
Theorem	xnn0lenn0nn0 13402	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 13403	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 13404	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*) → ((𝐴 +e 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0)))
Theorem	xnegdi 13405	Extended real version of negdi 11642. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → -e(𝐴 +e 𝐵) = ( -e𝐴 +e -e𝐵))
Theorem	xaddass 13406	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 13407, where +∞ is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +e 𝐵) +e 𝐶) = (𝐴 +e (𝐵 +e 𝐶)))
Theorem	xaddass2 13407	Associativity of extended real addition. See xaddass 13406 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +e 𝐵) +e 𝐶) = (𝐴 +e (𝐵 +e 𝐶)))
Theorem	xpncan 13408	Extended real version of pncan 11590. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +e 𝐵) +e -e𝐵) = 𝐴)
Theorem	xnpcan 13409	Extended real version of npcan 11593. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐴 +e -e𝐵) +e 𝐵) = 𝐴)
Theorem	xleadd1a 13410	Extended real version of leadd1 11811; note that the converse implication is not true, unlike the real version (for example 0 < 1 but (1 +e +∞) ≤ (0 +e +∞)). (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐴 +e 𝐶) ≤ (𝐵 +e 𝐶))
Theorem	xleadd2a 13411	Commuted form of xleadd1a 13410. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → (𝐶 +e 𝐴) ≤ (𝐶 +e 𝐵))
Theorem	xleadd1 13412	Weakened version of xleadd1a 13410 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 +e 𝐶) ≤ (𝐵 +e 𝐶)))
Theorem	xltadd1 13413	Extended real version of ltadd1 11810. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +e 𝐶) < (𝐵 +e 𝐶)))
Theorem	xltadd2 13414	Extended real version of ltadd2 11441. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 +e 𝐴) < (𝐶 +e 𝐵)))
Theorem	xaddge0 13415	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +e 𝐵))
Theorem	xle2add 13416	Extended real version of le2add 11825. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +e 𝐵) ≤ (𝐶 +e 𝐷)))
Theorem	xlt2add 13417	Extended real version of lt2add 11828. Note that ltleadd 11826, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +e 𝐵) < (𝐶 +e 𝐷)))
Theorem	xsubge0 13418	Extended real version of subge0 11856. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +e -e𝐵) ↔ 𝐵 ≤ 𝐴))
Theorem	xposdif 13419	Extended real version of posdif 11836. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +e -e𝐴)))
Theorem	xlesubadd 13420	Under certain conditions, the conclusion of lesubadd 11815 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +e -e𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +e 𝐵)))
Theorem	xmullem 13421	Lemma for rexmul 13428. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ)
Theorem	xmullem2 13422	Lemma for xmulneg1 13426. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))))
Theorem	xmulcom 13423	Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = (𝐵 ·e 𝐴))
Theorem	xmul01 13424	Extended real version of mul01 11516. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0)
Theorem	xmul02 13425	Extended real version of mul02 11515. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (0 ·e 𝐴) = 0)
Theorem	xmulneg1 13426	Extended real version of mulneg1 11779. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ( -e𝐴 ·e 𝐵) = -e(𝐴 ·e 𝐵))
Theorem	xmulneg2 13427	Extended real version of mulneg2 11780. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e -e𝐵) = -e(𝐴 ·e 𝐵))
Theorem	rexmul 13428	The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵))
Theorem	xmulf 13429	The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ·e :(ℝ* × ℝ*)⟶ℝ*
Theorem	xmulcl 13430	Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) ∈ ℝ*)
Theorem	xmulpnf1 13431	Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e +∞) = +∞)
Theorem	xmulpnf2 13432	Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (+∞ ·e 𝐴) = +∞)
Theorem	xmulmnf1 13433	Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e -∞) = -∞)
Theorem	xmulmnf2 13434	Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (-∞ ·e 𝐴) = -∞)
Theorem	xmulpnf1n 13435	Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (𝐴 ·e +∞) = -∞)
Theorem	xmulrid 13436	Extended real version of mulrid 11333. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 1) = 𝐴)
Theorem	xmullid 13437	Extended real version of mullid 11334. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (1 ·e 𝐴) = 𝐴)
Theorem	xmulm1 13438	Extended real version of mulm1 11784. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → ( -1 ·e 𝐴) = -e𝐴)
Theorem	xmulasslem2 13439	Lemma for xmulass 13444. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((0 < 𝐴 ∧ 𝐴 = -∞) → 𝜑)
Theorem	xmulgt0 13440	Extended real version of mulgt0 11414. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵))
Theorem	xmulge0 13441	Extended real version of mulge0 11861. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵))
Theorem	xmulasslem 13442*	Lemma for xmulass 13444. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝑥 = 𝐷 → (𝜓 ↔ 𝑋 = 𝑌))    &   ⊢ (𝑥 = -e𝐷 → (𝜓 ↔ 𝐸 = 𝐹))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 0 < 𝑥)) → 𝜓)    &   ⊢ (𝜑 → (𝑥 = 0 → 𝜓))    &   ⊢ (𝜑 → 𝐸 = -e𝑋)    &   ⊢ (𝜑 → 𝐹 = -e𝑌)    ⇒   ⊢ (𝜑 → 𝑋 = 𝑌)
Theorem	xmulasslem3 13443	Lemma for xmulass 13444. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → ((𝐴 ·e 𝐵) ·e 𝐶) = (𝐴 ·e (𝐵 ·e 𝐶)))
Theorem	xmulass 13444	Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 13406 which has to avoid the "undefined" combinations +∞ +e -∞ and -∞ +e +∞. 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 13445	Extended real version of lemul1a 12198. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))
Theorem	xlemul2a 13446	Extended real version of lemul2a 12199. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵))
Theorem	xlemul1 13447	Extended real version of lemul1 12196. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))
Theorem	xlemul2 13448	Extended real version of lemul2 12197. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵)))
Theorem	xltmul1 13449	Extended real version of ltmul1 12194. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴 ·e 𝐶) < (𝐵 ·e 𝐶)))
Theorem	xltmul2 13450	Extended real version of ltmul2 12195. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐶 ·e 𝐴) < (𝐶 ·e 𝐵)))
Theorem	xadddilem 13451	Lemma for xadddi 13452. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e (𝐵 +e 𝐶)) = ((𝐴 ·e 𝐵) +e (𝐴 ·e 𝐶)))
Theorem	xadddi 13452	Distributive property for extended real addition and multiplication. Like xaddass 13406, 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 𝐵) +e (𝐴 ·e 𝐶)))
Theorem	xadddir 13453	Commuted version of xadddi 13452. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → ((𝐴 +e 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +e (𝐵 ·e 𝐶)))
Theorem	xadddi2 13454	The assumption that the multiplier be real in xadddi 13452 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e (𝐵 +e 𝐶)) = ((𝐴 ·e 𝐵) +e (𝐴 ·e 𝐶)))
Theorem	xadddi2r 13455	Commuted version of xadddi2 13454. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ*) → ((𝐴 +e 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +e (𝐵 ·e 𝐶)))
Theorem	x2times 13456	Extended real version of 2times 12505. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐴 ∈ ℝ* → (2 ·e 𝐴) = (𝐴 +e 𝐴))
Theorem	xnegcld 13457	Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → -e𝐴 ∈ ℝ*)
Theorem	xaddcld 13458	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 +e 𝐵) ∈ ℝ*)
Theorem	xmulcld 13459	Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → (𝐴 ·e 𝐵) ∈ ℝ*)
Theorem	xadd4d 13460	Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 11566. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞))    &   ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞))    &   ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞))    &   ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞))    ⇒   ⊢ (𝜑 → ((𝐴 +e 𝐵) +e (𝐶 +e 𝐷)) = ((𝐴 +e 𝐶) +e (𝐵 +e 𝐷)))
Theorem	xnn0add4d 13461	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 13460. (Contributed by AV, 12-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0*)    ⇒   ⊢ (𝜑 → ((𝐴 +e 𝐵) +e (𝐶 +e 𝐷)) = ((𝐴 +e 𝐶) +e (𝐵 +e 𝐷)))
5.5.3  Supremum and infimum on the extended reals
Theorem	xrsupexmnf 13462*	Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.)
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {-∞}) ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ (𝐴 ∪ {-∞})𝑦 < 𝑧)))
Theorem	xrinfmexpnf 13463*	Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.)
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦)))
Theorem	xrsupsslem 13464*	Lemma for xrsupss 13466. (Contributed by NM, 25-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	xrinfmsslem 13465*	Lemma for xrinfmss 13467. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	xrsupss 13466*	Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.)
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	xrinfmss 13467*	Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.)
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	xrinfmss2 13468*	Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥◡ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡ < 𝑧)))
Theorem	xrub 13469*	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 13470*	The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.)
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵)
Theorem	supxr2 13471*	The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.)
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵)
Theorem	supxrcl 13472	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.)
⊢ (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	supxrun 13473	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 13474	Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∪ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < ))
Theorem	supxrpnf 13475	The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) = +∞)
Theorem	supxrunb1 13476*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	supxrunb2 13477*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞))
Theorem	supxrbnd1 13478*	The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞))
Theorem	supxrbnd2 13479*	The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.)
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞))
Theorem	xrsup0 13480	The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.)
⊢ sup(∅, ℝ*, < ) = -∞
Theorem	supxrub 13481	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 13482*	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 13483*	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 13484*	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 13485	The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup(𝐴, ℝ*, < ) < +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ)
Theorem	supxrgtmnf 13486	The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < ))
Theorem	supxrre1 13487	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 13488	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 13489	Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < ))
Theorem	xrsupssd 13490	Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐶 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → sup(𝐵, ℝ*, < ) ≤ sup(𝐶, ℝ*, < ))
Theorem	infxrcl 13491	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 13492	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 13493*	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 13494*	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 13495	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 13496	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 13497	Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → inf(𝐵, ℝ*, < ) ≤ inf(𝐴, ℝ*, < ))
Theorem	reltre 13498*	For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.)
⊢ ∀𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑦 < 𝑥
Theorem	rpltrp 13499*	For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.)
⊢ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ 𝑦 < 𝑥
Theorem	reltxrnmnf 13500*	For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.)
⊢ ∀𝑥 ∈ ℝ* (-∞ < 𝑥 → ∃𝑦 ∈ ℝ 𝑦 < 𝑥)