Home | Metamath
Proof Explorer Theorem List (p. 131 of 466) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xaddge0 13001 | The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | xle2add 13002 | Extended real version of le2add 11466. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 +𝑒 𝐵) ≤ (𝐶 +𝑒 𝐷))) | ||
Theorem | xlt2add 13003 | Extended real version of lt2add 11469. Note that ltleadd 11467, which has weaker assumptions, is not true for the extended reals (since 0 + +∞ < 1 + +∞ fails). (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))) | ||
Theorem | xsubge0 13004 | Extended real version of subge0 11497. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ (𝐴 +𝑒 -𝑒𝐵) ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | xposdif 13005 | Extended real version of posdif 11477. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))) | ||
Theorem | xlesubadd 13006 | Under certain conditions, the conclusion of lesubadd 11456 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶)) → ((𝐴 +𝑒 -𝑒𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 +𝑒 𝐵))) | ||
Theorem | xmullem 13007 | Lemma for rexmul 13014. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ ¬ (𝐴 = 0 ∨ 𝐵 = 0)) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞)))) ∧ ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞)))) → 𝐴 ∈ ℝ) | ||
Theorem | xmullem2 13008 | Lemma for xmulneg1 13012. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((((0 < 𝐵 ∧ 𝐴 = +∞) ∨ (𝐵 < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = +∞) ∨ (𝐴 < 0 ∧ 𝐵 = -∞))) → ¬ (((0 < 𝐵 ∧ 𝐴 = -∞) ∨ (𝐵 < 0 ∧ 𝐴 = +∞)) ∨ ((0 < 𝐴 ∧ 𝐵 = -∞) ∨ (𝐴 < 0 ∧ 𝐵 = +∞))))) | ||
Theorem | xmulcom 13009 | Extended real multiplication is commutative. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) = (𝐵 ·e 𝐴)) | ||
Theorem | xmul01 13010 | Extended real version of mul01 11163. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 0) = 0) | ||
Theorem | xmul02 13011 | Extended real version of mul02 11162. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (0 ·e 𝐴) = 0) | ||
Theorem | xmulneg1 13012 | Extended real version of mulneg1 11420. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵)) | ||
Theorem | xmulneg2 13013 | Extended real version of mulneg2 11421. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e -𝑒𝐵) = -𝑒(𝐴 ·e 𝐵)) | ||
Theorem | rexmul 13014 | The extended real multiplication when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵)) | ||
Theorem | xmulf 13015 | The extended real multiplication operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ·e :(ℝ* × ℝ*)⟶ℝ* | ||
Theorem | xmulcl 13016 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ·e 𝐵) ∈ ℝ*) | ||
Theorem | xmulpnf1 13017 | Multiplication by plus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e +∞) = +∞) | ||
Theorem | xmulpnf2 13018 | Multiplication by plus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (+∞ ·e 𝐴) = +∞) | ||
Theorem | xmulmnf1 13019 | Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (𝐴 ·e -∞) = -∞) | ||
Theorem | xmulmnf2 13020 | Multiplication by minus infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (-∞ ·e 𝐴) = -∞) | ||
Theorem | xmulpnf1n 13021 | Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (𝐴 ·e +∞) = -∞) | ||
Theorem | xmulid1 13022 | Extended real version of mulid1 10982. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ·e 1) = 𝐴) | ||
Theorem | xmulid2 13023 | Extended real version of mulid2 10983. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (1 ·e 𝐴) = 𝐴) | ||
Theorem | xmulm1 13024 | Extended real version of mulm1 11425. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (-1 ·e 𝐴) = -𝑒𝐴) | ||
Theorem | xmulasslem2 13025 | Lemma for xmulass 13030. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((0 < 𝐴 ∧ 𝐴 = -∞) → 𝜑) | ||
Theorem | xmulgt0 13026 | Extended real version of mulgt0 11061. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵)) | ||
Theorem | xmulge0 13027 | Extended real version of mulge0 11502. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵)) | ||
Theorem | xmulasslem 13028* | Lemma for xmulass 13030. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝑥 = 𝐷 → (𝜓 ↔ 𝑋 = 𝑌)) & ⊢ (𝑥 = -𝑒𝐷 → (𝜓 ↔ 𝐸 = 𝐹)) & ⊢ (𝜑 → 𝑋 ∈ ℝ*) & ⊢ (𝜑 → 𝑌 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 0 < 𝑥)) → 𝜓) & ⊢ (𝜑 → (𝑥 = 0 → 𝜓)) & ⊢ (𝜑 → 𝐸 = -𝑒𝑋) & ⊢ (𝜑 → 𝐹 = -𝑒𝑌) ⇒ ⊢ (𝜑 → 𝑋 = 𝑌) | ||
Theorem | xmulasslem3 13029 | Lemma for xmulass 13030. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 < 𝐶)) → ((𝐴 ·e 𝐵) ·e 𝐶) = (𝐴 ·e (𝐵 ·e 𝐶))) | ||
Theorem | xmulass 13030 | Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 12992 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 13031 | Extended real version of lemul1a 11838. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) | ||
Theorem | xlemul2a 13032 | Extended real version of lemul2a 11839. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵)) | ||
Theorem | xlemul1 13033 | Extended real version of lemul1 11836. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) | ||
Theorem | xlemul2 13034 | Extended real version of lemul2 11837. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐶 ·e 𝐴) ≤ (𝐶 ·e 𝐵))) | ||
Theorem | xltmul1 13035 | Extended real version of ltmul1 11834. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴 ·e 𝐶) < (𝐵 ·e 𝐶))) | ||
Theorem | xltmul2 13036 | Extended real version of ltmul2 11835. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐶 ·e 𝐴) < (𝐶 ·e 𝐵))) | ||
Theorem | xadddilem 13037 | Lemma for xadddi 13038. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) | ||
Theorem | xadddi 13038 | Distributive property for extended real addition and multiplication. Like xaddass 12992, 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 13039 | Commuted version of xadddi 13038. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | xadddi2 13040 | The assumption that the multiplier be real in xadddi 13038 can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) | ||
Theorem | xadddi2r 13041 | Commuted version of xadddi2 13040. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵) ∧ 𝐶 ∈ ℝ*) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
Theorem | x2times 13042 | Extended real version of 2times 12118. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ (𝐴 ∈ ℝ* → (2 ·e 𝐴) = (𝐴 +𝑒 𝐴)) | ||
Theorem | xnegcld 13043 | Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -𝑒𝐴 ∈ ℝ*) | ||
Theorem | xaddcld 13044 | The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ ℝ*) | ||
Theorem | xmulcld 13045 | Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ·e 𝐵) ∈ ℝ*) | ||
Theorem | xadd4d 13046 | Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 11212. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞)) & ⊢ (𝜑 → (𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞)) & ⊢ (𝜑 → (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) & ⊢ (𝜑 → (𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞)) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) | ||
Theorem | xnn0add4d 13047 | Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 13046. (Contributed by AV, 12-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0*) & ⊢ (𝜑 → 𝐵 ∈ ℕ0*) & ⊢ (𝜑 → 𝐶 ∈ ℕ0*) & ⊢ (𝜑 → 𝐷 ∈ ℕ0*) ⇒ ⊢ (𝜑 → ((𝐴 +𝑒 𝐵) +𝑒 (𝐶 +𝑒 𝐷)) = ((𝐴 +𝑒 𝐶) +𝑒 (𝐵 +𝑒 𝐷))) | ||
Theorem | xrsupexmnf 13048* | Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {-∞}) ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ (𝐴 ∪ {-∞})𝑦 < 𝑧))) | ||
Theorem | xrinfmexpnf 13049* | Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006.) |
⊢ (∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∪ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∪ {+∞})𝑧 < 𝑦))) | ||
Theorem | xrsupsslem 13050* | Lemma for xrsupss 13052. (Contributed by NM, 25-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | xrinfmsslem 13051* | Lemma for xrinfmss 13053. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ* ∧ (𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrsupss 13052* | Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | xrinfmss 13053* | Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrinfmss2 13054* | Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑥◡ < 𝑦 ∧ ∀𝑦 ∈ ℝ* (𝑦◡ < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡ < 𝑧))) | ||
Theorem | xrub 13055* | 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 13056* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) (Revised by Mario Carneiro, 21-Apr-2015.) |
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝐵 < 𝑥 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | supxr2 13057* | The supremum of a set of extended reals. (Contributed by NM, 9-Apr-2006.) |
⊢ (((𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐵 ∧ ∀𝑥 ∈ ℝ (𝑥 < 𝐵 → ∃𝑦 ∈ 𝐴 𝑥 < 𝑦))) → sup(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | supxrcl 13058 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 24-Oct-2005.) |
⊢ (𝐴 ⊆ ℝ* → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | supxrun 13059 | 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 13060 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∪ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < )) | ||
Theorem | supxrpnf 13061 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) = +∞) | ||
Theorem | supxrunb1 13062* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | supxrunb2 13063* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 < 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | supxrbnd1 13064* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | supxrbnd2 13065* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) < +∞)) | ||
Theorem | xrsup0 13066 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
⊢ sup(∅, ℝ*, < ) = -∞ | ||
Theorem | supxrub 13067 | 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 13068* | 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 13069* | 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 13070* | 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 13071 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ sup(𝐴, ℝ*, < ) < +∞) → sup(𝐴, ℝ*, < ) ∈ ℝ) | ||
Theorem | supxrgtmnf 13072 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → -∞ < sup(𝐴, ℝ*, < )) | ||
Theorem | supxrre1 13073 | 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 13074 | 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 13075 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ*) → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | infxrcl 13076 | 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 13077 | 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 13078* | 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 13079* | 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 13080 | 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 13081 | 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 13082 | 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 13083* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑦 < 𝑥 | ||
Theorem | rpltrp 13084* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ 𝑦 < 𝑥 | ||
Theorem | reltxrnmnf 13085* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
⊢ ∀𝑥 ∈ ℝ* (-∞ < 𝑥 → ∃𝑦 ∈ ℝ 𝑦 < 𝑥) | ||
Theorem | infmremnf 13086 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
⊢ inf(ℝ, ℝ*, < ) = -∞ | ||
Theorem | infmrp1 13087 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
⊢ inf(ℝ+, ℝ, < ) = 0 | ||
Syntax | cioo 13088 | Extend class notation with the set of open intervals of extended reals. |
class (,) | ||
Syntax | cioc 13089 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
class (,] | ||
Syntax | cico 13090 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
class [,) | ||
Syntax | cicc 13091 | Extend class notation with the set of closed intervals of extended reals. |
class [,] | ||
Definition | df-ioo 13092* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Definition | df-ioc 13093* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ (,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) | ||
Definition | df-ico 13094* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) | ||
Definition | df-icc 13095* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | ||
Theorem | ixxval 13096* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴𝑂𝐵) = {𝑧 ∈ ℝ* ∣ (𝐴𝑅𝑧 ∧ 𝑧𝑆𝐵)}) | ||
Theorem | elixx1 13097* | Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴𝑂𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴𝑅𝐶 ∧ 𝐶𝑆𝐵))) | ||
Theorem | ixxf 13098* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ 𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ* | ||
Theorem | ixxex 13099* | The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ 𝑂 ∈ V | ||
Theorem | ixxssxr 13100* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ 𝑂 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑆𝑦)}) ⇒ ⊢ (𝐴𝑂𝐵) ⊆ ℝ* |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |