![]() |
Metamath
Proof Explorer Theorem List (p. 454 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xrlexaddrp 45301* | If an extended real number 𝐴 can be approximated from above, adding positive reals to 𝐵, then 𝐴 is less than or equal to 𝐵. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | supsubc 45302* | The supremum function distributes over subtraction in a sense similar to that in supaddc 12232. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 − 𝐵)} ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 𝐵) = sup(𝐶, ℝ, < )) | ||
Theorem | xralrple2 45303* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. A variant on xralrple 13243. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ ((1 + 𝑥) · 𝐵))) | ||
Theorem | nnuzdisj 45304 | The first 𝑁 elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ ((1...𝑁) ∩ (ℤ≥‘(𝑁 + 1))) = ∅ | ||
Theorem | ltdivgt1 45305 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐵 ↔ (𝐴 / 𝐵) < 𝐴)) | ||
Theorem | xrltned 45306 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nnsplit 45307 | Express the set of positive integers as the disjoint (see nnuzdisj 45304) union of the first 𝑁 values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝑁 ∈ ℕ → ℕ = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
Theorem | divdiv3d 45308 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐶 · 𝐵))) | ||
Theorem | abslt2sqd 45309 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < (abs‘𝐵)) ⇒ ⊢ (𝜑 → (𝐴↑2) < (𝐵↑2)) | ||
Theorem | qenom 45310 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≈ ω | ||
Theorem | qct 45311 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≼ ω | ||
Theorem | xrltnled 45312 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
Theorem | lenlteq 45313 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xrred 45314 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ -∞) & ⊢ (𝜑 → 𝐴 ≠ +∞) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rr2sscn2 45315 | The cartesian square of ℝ is a subset of the cartesian square of ℂ. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (ℝ × ℝ) ⊆ (ℂ × ℂ) | ||
Theorem | infxr 45316* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | infxrunb2 45317* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | infxrbnd2 45318* | The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ -∞ < inf(𝐴, ℝ*, < ))) | ||
Theorem | infleinflem1 45319 | Lemma for infleinf 45321, case 𝐵 ≠ ∅ ∧ -∞ < inf(𝐵, ℝ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ (inf(𝐵, ℝ*, < ) +𝑒 (𝑊 / 2))) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 (𝑊 / 2))) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ (inf(𝐵, ℝ*, < ) +𝑒 𝑊)) | ||
Theorem | infleinflem2 45320 | Lemma for infleinf 45321, when inf(𝐵, ℝ*, < ) = -∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 < (𝑅 − 2)) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1)) ⇒ ⊢ (𝜑 → 𝑍 < 𝑅) | ||
Theorem | infleinf 45321* | If any element of 𝐵 can be approximated from above by members of 𝐴, then the infimum of 𝐴 is less than or equal to the infimum of 𝐵. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, < )) | ||
Theorem | xralrple4 45322* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + (𝑥↑𝑁)))) | ||
Theorem | xralrple3 45323* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ (𝐵 + (𝐶 · 𝑥)))) | ||
Theorem | eluzelzd 45324 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | suplesup2 45325* | If any element of 𝐴 is less than or equal to an element in 𝐵, then the supremum of 𝐴 is less than or equal to the supremum of 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | recnnltrp 45326 | 𝑁 is a natural number large enough that its reciprocal is smaller than the given positive 𝐸. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ 𝑁 = ((⌊‘(1 / 𝐸)) + 1) ⇒ ⊢ (𝐸 ∈ ℝ+ → (𝑁 ∈ ℕ ∧ (1 / 𝑁) < 𝐸)) | ||
Theorem | nnn0 45327 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ℕ ≠ ∅ | ||
Theorem | fzct 45328 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁...𝑀) ≼ ω | ||
Theorem | rpgtrecnn 45329* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐴 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴) | ||
Theorem | fzossuz 45330 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑀..^𝑁) ⊆ (ℤ≥‘𝑀) | ||
Theorem | infxrrefi 45331 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < )) | ||
Theorem | xrralrecnnle 45332* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ 𝐴 ≤ (𝐵 + (1 / 𝑛)))) | ||
Theorem | fzoct 45333 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁..^𝑀) ≼ ω | ||
Theorem | frexr 45334 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | ||
Theorem | nnrecrp 45335 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ+) | ||
Theorem | reclt0d 45336 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) < 0) | ||
Theorem | lt0neg1dd 45337 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 0 < -𝐴) | ||
Theorem | infxrcld 45338 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | xrralrecnnge 45339* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (𝐴 − (1 / 𝑛)) ≤ 𝐵)) | ||
Theorem | reclt0 45340 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 < 0 ↔ (1 / 𝐴) < 0)) | ||
Theorem | ltmulneg 45341 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐵 · 𝐶) < (𝐴 · 𝐶))) | ||
Theorem | allbutfi 45342* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 45038 and eliuniin2 45059 (here, the precondition can be dropped; see eliuniincex 45048). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) | ||
Theorem | ltdiv23neg 45343 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) | ||
Theorem | xreqnltd 45344 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐵) | ||
Theorem | mnfnre2 45345 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ¬ -∞ ∈ ℝ | ||
Theorem | zssxr 45346 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ℤ ⊆ ℝ* | ||
Theorem | fisupclrnmpt 45347* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐵 ↦ 𝐶), 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supxrunb3 45348* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | elfzod 45349 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 < 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑀..^𝑁)) | ||
Theorem | fimaxre4 45350* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) | ||
Theorem | ren0 45351 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ℝ ≠ ∅ | ||
Theorem | eluzelz2 45352 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ) | ||
Theorem | resabs2d 45353 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)) | ||
Theorem | uzid2 45354 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝑀 ∈ (ℤ≥‘𝑁) → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | supxrleubrnmpt 45355* | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | uzssre2 45356 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℝ | ||
Theorem | uzssd 45357 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀)) | ||
Theorem | eluzd 45358 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑍) | ||
Theorem | infxrlbrnmpt2 45359* | A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐷) | ||
Theorem | xrre4 45360 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞))) | ||
Theorem | uz0 45361 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅) | ||
Theorem | eluzelz2d 45362 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | infleinf2 45363* | If any element in 𝐵 is greater than or equal to an element in 𝐴, then the infimum of 𝐴 is less than or equal to the infimum of 𝐵. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, < )) | ||
Theorem | unb2ltle 45364* | "Unbounded below" expressed with < and with ≤. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) | ||
Theorem | uzidd2 45365 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑍) | ||
Theorem | uzssd2 45366 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ 𝑍) | ||
Theorem | rexabslelem 45367* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) | ||
Theorem | rexabsle 45368* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑤 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑧 ≤ 𝐵))) | ||
Theorem | allbutfiinf 45369* | Given a "for all but finitely many" condition, the condition holds from 𝑁 on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) | ||
Theorem | supxrrernmpt 45370* | The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < )) | ||
Theorem | suprleubrnmpt 45371* | The supremum of a nonempty bounded indexed set of reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | infrnmptle 45372* | An indexed infimum of extended reals is smaller than another indexed infimum of extended reals, when every indexed element is smaller than the corresponding one. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐶), ℝ*, < )) | ||
Theorem | infxrunb3 45373* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | uzn0d 45374 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑍 ≠ ∅) | ||
Theorem | uzssd3 45375 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (ℤ≥‘𝑁) ⊆ 𝑍) | ||
Theorem | rexabsle2 45376* | An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (abs‘𝐵) ≤ 𝑦 ↔ (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵))) | ||
Theorem | infxrunb3rnmpt 45377* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -∞)) | ||
Theorem | supxrre3rnmpt 45378* | The indexed supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)) | ||
Theorem | uzublem 45379* | A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ Ⅎ𝑗𝑋 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) & ⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝐾)𝐵 ≤ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥) | ||
Theorem | uzub 45380* | A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∃𝑘 ∈ 𝑍 ∀𝑗 ∈ (ℤ≥‘𝑘)𝐵 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥)) | ||
Theorem | ssrexr 45381 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℝ*) | ||
Theorem | supxrmnf2 45382 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∖ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < )) | ||
Theorem | supxrcli 45383 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ⊆ ℝ* ⇒ ⊢ sup(𝐴, ℝ*, < ) ∈ ℝ* | ||
Theorem | uzid3 45384 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ (ℤ≥‘𝑁)) | ||
Theorem | infxrlesupxr 45385 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 45398. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | xnegeqd 45386 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵) | ||
Theorem | xnegrecl 45387 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ) | ||
Theorem | xnegnegi 45388 | Extended real version of negneg 11556. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ -𝑒-𝑒𝐴 = 𝐴 | ||
Theorem | xnegeqi 45389 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝑒𝐴 = -𝑒𝐵 | ||
Theorem | nfxnegd 45390 | Deduction version of nfxneg 45410. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝑒𝐴) | ||
Theorem | xnegnegd 45391 | Extended real version of negnegd 11608. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -𝑒-𝑒𝐴 = 𝐴) | ||
Theorem | uzred 45392 | An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | xnegcli 45393 | Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ -𝑒𝐴 ∈ ℝ* | ||
Theorem | supminfrnmpt 45394* | The indexed supremum of a bounded-above set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) = -inf(ran (𝑥 ∈ 𝐴 ↦ -𝐵), ℝ, < )) | ||
Theorem | infxrpnf 45395 | Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → inf((𝐴 ∪ {+∞}), ℝ*, < ) = inf(𝐴, ℝ*, < )) | ||
Theorem | infxrrnmptcl 45396* | The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ∈ ℝ*) | ||
Theorem | leneg2d 45397 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) | ||
Theorem | supxrltinfxr 45398 | The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ sup(∅, ℝ*, < ) < inf(∅, ℝ*, < ) | ||
Theorem | max1d 45399 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | ||
Theorem | supxrleubrnmptf 45400 | The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |