![]() |
Metamath
Proof Explorer Theorem List (p. 404 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | disjf1o 40301* | A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅} & ⊢ 𝐷 = (ran 𝐹 ∖ {∅}) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→𝐷) | ||
Theorem | fompt 40302* | Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = 𝐶)) | ||
Theorem | disjinfi 40303* | Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶 (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Fin) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin) | ||
Theorem | fvovco 40304 | Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊)) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1st ‘(𝐹‘𝑌))𝑂(2nd ‘(𝐹‘𝑌)))) | ||
Theorem | ssnnf1octb 40305* | There exists a bijection between a subset of ℕ and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴)) | ||
Theorem | mapdm0OLD 40306 | Obsolete version of mapdm0 8155 as of 3-Dec-2021. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ∅) = {∅}) | ||
Theorem | nnf1oxpnn 40307 | There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ∃𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ) | ||
Theorem | rnmptssd 40308* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | projf1o 40309* | 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 40310 | Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑𝑚 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐴) | ||
Theorem | fvixp2 40311* | Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | ||
Theorem | fidmfisupp 40312 | A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | choicefi 40313* | 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 40314 | The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴 ↑𝑚 𝐵) ≼ ω) | ||
Theorem | cnmetcoval 40315 | 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 40316* | Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐺:𝐶⟶𝐷) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑥)))) | ||
Theorem | elmapsnd 40317 | Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹 Fn {𝐴}) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑𝑚 {𝐴})) | ||
Theorem | mapss2 40318 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))) | ||
Theorem | fsneq 40319 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴))) | ||
Theorem | difmap 40320 | Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑𝑚 𝐶) ⊆ ((𝐴 ↑𝑚 𝐶) ∖ (𝐵 ↑𝑚 𝐶))) | ||
Theorem | unirnmap 40321 | Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 𝐴)) ⇒ ⊢ (𝜑 → 𝑋 ⊆ (ran ∪ 𝑋 ↑𝑚 𝐴)) | ||
Theorem | inmap 40322 | Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑𝑚 𝐶) ∩ (𝐵 ↑𝑚 𝐶)) = ((𝐴 ∩ 𝐵) ↑𝑚 𝐶)) | ||
Theorem | fcoss 40323 | Composition of two mappings. Similar to fco 6308, but with a weaker condition on the domain of 𝐹. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐺:𝐷⟶𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐷⟶𝐵) | ||
Theorem | fsneqrn 40324 | Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐵 = {𝐴} & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐺 Fn 𝐵) ⇒ ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺)) | ||
Theorem | difmapsn 40325 | Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ((𝐴 ↑𝑚 {𝐶}) ∖ (𝐵 ↑𝑚 {𝐶})) = ((𝐴 ∖ 𝐵) ↑𝑚 {𝐶})) | ||
Theorem | mapssbi 40326 | Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) & ⊢ (𝜑 → 𝐶 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))) | ||
Theorem | unirnmapsn 40327 | Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝐶 = {𝐴} & ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑𝑚 𝐶)) ⇒ ⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑𝑚 𝐶)) | ||
Theorem | iunmapss 40328* | The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑𝑚 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐶)) | ||
Theorem | ssmapsn 40329* | A subset 𝐶 of a set exponentiation to a singleton, is its projection 𝐷 exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑓𝐷 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑𝑚 {𝐴})) & ⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓 ⇒ ⊢ (𝜑 → 𝐶 = (𝐷 ↑𝑚 {𝐴})) | ||
Theorem | iunmapsn 40330* | 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.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑𝑚 {𝐶}) = (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 {𝐶})) | ||
Theorem | absfico 40331 | Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ abs:ℂ⟶(0[,)+∞) | ||
Theorem | icof 40332 | 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 | rnmpt0 40333* | The range of a function in maps-to notation is empty if and only if its domain is empty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → (ran 𝐹 = ∅ ↔ 𝐴 = ∅)) | ||
Theorem | rnmptn0 40334* | The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ran 𝐹 ≠ ∅) | ||
Theorem | elpmrn 40335 | The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → ran 𝐹 ⊆ 𝐴) | ||
Theorem | imaexi 40336 | The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ (𝐴 “ 𝐵) ∈ V | ||
Theorem | axccdom 40337* | Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ≼ ω) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧 ∈ 𝑋 (𝑓‘𝑧) ∈ 𝑧)) | ||
Theorem | dmmptdf 40338* | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
Theorem | elpmi2 40339 | The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → dom 𝐹 ⊆ 𝐵) | ||
Theorem | dmrelrnrel 40340* | A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵)𝑆(𝐹‘𝐶)) | ||
Theorem | fco3 40341 | Functionality of a composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):(◡𝐺 “ dom 𝐹)⟶ran 𝐹) | ||
Theorem | fvcod 40342 | Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ∈ dom 𝐺) & ⊢ 𝐻 = (𝐹 ∘ 𝐺) ⇒ ⊢ (𝜑 → (𝐻‘𝐴) = (𝐹‘(𝐺‘𝐴))) | ||
Theorem | fcod 40343 | Composition of two mappings. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶) | ||
Theorem | freld 40344 | A mapping is a relation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → Rel 𝐹) | ||
Theorem | elrnmpt2id 40345* | Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) ∈ ran 𝐹) | ||
Theorem | axccd 40346* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ≈ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
Theorem | axccd2 40347* | An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ≼ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥) | ||
Theorem | funimassd 40348* | Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Fun 𝐹) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ 𝐵) | ||
Theorem | fimassd 40349 | The image of a class is a subset of its codomain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐹 “ 𝑋) ⊆ 𝐵) | ||
Theorem | feqresmptf 40350* | Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) | ||
Theorem | fnmptd 40351* | The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 Fn 𝐴) | ||
Theorem | elrnmpt1d 40352 | Elementhood in an image set. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝑥 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐵 ∈ ran 𝐹) | ||
Theorem | dmresss 40353 | The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ dom (𝐴 ↾ 𝐵) ⊆ dom 𝐴 | ||
Theorem | mptima 40354* | Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) | ||
Theorem | dmmptssf 40355 | The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | dmmptdf2 40356 | The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐴 = 𝐵) | ||
Theorem | dmuz 40357 | Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ dom ℤ≥ = ℤ | ||
Theorem | fmptd2f 40358* | Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) | ||
Theorem | mpteq1df 40359 | An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | mptexf 40360 | If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 6756. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V | ||
Theorem | fvmpt4 40361* | Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | ||
Theorem | fmptf 40362* | Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | resimass 40363 | The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝐴 ↾ 𝐵) “ 𝐶) ⊆ (𝐴 “ 𝐶) | ||
Theorem | mptssid 40364 | The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐵) | ||
Theorem | mptfnd 40365 | 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 40366 | An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | rnmptlb 40367* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧) | ||
Theorem | rnmptbddlem 40368* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
Theorem | rnmptbdd 40369* | Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦) | ||
Theorem | mptima2 40370* | Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ 𝐶 ↦ 𝐵)) | ||
Theorem | fvelimad 40371* | Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐹 “ 𝐵)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑥) = 𝐶) | ||
Theorem | funimaeq 40372* | 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 40373* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | rnmptbd2lem 40374* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
Theorem | rnmptbd2 40375* | Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)) | ||
Theorem | infnsuprnmpt 40376* | 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 40377* | 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 40378* | 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 40379* | 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 40380* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐶 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶) | ||
Theorem | rnmptbdlem 40381* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
Theorem | rnmptbd 40382* | Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)) | ||
Theorem | rnmptss2 40383* | 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 40384* | The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐷) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐷)𝐶 = 𝐵)) | ||
Theorem | ralrnmpt3 40385* | A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | fvelima2 40386* | Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (𝐹 “ 𝐶)) → ∃𝑥 ∈ (𝐴 ∩ 𝐶)(𝐹‘𝑥) = 𝐵) | ||
Theorem | funresd 40387 | A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ (𝜑 → Fun (𝐹 ↾ 𝐴)) | ||
Theorem | rnmptssbi 40388* | The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (ran 𝐹 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)) | ||
Theorem | fnfvima2 40389 | Given an element of the preimage, its function value is in the image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐶)) | ||
Theorem | fnfvelrnd 40390 | A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐵) ∈ ran 𝐹) | ||
Theorem | imass2d 40391 | Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | imassmpt 40392* | Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹 “ 𝐶) ⊆ 𝐷 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ 𝐷)) | ||
Theorem | fnssresd 40393 | Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐵) Fn 𝐵) | ||
Theorem | fpmd 40394 | A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | fconst7 40395* | An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐹 & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | sub2times 40396 | Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴) | ||
Theorem | abssubrp 40397 | The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+) | ||
Theorem | elfzfzo 40398 | 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 40399 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1)) | ||
Theorem | abscosbd 40400 | Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |