| Metamath
Proof Explorer Theorem List (p. 453 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rnmptssd 45201* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
| Theorem | projf1o 45202* | A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ 〈𝐴, 𝑥〉) ⇒ ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵)) | ||
| Theorem | fvmap 45203 | Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐴) | ||
| Theorem | fvixp2 45204* | Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | ||
| Theorem | choicefi 45205* | For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) | ||
| Theorem | mpct 45206 | The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴 ↑m 𝐵) ≼ ω) | ||
| Theorem | cnmetcoval 45207 | Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ 𝐷 = (abs ∘ − ) & ⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1st ‘(𝐹‘𝐵)) − (2nd ‘(𝐹‘𝐵))))) | ||
| Theorem | fcomptss 45208* | Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑥)))) | ||
| Theorem | elmapsnd 45209 | Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹 Fn {𝐴}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m {𝐴})) | ||
| Theorem | mapss2 45210 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))) | ||
| Theorem | fsneq 45211 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴))) | ||
| Theorem | difmap 45212 | Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶))) | ||
| Theorem | unirnmap 45213 | Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐴)) ⇒ ⊢ (𝜑 → 𝑋 ⊆ (ran ∪ 𝑋 ↑m 𝐴)) | ||
| Theorem | inmap 45214 | Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑m 𝐶) ∩ (𝐵 ↑m 𝐶)) = ((𝐴 ∩ 𝐵) ↑m 𝐶)) | ||
| Theorem | fcoss 45215 | Composition of two mappings. Similar to fco 6760, but with a weaker condition on the domain of 𝐹. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐺:𝐷⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐷⟶𝐵) | ||
| Theorem | fsneqrn 45216 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺)) | ||
| Theorem | difmapsn 45217 | Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑m {𝐶}) ∖ (𝐵 ↑m {𝐶})) = ((𝐴 ∖ 𝐵) ↑m {𝐶})) | ||
| Theorem | mapssbi 45218 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))) | ||
| Theorem | unirnmapsn 45219 | Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐶 = {𝐴} & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐶)) ⇒ ⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑m 𝐶)) | ||
| Theorem | iunmapss 45220* | The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶)) | ||
| Theorem | ssmapsn 45221* | A subset 𝐶 of a set exponentiation to a singleton, is its projection 𝐷 exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑓𝐷 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑m {𝐴})) & ⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓 ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↑m {𝐴})) | ||
| Theorem | iunmapsn 45222* | The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) = (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) | ||
| Theorem | absfico 45223 | Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ abs:ℂ⟶(0[,)+∞) | ||
| Theorem | icof 45224 | The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ* | ||
| Theorem | elpmrn 45225 | The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → ran 𝐹 ⊆ 𝐴) | ||
| Theorem | imaexi 45226 | The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Proof shortened by SN, 27-Apr-2025.) |
| ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ (𝐴 “ 𝐵) ∈ V | ||
| Theorem | axccdom 45227* | Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧 ∈ 𝑋 (𝑓‘𝑧) ∈ 𝑧)) | ||
| Theorem | dmmptdff 45228 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
| Theorem | dmmptdf 45229* | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
| Theorem | elpmi2 45230 | The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → dom 𝐹 ⊆ 𝐵) | ||
| Theorem | dmrelrnrel 45231* | A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)) | ||
| Theorem | fvcod 45232 | Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐺) & ⊢ 𝐻 = (𝐹 ∘ 𝐺) ⇒ ⊢ (𝜑 → (𝐻‘𝐴) = (𝐹‘(𝐺‘𝐴))) | ||
| Theorem | elrnmpoid 45233* | Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) ∈ ran 𝐹) | ||
| Theorem | axccd 45234* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ≈ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
| Theorem | axccd2 45235* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
| Theorem | feqresmptf 45236* | Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) | ||
| Theorem | dmmptssf 45237 | The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
| Theorem | dmmptdf2 45238 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
| Theorem | dmuz 45239 | Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ dom ℤ≥ = ℤ | ||
| Theorem | fmptd2f 45240* | Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) | ||
| Theorem | mpteq1df 45241 | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by SN, 11-Nov-2024.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | mpteq1dfOLD 45242 | Obsolete version of mpteq1df 45241 as of 11-Nov-2024. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | mptexf 45243 | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7241. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
| Theorem | fvmpt4 45244* | Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
| Theorem | fmptf 45245* | Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
| Theorem | resimass 45246 | The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ ((𝐴 ↾ 𝐵) “ 𝐶) ⊆ (𝐴 “ 𝐶) | ||
| Theorem | mptssid 45247 | The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐵) | ||
| Theorem | mptfnd 45248 | The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | ||
| Theorem | mpteq12daOLD 45249 | Obsolete version of mpteq12da 5227 as of 11-Nov-2024. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
| Theorem | rnmptlb 45250* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) | ||
| Theorem | rnmptbddlem 45251* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
| Theorem | rnmptbdd 45252* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
| Theorem | funimaeq 45253* | 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 45254* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
| Theorem | rnmptbd2lem 45255* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
| Theorem | rnmptbd2 45256* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
| Theorem | infnsuprnmpt 45257* | 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 45258* | 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 45259* | 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 45260* | 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 45261* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
| Theorem | rnmptbdlem 45262* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
| Theorem | rnmptbd 45263* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
| Theorem | rnmptss2 45264* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ ran (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
| Theorem | elmptima 45265* | The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐷) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐷)𝐶 = 𝐵)) | ||
| Theorem | ralrnmpt3 45266* | A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
| Theorem | rnmptssbi 45267* | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (ran 𝐹 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)) | ||
| Theorem | imass2d 45268 | Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
| Theorem | imassmpt 45269* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 “ 𝐶) ⊆ 𝐷 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ 𝐷)) | ||
| Theorem | fpmd 45270 | A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
| Theorem | fconst7 45271* | An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵})) | ||
| Theorem | fnmptif 45272 | Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ 𝐹 Fn 𝐴 | ||
| Theorem | dmmptif 45273 | Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐵 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = 𝐴 | ||
| Theorem | mpteq2dfa 45274 | Slightly more general equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | ||
| Theorem | dmmpt1 45275 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom (𝑥 ∈ 𝐵 ↦ 𝐶) = 𝐵) | ||
| Theorem | fmptff 45276 | Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
| Theorem | fvmptelcdmf 45277 | The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) | ||
| Theorem | fmptdff 45278 | A version of fmptd 7134 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
| Theorem | fvmpt2df 45279 | Deduction version of fvmpt2 7027. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) | ||
| Theorem | rn1st 45280 | The range of a function with a first-countable domain is itself first-countable. This is a variation of 1stcrestlem 23460, with a not-free hypothesis replacing a disjoint variable constraint. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
| Theorem | rnmptssff 45281 | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
| Theorem | rnmptssdff 45282 | The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
| Theorem | fvmpt4d 45283 | Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 15-Feb-2025.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
| Theorem | sub2times 45284 | Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴) | ||
| Theorem | nnxrd 45285 | A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
| Theorem | nnxr 45286 | A natural number is an extended real. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ*) | ||
| Theorem | abssubrp 45287 | The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+) | ||
| Theorem | elfzfzo 45288 | 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 45289 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1)) | ||
| Theorem | abscosbd 45290 | Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1) | ||
| Theorem | mul13d 45291 | Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐶 · (𝐵 · 𝐴))) | ||
| Theorem | negpilt0 45292 | Negative π is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ -π < 0 | ||
| Theorem | dstregt0 45293* | 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 45294 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐷)) = ((𝐴 − 𝐷) + (𝐶 − 𝐵))) | ||
| Theorem | xrlttri5d 45295 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 < 𝐵) | ||
| Theorem | neglt 45296 | The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ ℝ+ → -𝐴 < 𝐴) | ||
| Theorem | zltlesub 45297 | 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 45298 | The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) < 0) | ||
| Theorem | subsub23d 45299 | Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
| Theorem | 2timesgt 45300 | Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝐴 ∈ ℝ+ → 𝐴 < (2 · 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |