Home | Metamath
Proof Explorer Theorem List (p. 386 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nemnftgtmnft 38501 | An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞) → -∞ < 𝐴) | ||
Theorem | xrgtso 38502 | 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ◡ < Or ℝ* | ||
Theorem | rpex 38503 | The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ℝ+ ∈ V | ||
Theorem | xrge0ge0 38504 | A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ (0[,]+∞) → 0 ≤ 𝐴) | ||
Theorem | xrssre 38505 | A subset of extended reals that does not contain +∞ and -∞ is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → ¬ +∞ ∈ 𝐴) & ⊢ (𝜑 → ¬ -∞ ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℝ) | ||
Theorem | ssuzfz 38506 | A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ⊆ 𝑍) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝑀...sup(𝐴, ℝ, < ))) | ||
Theorem | absfun 38507 | The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Fun abs | ||
Theorem | infrpge 38508* | The infimum of a non empty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝐴 𝑧 ≤ (inf(𝐴, ℝ*, < ) +𝑒 𝐵)) | ||
Theorem | xrlexaddrp 38509* | If an extended real number 𝐴 can be approximated from above, adding positive reals to 𝐵, then 𝐴 is smaller or equal than 𝐵. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐴 ≤ (𝐵 +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) | ||
Theorem | supsubc 38510* | The supremum function distributes over subtraction in a sense similar to that in supaddc 10867. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 − 𝐵)} ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 𝐵) = sup(𝐶, ℝ, < )) | ||
Theorem | xralrple2 38511* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. A variant on xralrple 11910. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ ((1 + 𝑥) · 𝐵))) | ||
Theorem | nnuzdisj 38512 | 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 38513 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐵 ↔ (𝐴 / 𝐵) < 𝐴)) | ||
Theorem | xrltned 38514 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nnsplit 38515 | Express the set of positive integers as the disjoint (see nnuzdisj 38512) union of the first 𝑁 values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝑁 ∈ ℕ → ℕ = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
Theorem | divdiv3d 38516 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐶 · 𝐵))) | ||
Theorem | abslt2sqd 38517 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < (abs‘𝐵)) ⇒ ⊢ (𝜑 → (𝐴↑2) < (𝐵↑2)) | ||
Theorem | qenom 38518 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≈ ω | ||
Theorem | qct 38519 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≼ ω | ||
Theorem | xrltnled 38520 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
Theorem | lenlteq 38521 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xrred 38522 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ -∞) & ⊢ (𝜑 → 𝐴 ≠ +∞) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rr2sscn2 38523 | ℝ^2 is a subset of CC^ 2. Common case. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (ℝ × ℝ) ⊆ (ℂ × ℂ) | ||
Theorem | infxr 38524* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | infxrunb2 38525* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | infxrbnd2 38526* | 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 38527 | Lemma for infleinf 38529, case 𝐵 ≠ ∅ ∧ -∞ < inf(𝐵, ℝ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ (inf(𝐵, ℝ*, < ) +𝑒 (𝑊 / 2))) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 (𝑊 / 2))) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ (inf(𝐵, ℝ*, < ) +𝑒 𝑊)) | ||
Theorem | infleinflem2 38528 | Lemma for infleinf 38529, when inf(𝐵, ℝ*, < ) = -∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 < (𝑅 − 2)) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1)) ⇒ ⊢ (𝜑 → 𝑍 < 𝑅) | ||
Theorem | infleinf 38529* | If any element of 𝐵 can be approximated from above by members of 𝐴, then the infimum of 𝐴 is smaller or equal to the infimum of 𝐵. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ 𝐴 𝑧 ≤ (𝑥 +𝑒 𝑦)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ inf(𝐵, ℝ*, < )) | ||
Theorem | xralrple4 38530* | 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 38531* | 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 38532 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | suplesup2 38533* | If any element of 𝐴 is smaller or equal to an element in 𝐵, then the supremum of 𝐴 is smaller or equal to the supremum of 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ≤ sup(𝐵, ℝ*, < )) | ||
Theorem | recnnltrp 38534 | 𝑁 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 | fiminre2 38535* | A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | nnn0 38536 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ℕ ≠ ∅ | ||
Theorem | fzct 38537 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁...𝑀) ≼ ω | ||
Theorem | rpgtrecnn 38538* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐴 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴) | ||
Theorem | fzossuz 38539 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑀..^𝑁) ⊆ (ℤ≥‘𝑀) | ||
Theorem | fzossz 38540 | A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑀..^𝑁) ⊆ ℤ | ||
Theorem | infrefilb 38541 | The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴) | ||
Theorem | infxrrefi 38542 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < )) | ||
Theorem | xrralrecnnle 38543* | 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 38544 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁..^𝑀) ≼ ω | ||
Theorem | frexr 38545 | A function taking real values, is a function taking extended real values. Common case. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | ||
Theorem | nnrecrp 38546 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ+) | ||
Theorem | qred 38547 | A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | reclt0d 38548 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) < 0) | ||
Theorem | lt0neg1dd 38549 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 0 < -𝐴) | ||
Theorem | mnfled 38550 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -∞ ≤ 𝐴) | ||
Theorem | xrleidd 38551 | 'Less than or equal to' is reflexive for extended reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐴) | ||
Theorem | negelrpd 38552 | The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℝ+) | ||
Theorem | infxrcld 38553 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | xrralrecnnge 38554* | 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 38555 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 < 0 ↔ (1 / 𝐴) < 0)) | ||
Theorem | ltmulneg 38556 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐵 · 𝐶) < (𝐴 · 𝐶))) | ||
Theorem | allbutfi 38557* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 38307 and eliuniin2 38335 (here, the precondition can be dropped; see eliuniincex 38323). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) | ||
Theorem | ltdiv23neg 38558 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) | ||
Theorem | gtnelioc 38559 | A real number larger than the upper bound of a left open right closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | ioossioc 38560 | An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵) | ||
Theorem | ioondisj2 38561 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅) | ||
Theorem | ioondisj1 38562 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐶 < 𝐷)) ∧ (𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)) → ((𝐴(,)𝐵) ∩ (𝐶(,)𝐷)) ≠ ∅) | ||
Theorem | ioosscn 38563 | An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴(,)𝐵) ⊆ ℂ | ||
Theorem | ioogtlb 38564 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝐶) | ||
Theorem | evthiccabs 38565* | Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ (abs‘(𝐹‘𝑥)) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑧)) ≤ (abs‘(𝐹‘𝑤)))) | ||
Theorem | ltnelicc 38566 | A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 < 𝐴) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | eliood 38567 | Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐶 < 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) | ||
Theorem | iooabslt 38568 | An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − 𝐵)(,)(𝐴 + 𝐵))) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < 𝐵) | ||
Theorem | gtnelicc 38569 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | iooinlbub 38570 | An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴(,)𝐵) ∩ {𝐴, 𝐵}) = ∅ | ||
Theorem | iocgtlb 38571 | An element of a left open right closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐴 < 𝐶) | ||
Theorem | iocleub 38572 | An element of a left open right closed interval is smaller or equal to its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ≤ 𝐵) | ||
Theorem | eliccd 38573 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) | ||
Theorem | iccssred 38574 | A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | ||
Theorem | eliccre 38575 | A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | eliooshift 38576 | Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 + 𝐷) ∈ ((𝐵 + 𝐷)(,)(𝐶 + 𝐷)))) | ||
Theorem | eliocd 38577 | Membership in a left open, right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴(,]𝐵)) | ||
Theorem | snunioo2 38578 | The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵)) | ||
Theorem | icoltub 38579 | An element of a left closed right open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐶 < 𝐵) | ||
Theorem | tgiooss 38580 | The restriction of the complex topology to a subset of reals, is a restriction of the standard topology on reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): Use rerest 22415 instead in fourierdlem48 39047, fourierdlem49 39048, fourierdlem62 39061 then delete this. |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝐾 ↾t 𝐴)) | ||
Theorem | eliocre 38581 | A member of a left open, right closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ (𝐴(,]𝐵)) → 𝐶 ∈ ℝ) | ||
Theorem | iooltub 38582 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵) | ||
Theorem | ioontr 38583 | The interior of an interval in the standard topology on ℝ is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵) | ||
Theorem | eliccxr 38584 | A member of a closed interval is a an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝐵[,]𝐶) → 𝐴 ∈ ℝ*) | ||
Theorem | snunioo1 38585 | The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴}) = (𝐴[,)𝐵)) | ||
Theorem | lbioc 38586 | An left open right closed interval doesn't contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ¬ 𝐴 ∈ (𝐴(,]𝐵) | ||
Theorem | ioomidp 38587 | The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → ((𝐴 + 𝐵) / 2) ∈ (𝐴(,)𝐵)) | ||
Theorem | iccdifioo 38588 | If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → ((𝐴[,]𝐵) ∖ (𝐴(,)𝐵)) = {𝐴, 𝐵}) | ||
Theorem | iccdifprioo 38589 | An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴[,]𝐵) ∖ {𝐴, 𝐵}) = (𝐴(,)𝐵)) | ||
Theorem | ioossioobi 38590 | Biconditional form of ioossioo 12136. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐷 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → ((𝐶(,)𝐷) ⊆ (𝐴(,)𝐵) ↔ (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵))) | ||
Theorem | iccshift 38591* | A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) | ||
Theorem | iccsuble 38592 | An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝐷 ∈ (𝐴[,]𝐵)) ⇒ ⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐵 − 𝐴)) | ||
Theorem | iocopn 38593 | A left open right closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝐽 = (𝐾 ↾t (𝐴(,]𝐵)) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐶(,]𝐵) ∈ 𝐽) | ||
Theorem | eliccelioc 38594 | Membership in a closed interval and in a left open right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴(,]𝐵) ↔ (𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐶 ≠ 𝐴))) | ||
Theorem | iooshift 38595* | An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝑇)(,)(𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴(,)𝐵)𝑤 = (𝑧 + 𝑇)}) | ||
Theorem | iccintsng 38596 | Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,]𝐵) ∩ (𝐵[,]𝐶)) = {𝐵}) | ||
Theorem | icoiccdif 38597 | Left closed, right open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) = ((𝐴[,]𝐵) ∖ {𝐵})) | ||
Theorem | icoopn 38598 | A left closed right open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ 𝐽 = (𝐾 ↾t (𝐴[,)𝐵)) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴[,)𝐶) ∈ 𝐽) | ||
Theorem | icoub 38599 | A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐴 ∈ ℝ* → ¬ 𝐵 ∈ (𝐴[,)𝐵)) | ||
Theorem | eliccxrd 38600 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐶 ≤ 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |