Home | Metamath
Proof Explorer Theorem List (p. 416 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elrnmpoid 41501* | Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) ∈ ran 𝐹) | ||
Theorem | axccd 41502* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ≈ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
Theorem | axccd2 41503* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
Theorem | funimassd 41504* | Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Fun 𝐹) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐵) | ||
Theorem | fimassd 41505 | The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝑋) ⊆ 𝐵) | ||
Theorem | feqresmptf 41506* | Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) | ||
Theorem | elrnmpt1d 41507 | Elementhood in an image set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 ∈ ran 𝐹) | ||
Theorem | dmresss 41508 | The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ dom (𝐴 ↾ 𝐵) ⊆ dom 𝐴 | ||
Theorem | dmmptssf 41509 | The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | dmmptdf2 41510 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
Theorem | dmuz 41511 | Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ dom ℤ≥ = ℤ | ||
Theorem | fmptd2f 41512* | Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) | ||
Theorem | mpteq1df 41513 | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mptexf 41514 | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6986. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | fvmpt4 41515* | Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
Theorem | fmptf 41516* | Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | resimass 41517 | The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝐴 ↾ 𝐵) “ 𝐶) ⊆ (𝐴 “ 𝐶) | ||
Theorem | mptssid 41518 | The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐵) | ||
Theorem | mptfnd 41519 | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
Theorem | mpteq12da 41520 | An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | rnmptlb 41521* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) | ||
Theorem | rnmptbddlem 41522* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
Theorem | rnmptbdd 41523* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
Theorem | mptima2 41524* | Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵)) | ||
Theorem | funimaeq 41525* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) = (𝐺 “ 𝐴)) | ||
Theorem | rnmptssf 41526* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | rnmptbd2lem 41527* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
Theorem | rnmptbd2 41528* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
Theorem | infnsuprnmpt 41529* | The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) = -sup(ran (𝑥 ∈ 𝐴 ↦ -𝐵), ℝ, < )) | ||
Theorem | suprclrnmpt 41530* | Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in maps-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) ∈ ℝ) | ||
Theorem | suprubrnmpt2 41531* | A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐷 ≤ sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < )) | ||
Theorem | suprubrnmpt 41532* | A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < )) | ||
Theorem | rnmptssdf 41533* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | rnmptbdlem 41534* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
Theorem | rnmptbd 41535* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
Theorem | rnmptss2 41536* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ ran (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | elmptima 41537* | The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐷) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐷)𝐶 = 𝐵)) | ||
Theorem | ralrnmpt3 41538* | A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | fvelima2 41539* | Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (𝐹 “ 𝐶)) → ∃𝑥 ∈ (𝐴 ∩ 𝐶)(𝐹‘𝑥) = 𝐵) | ||
Theorem | funresd 41540 | A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴)) | ||
Theorem | rnmptssbi 41541* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (ran 𝐹 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)) | ||
Theorem | fnfvelrnd 41542 | A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | imass2d 41543 | Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | imassmpt 41544* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 “ 𝐶) ⊆ 𝐷 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ 𝐷)) | ||
Theorem | fpmd 41545 | A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | fconst7 41546* | An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | sub2times 41547 | Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴) | ||
Theorem | abssubrp 41548 | The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+) | ||
Theorem | elfzfzo 41549 | Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ (𝑀..^𝑁) ↔ (𝐴 ∈ (𝑀...𝑁) ∧ 𝐴 < 𝑁)) | ||
Theorem | oddfl 41550 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1)) | ||
Theorem | abscosbd 41551 | Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1) | ||
Theorem | mul13d 41552 | Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐶 · (𝐵 · 𝐴))) | ||
Theorem | negpilt0 41553 | Negative π is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ -π < 0 | ||
Theorem | dstregt0 41554* | A complex number 𝐴 that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦))) | ||
Theorem | subadd4b 41555 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐷)) = ((𝐴 − 𝐷) + (𝐶 − 𝐵))) | ||
Theorem | xrlttri5d 41556 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | neglt 41557 | The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ+ → -𝐴 < 𝐴) | ||
Theorem | zltlesub 41558 | If an integer 𝑁 is less than or equal to a real, and we subtract a quantity less than 1, then 𝑁 is less than or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 < 1) & ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ) ⇒ ⊢ (𝜑 → 𝑁 ≤ (𝐴 − 𝐵)) | ||
Theorem | divlt0gt0d 41559 | The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) < 0) | ||
Theorem | subsub23d 41560 | Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
Theorem | 2timesgt 41561 | Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 < (2 · 𝐴)) | ||
Theorem | reopn 41562 | The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℝ ∈ (topGen‘ran (,)) | ||
Theorem | elfzop1le2 41563 | A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 + 1) ≤ 𝑁) | ||
Theorem | sub31 41564 | Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 − 𝐶)) = (𝐶 − (𝐵 − 𝐴))) | ||
Theorem | nnne1ge2 41565 | A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 2 ≤ 𝑁) | ||
Theorem | lefldiveq 41566 | A closed enough, smaller real 𝐶 has the same floor of 𝐴 when both are divided by 𝐵. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ((𝐴 − (𝐴 mod 𝐵))[,]𝐴)) ⇒ ⊢ (𝜑 → (⌊‘(𝐴 / 𝐵)) = (⌊‘(𝐶 / 𝐵))) | ||
Theorem | negsubdi3d 41567 | Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → -(𝐴 − 𝐵) = (-𝐴 − -𝐵)) | ||
Theorem | ltdiv2dd 41568 | Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) < (𝐶 / 𝐴)) | ||
Theorem | abssinbd 41569 | Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(sin‘𝐴)) ≤ 1) | ||
Theorem | halffl 41570 | Floor of (1 / 2). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (⌊‘(1 / 2)) = 0 | ||
Theorem | monoords 41571* | Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) & ⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝐼 < 𝐽) ⇒ ⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) | ||
Theorem | hashssle 41572 | The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by hashss 13773, and hashssle 41572 should be deleted afterwards. |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴)) | ||
Theorem | lttri5d 41573 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | fzisoeu 41574* | A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 13823 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐻 ∈ Fin) & ⊢ (𝜑 → < Or 𝐻) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑁 = ((♯‘𝐻) + (𝑀 − 1)) ⇒ ⊢ (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)) | ||
Theorem | lt3addmuld 41575 | If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐷) & ⊢ (𝜑 → 𝐵 < 𝐷) & ⊢ (𝜑 → 𝐶 < 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) < (3 · 𝐷)) | ||
Theorem | absnpncan2d 41576 | Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐷)) ≤ (((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷)))) | ||
Theorem | fperiodmullem 41577* | A function with period T is also periodic with period nonnegative multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) | ||
Theorem | fperiodmul 41578* | A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 · 𝑇))) = (𝐹‘𝑋)) | ||
Theorem | upbdrech 41579* | Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐶 = sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | lt4addmuld 41580 | If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐸) & ⊢ (𝜑 → 𝐵 < 𝐸) & ⊢ (𝜑 → 𝐶 < 𝐸) & ⊢ (𝜑 → 𝐷 < 𝐸) ⇒ ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) + 𝐷) < (4 · 𝐸)) | ||
Theorem | absnpncan3d 41581 | Triangular inequality, combined with cancellation law for subtraction (applied three times). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐸 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐸)) ≤ ((((abs‘(𝐴 − 𝐵)) + (abs‘(𝐵 − 𝐶))) + (abs‘(𝐶 − 𝐷))) + (abs‘(𝐷 − 𝐸)))) | ||
Theorem | upbdrech2 41582* | Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) & ⊢ 𝐶 = if(𝐴 = ∅, 0, sup({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}, ℝ, < )) ⇒ ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) | ||
Theorem | ssfiunibd 41583* | A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑥 𝐵 ≤ 𝑦) & ⊢ (𝜑 → 𝐶 ⊆ ∪ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑧 ∈ 𝐶 𝐵 ≤ 𝑤) | ||
Theorem | fzdifsuc2 41584 | Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc 12970, but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘(𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) | ||
Theorem | fzsscn 41585 | A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℂ | ||
Theorem | divcan8d 41586 | A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 / (𝐴 · 𝐵)) = (1 / 𝐴)) | ||
Theorem | dmmcand 41587 | Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 · 𝐶)) = (𝐴 · 𝐶)) | ||
Theorem | fzssre 41588 | A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝑀...𝑁) ⊆ ℝ | ||
Theorem | elfzelzd 41589 | A member of a finite set of sequential integer is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) ⇒ ⊢ (𝜑 → 𝐾 ∈ ℤ) | ||
Theorem | bccld 41590 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐾 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑁C𝐾) ∈ ℕ0) | ||
Theorem | leadd12dd 41591 | Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐶) & ⊢ (𝜑 → 𝐵 ≤ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) | ||
Theorem | fzssnn0 41592 | A finite set of sequential integers that is a subset of ℕ0. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (0...𝑁) ⊆ ℕ0 | ||
Theorem | xreqle 41593 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) | ||
Theorem | xaddid2d 41594 | 0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) ⇒ ⊢ (𝜑 → (0 +𝑒 𝐴) = 𝐴) | ||
Theorem | xadd0ge 41595 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | elfzolem1 41596 | A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝐾 ∈ (𝑀..^𝑁) → 𝐾 ≤ (𝑁 − 1)) | ||
Theorem | xrgtned 41597 | 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) | ||
Theorem | xrleneltd 41598 | 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
Theorem | xaddcomd 41599 | The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | ||
Theorem | supxrre3 41600* | The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → (sup(𝐴, ℝ*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |