Home | Metamath
Proof Explorer Theorem List (p. 416 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | supsubc 41501* | The supremum function distributes over subtraction in a sense similar to that in supaddc 11597. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 − 𝐵)} ⇒ ⊢ (𝜑 → (sup(𝐴, ℝ, < ) − 𝐵) = sup(𝐶, ℝ, < )) | ||
Theorem | xralrple2 41502* | Show that 𝐴 is less than 𝐵 by showing that there is no positive bound on the difference. A variant on xralrple 12588. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ+ 𝐴 ≤ ((1 + 𝑥) · 𝐵))) | ||
Theorem | nnuzdisj 41503 | 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 41504 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐵 ↔ (𝐴 / 𝐵) < 𝐴)) | ||
Theorem | xrltned 41505 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nnsplit 41506 | Express the set of positive integers as the disjoint (see nnuzdisj 41503) union of the first 𝑁 values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝑁 ∈ ℕ → ℕ = ((1...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) | ||
Theorem | divdiv3d 41507 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐶 · 𝐵))) | ||
Theorem | abslt2sqd 41508 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (abs‘𝐴) < (abs‘𝐵)) ⇒ ⊢ (𝜑 → (𝐴↑2) < (𝐵↑2)) | ||
Theorem | qenom 41509 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≈ ω | ||
Theorem | qct 41510 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ℚ ≼ ω | ||
Theorem | xrltnled 41511 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) | ||
Theorem | lenlteq 41512 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | xrred 41513 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ -∞) & ⊢ (𝜑 → 𝐴 ≠ +∞) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rr2sscn2 41514 | The cartesian square of ℝ is a subset of the cartesian square of ℂ. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (ℝ × ℝ) ⊆ (ℂ × ℂ) | ||
Theorem | infxr 41515* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → ∃𝑦 ∈ 𝐴 𝑦 < 𝑥)) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) = 𝐵) | ||
Theorem | infxrunb2 41516* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | infxrbnd2 41517* | 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 41518 | Lemma for infleinf 41520, case 𝐵 ≠ ∅ ∧ -∞ < inf(𝐵, ℝ*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ (inf(𝐵, ℝ*, < ) +𝑒 (𝑊 / 2))) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 (𝑊 / 2))) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ (inf(𝐵, ℝ*, < ) +𝑒 𝑊)) | ||
Theorem | infleinflem2 41519 | Lemma for infleinf 41520, when inf(𝐵, ℝ*, < ) = -∞. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ⊆ ℝ*) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 < (𝑅 − 2)) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ≤ (𝑋 +𝑒 1)) ⇒ ⊢ (𝜑 → 𝑍 < 𝑅) | ||
Theorem | infleinf 41520* | 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 41521* | 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 41522* | 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 41523 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | suplesup2 41524* | 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 41525 | 𝑁 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 41526* | A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | nnn0 41527 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ℕ ≠ ∅ | ||
Theorem | fzct 41528 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁...𝑀) ≼ ω | ||
Theorem | rpgtrecnn 41529* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐴 ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴) | ||
Theorem | fzossuz 41530 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑀..^𝑁) ⊆ (ℤ≥‘𝑀) | ||
Theorem | infrefilb 41531 | 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 41532 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, < )) | ||
Theorem | xrralrecnnle 41533* | 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 41534 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝑁..^𝑀) ≼ ω | ||
Theorem | frexr 41535 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | ||
Theorem | nnrecrp 41536 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ+) | ||
Theorem | qred 41537 | A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | reclt0d 41538 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) < 0) | ||
Theorem | lt0neg1dd 41539 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 0 < -𝐴) | ||
Theorem | mnfled 41540 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -∞ ≤ 𝐴) | ||
Theorem | infxrcld 41541 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | xrralrecnnge 41542* | 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 41543 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 < 0 ↔ (1 / 𝐴) < 0)) | ||
Theorem | ltmulneg 41544 | Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐵 · 𝐶) < (𝐴 · 𝐶))) | ||
Theorem | allbutfi 41545* | For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 41245 and eliuniin2 41267 (here, the precondition can be dropped; see eliuniincex 41256). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 ⇒ ⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑛 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵) | ||
Theorem | ltdiv23neg 41546 | Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 0) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 < 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) < 𝐶 ↔ (𝐴 / 𝐶) < 𝐵)) | ||
Theorem | xreqnltd 41547 | A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐵) | ||
Theorem | mnfnre2 41548 | Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ¬ -∞ ∈ ℝ | ||
Theorem | uzssre 41549 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (ℤ≥‘𝑀) ⊆ ℝ | ||
Theorem | zssxr 41550 | The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ℤ ⊆ ℝ* | ||
Theorem | fisupclrnmpt 41551* | A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐵 ↦ 𝐶), 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supxrunb3 41552* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ sup(𝐴, ℝ*, < ) = +∞)) | ||
Theorem | elfzod 41553 | Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 < 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑀..^𝑁)) | ||
Theorem | fimaxre4 41554* | A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) | ||
Theorem | ren0 41555 | The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ℝ ≠ ∅ | ||
Theorem | eluzelz2 41556 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ) | ||
Theorem | resabs2d 41557 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)) | ||
Theorem | uzid2 41558 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝑀 ∈ (ℤ≥‘𝑁) → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | supxrleubrnmpt 41559* | 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 41560 | An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ 𝑍 ⊆ ℝ | ||
Theorem | uzssd 41561 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀)) | ||
Theorem | eluzd 41562 | Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝑍) | ||
Theorem | elfzd 41563 | Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ≤ 𝐾) & ⊢ (𝜑 → 𝐾 ≤ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) | ||
Theorem | infxrlbrnmpt2 41564* | 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 41565 | An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (𝐴 ≠ -∞ ∧ 𝐴 ≠ +∞))) | ||
Theorem | uz0 41566 | The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (¬ 𝑀 ∈ ℤ → (ℤ≥‘𝑀) = ∅) | ||
Theorem | eluzelz2d 41567 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℤ) | ||
Theorem | infleinf2 41568* | 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 41569* | "Unbounded below" expressed with < and with ≤. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑤 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) | ||
Theorem | uzidd2 41570 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑍) | ||
Theorem | uzssd2 41571 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ 𝑍) | ||
Theorem | rexabslelem 41572* | 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 41573* | 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 41574* | Given a "for all but finitely many" condition, the condition holds from 𝑁 on. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐵 & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ 𝑁 = inf({𝑛 ∈ 𝑍 ∣ ∀𝑚 ∈ (ℤ≥‘𝑛)𝑋 ∈ 𝐵}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑁 ∈ 𝑍 ∧ ∀𝑚 ∈ (ℤ≥‘𝑁)𝑋 ∈ 𝐵)) | ||
Theorem | supxrrernmpt 41575* | 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 41576* | 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 41577* | 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 41578* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ⊆ ℝ* → (∀𝑥 ∈ ℝ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf(𝐴, ℝ*, < ) = -∞)) | ||
Theorem | uzn0d 41579 | The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝜑 → 𝑍 ≠ ∅) | ||
Theorem | uzssd3 41580 | Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (ℤ≥‘𝑁) ⊆ 𝑍) | ||
Theorem | rexabsle2 41581* | 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 41582* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ℝ ∃𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ*, < ) = -∞)) | ||
Theorem | supxrre3rnmpt 41583* | 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 41584* | 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 41585* | 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 41586 | A subset of the reals is a subset of the extended reals. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ℝ*) | ||
Theorem | supxrmnf2 41587 | Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ⊆ ℝ* → sup((𝐴 ∖ {-∞}), ℝ*, < ) = sup(𝐴, ℝ*, < )) | ||
Theorem | supxrcli 41588 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ⊆ ℝ* ⇒ ⊢ sup(𝐴, ℝ*, < ) ∈ ℝ* | ||
Theorem | uzid3 41589 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ (ℤ≥‘𝑁)) | ||
Theorem | infxrlesupxr 41590 | The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr 41604. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → inf(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )) | ||
Theorem | xnegeqd 41591 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵) | ||
Theorem | xnegrecl 41592 | The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ) | ||
Theorem | xnegnegi 41593 | Extended real version of negneg 10925. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ -𝑒-𝑒𝐴 = 𝐴 | ||
Theorem | xnegeqi 41594 | Equality of two extended numbers with -𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝑒𝐴 = -𝑒𝐵 | ||
Theorem | nfxnegd 41595 | Deduction version of nfxneg 41617. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝑒𝐴) | ||
Theorem | xnegnegd 41596 | Extended real version of negnegd 10977. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → -𝑒-𝑒𝐴 = 𝐴) | ||
Theorem | uzred 41597 | An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | xnegcli 41598 | Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ -𝑒𝐴 ∈ ℝ* | ||
Theorem | supminfrnmpt 41599* | 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 | ceilged 41600 | The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ (⌈‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |