![]() |
Metamath
Proof Explorer Theorem List (p. 473 of 478) | < 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-30149) |
![]() (30150-31672) |
![]() (31673-47754) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 0dig2nn0o 47201 | The last bit of an odd integer is 1. (Contributed by AV, 3-Jun-2010.) |
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (0(digit‘2)𝑁) = 1) | ||
Theorem | dig2bits 47202 | The 𝐾 th digit of a nonnegative integer 𝑁 in a binary system is its 𝐾 th bit. (Contributed by AV, 24-May-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) → ((𝐾(digit‘2)𝑁) = 1 ↔ 𝐾 ∈ (bits‘𝑁))) | ||
Theorem | dignn0flhalflem1 47203 | Lemma 1 for dignn0flhalf 47206. (Contributed by AV, 7-Jun-2012.) |
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁)))) | ||
Theorem | dignn0flhalflem2 47204 | Lemma 2 for dignn0flhalf 47206. (Contributed by AV, 7-Jun-2012.) |
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) | ||
Theorem | dignn0ehalf 47205 | The digits of the half of an even nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 3-Jun-2010.) |
⊢ (((𝐴 / 2) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0) → ((𝐼 + 1)(digit‘2)𝐴) = (𝐼(digit‘2)(𝐴 / 2))) | ||
Theorem | dignn0flhalf 47206 | The digits of the rounded half of a nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 7-Jun-2010.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐼 ∈ ℕ0) → ((𝐼 + 1)(digit‘2)𝐴) = (𝐼(digit‘2)(⌊‘(𝐴 / 2)))) | ||
Theorem | nn0sumshdiglemA 47207* | Lemma for nn0sumshdig 47211 (induction step, even multiplier). (Contributed by AV, 3-Jun-2020.) |
⊢ (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) | ||
Theorem | nn0sumshdiglemB 47208* | Lemma for nn0sumshdig 47211 (induction step, odd multiplier). (Contributed by AV, 7-Jun-2020.) |
⊢ (((𝑎 ∈ ℕ ∧ ((𝑎 − 1) / 2) ∈ ℕ0) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b‘𝑥) = 𝑦 → 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) | ||
Theorem | nn0sumshdiglem1 47209* | Lemma 1 for nn0sumshdig 47211 (induction step). (Contributed by AV, 7-Jun-2020.) |
⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) | ||
Theorem | nn0sumshdiglem2 47210* | Lemma 2 for nn0sumshdig 47211. (Contributed by AV, 7-Jun-2020.) |
⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) | ||
Theorem | nn0sumshdig 47211* | A nonnegative integer can be represented as sum of its shifted bits. (Contributed by AV, 7-Jun-2020.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 = Σ𝑘 ∈ (0..^(#b‘𝐴))((𝑘(digit‘2)𝐴) · (2↑𝑘))) | ||
Theorem | nn0mulfsum 47212* | Trivial algorithm to calculate the product of two nonnegative integers 𝑎 and 𝑏 by adding 𝑏 to itself 𝑎 times. (Contributed by AV, 17-May-2020.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (1...𝐴)𝐵) | ||
Theorem | nn0mullong 47213* | Standard algorithm (also known as "long multiplication" or "grade-school multiplication") to calculate the product of two nonnegative integers 𝑎 and 𝑏 by multiplying the multiplicand 𝑏 by each digit of the multiplier 𝑎 and then add up all the properly shifted results. Here, the binary representation of the multiplier 𝑎 is used, i.e., the above mentioned "digits" are 0 or 1. This is a similar result as provided by smumul 16430. (Contributed by AV, 7-Jun-2020.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (0..^(#b‘𝐴))(((𝑘(digit‘2)𝐴) · (2↑𝑘)) · 𝐵)) | ||
According to Wikipedia ("Arity", https://en.wikipedia.org/wiki/Arity, 19-May-2024): "In logic, mathematics, and computer science, arity is the number of arguments or operands taken by a function, operation or relation." N-ary functions are often also called multivariate functions, without indicating the actual number of argumens. See also Wikipedia ("Multivariate functions", 19-May-2024, https://en.wikipedia.org/wiki/Function_(mathematics)#Multivariate_functions ): "A multivariate function, multivariable function, or function of several variables is a function that depends on several arguments. ... Formally, a function of n variables is a function whose domain is a set of n-tuples. For example, multiplication of integers is a function of two variables, or bivariate function, whose domain is the set of all ordered pairs (2-tuples) of integers, and whose codomain is the set of integers. The same is true for every binary operation. Commonly, an n-tuple is denoted enclosed between parentheses, such as in ( 1 , 2 , ... , n ). When using functional notation, one usually omits the parentheses surrounding tuples, writing f ( x1 , ... , xn ) instead of f ( ( x1 , ... , xn ) ). Given n sets X1 , ... , Xn , the set of all n-tuples ( x1 , ... , xn ) such that x1 is element of X1 , ... , xn is element of Xn is called the Cartesian product of X1 , ... , Xn , and denoted X1 X ... X Xn . Therefore, a multivariate function is a function that has a Cartesian product or a proper subset of a Cartesian product as a domain: 𝑓:𝑈⟶𝑌 where where the domain 𝑈 has the form 𝑈 ⊆ ((...((𝑋‘1) × (𝑋‘2)) × ...) × (𝑋‘𝑛))." In the following, n-ary functions are defined as mappings (see df-map 8818) from a finite sequence of arguments, which themselves are defined as mappings from the half-open range of nonnegative integers to the domain of each argument. Furthermore, the definition is restricted to endofunctions, meaning that the domain(s) of the argument(s) is identical with its codomain. This means that the domains of all arguments are identical (in contrast to the definition in Wikipedia, see above: here, we have X1 = X2 = ... = Xn = X). For small n, n-ary functions correspond to "usual" functions with a different number of arguments: - n = 0 (nullary functions): These correspond actually to constants, see 0aryfvalelfv 47223 and mapsn 8878: (𝑋 ↑m {∅}) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 47233 and efmndbas 18748: (𝑋 ↑m 𝑋) - n = 2 (binary functions): These correspond to usual operations on two elements of the same set, also called "binary operation" (according to Wikipedia ("Binary operation", 19-May-2024, https://en.wikipedia.org/wiki/Binary_operation 18748): "In mathematics, a binary operation or dyadic operation is a rule for combining two elements (called operands) to produce another element. More formally, a binary operation is an operation of arity two. More specifically, a binary operation on a set is a binary operation whose two domains and the codomain are the same set." Sometimes also called "closed internal binary operation"), see 2aryenef 47244 and compare with df-clintop 46545: (𝑋 ↑m (𝑋 × 𝑋)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (𝑈↑↑𝑁) (see df-finxp 36203) could have been used to represent multiple arguments. However, this concept is not fully developed yet (it is within a mathbox), and it is currently based on ordinal numbers, e.g., (𝑈↑↑2o), instead of integers, e.g., (𝑈↑↑2), which is not very practical. The definition df-ixp of infinite Cartesian product could also have been used to represent multiple arguments, but this would have been more cumbersome without any additional advantage. naryfvalixp 47217 shows that both definitions are equivalent. | ||
Syntax | cnaryf 47214 | Extend the definition of a class to include the n-ary functions. |
class -aryF | ||
Definition | df-naryf 47215* | Define the n-ary (endo)functions. (Contributed by AV, 11-May-2024.) (Revised by TA and SN, 7-Jun-2024.) |
⊢ -aryF = (𝑛 ∈ ℕ0, 𝑥 ∈ V ↦ (𝑥 ↑m (𝑥 ↑m (0..^𝑛)))) | ||
Theorem | naryfval 47216 | The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m (𝑋 ↑m 𝐼))) | ||
Theorem | naryfvalixp 47217* | The set of the n-ary (endo)functions on a class 𝑋 expressed with the notation of infinite Cartesian products. (Contributed by AV, 19-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m X𝑥 ∈ 𝐼 𝑋)) | ||
Theorem | naryfvalel 47218 | An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m 𝐼)⟶𝑋)) | ||
Theorem | naryrcl 47219 | Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V)) | ||
Theorem | naryfvalelfv 47220 | The value of an n-ary (endo)function on a set 𝑋 is an element of 𝑋. (Contributed by AV, 14-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ ((𝐹 ∈ (𝑁-aryF 𝑋) ∧ 𝐴:𝐼⟶𝑋) → (𝐹‘𝐴) ∈ 𝑋) | ||
Theorem | naryfvalelwrdf 47221* | An n-ary (endo)function on a set 𝑋 expressed as a function over the set of words on 𝑋 of length 𝑛. (Contributed by AV, 4-Jun-2024.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:{𝑤 ∈ Word 𝑋 ∣ (♯‘𝑤) = 𝑁}⟶𝑋)) | ||
Theorem | 0aryfvalel 47222* | A nullary (endo)function on a set 𝑋 is a singleton of an ordered pair with the empty set as first component. A nullary function represents a constant: (𝐹‘∅) = 𝐶 with 𝐶 ∈ 𝑋, see also 0aryfvalelfv 47223. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.) |
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐹 = {〈∅, 𝑥〉})) | ||
Theorem | 0aryfvalelfv 47223* | The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.) |
⊢ (𝐹 ∈ (0-aryF 𝑋) → ∃𝑥 ∈ 𝑋 (𝐹‘∅) = 𝑥) | ||
Theorem | 1aryfvalel 47224 | A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.) |
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0})⟶𝑋)) | ||
Theorem | fv1arycl 47225 | Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.) |
⊢ ((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐺‘{〈0, 𝐴〉}) ∈ 𝑋) | ||
Theorem | 1arympt1 47226* | A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴:𝑋⟶𝑋) → 𝐹 ∈ (1-aryF 𝑋)) | ||
Theorem | 1arympt1fv 47227* | The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{〈0, 𝐵〉}) = (𝐴‘𝐵)) | ||
Theorem | 1arymaptfv 47228* | The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝐹 ∈ (1-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐹‘{〈0, 𝑥〉}))) | ||
Theorem | 1arymaptf 47229* | The mapping of unary (endo)functions is a function into the set of endofunctions. (Contributed by AV, 18-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)⟶(𝑋 ↑m 𝑋)) | ||
Theorem | 1arymaptf1 47230* | The mapping of unary (endo)functions is a one-to-one function into the set of endofunctions. (Contributed by AV, 19-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–1-1→(𝑋 ↑m 𝑋)) | ||
Theorem | 1arymaptfo 47231* | The mapping of unary (endo)functions is a function onto the set of endofunctions. (Contributed by AV, 18-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–onto→(𝑋 ↑m 𝑋)) | ||
Theorem | 1arymaptf1o 47232* | The mapping of unary (endo)functions is a one-to-one function onto the set of endofunctions. (Contributed by AV, 19-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(1-aryF 𝑋)–1-1-onto→(𝑋 ↑m 𝑋)) | ||
Theorem | 1aryenef 47233 | The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.) |
⊢ (1-aryF 𝑋) ≈ (𝑋 ↑m 𝑋) | ||
Theorem | 1aryenefmnd 47234 | The set of unary (endo)functions and the base set of the monoid of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.) |
⊢ (1-aryF 𝑋) ≈ (Base‘(EndoFMnd‘𝑋)) | ||
Theorem | 2aryfvalel 47235 | A binary (endo)function on a set 𝑋. (Contributed by AV, 20-May-2024.) |
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (2-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0, 1})⟶𝑋)) | ||
Theorem | fv2arycl 47236 | Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.) |
⊢ ((𝐺 ∈ (2-aryF 𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐺‘{〈0, 𝐴〉, 〈1, 𝐵〉}) ∈ 𝑋) | ||
Theorem | 2arympt 47237* | A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.) |
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑂:(𝑋 × 𝑋)⟶𝑋) → 𝐹 ∈ (2-aryF 𝑋)) | ||
Theorem | 2arymptfv 47238* | The value of a binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.) |
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{〈0, 𝐴〉, 〈1, 𝐵〉}) = (𝐴𝑂𝐵)) | ||
Theorem | 2arymaptfv 47239* | The value of the mapping of binary (endo)functions. (Contributed by AV, 21-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝐹 ∈ (2-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝐹‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) | ||
Theorem | 2arymaptf 47240* | The mapping of binary (endo)functions is a function into the set of binary operations. (Contributed by AV, 21-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)⟶(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2arymaptf1 47241* | The mapping of binary (endo)functions is a one-to-one function into the set of binary operations. (Contributed by AV, 22-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–1-1→(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2arymaptfo 47242* | The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–onto→(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2arymaptf1o 47243* | The mapping of binary (endo)functions is a one-to-one function onto the set of binary operations. (Contributed by AV, 23-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (2-aryF 𝑋) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉, 〈1, 𝑦〉}))) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐻:(2-aryF 𝑋)–1-1-onto→(𝑋 ↑m (𝑋 × 𝑋))) | ||
Theorem | 2aryenef 47244 | The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.) |
⊢ (2-aryF 𝑋) ≈ (𝑋 ↑m (𝑋 × 𝑋)) | ||
According to Wikipedia ("Ackermann function", 8-May-2024, https://en.wikipedia.org/wiki/Ackermann_function): "In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. ... One common version is the two-argument Ackermann-Péter function developed by Rózsa Péter and Raphael Robinson. Its value grows very rapidly; for example, A(4,2) results in 2^65536-3 [see ackval42 47284)], an integer of 19,729 decimal digits." In the following, the Ackermann function is defined as iterated 1-ary function (also mentioned in Wikipedia), see df-ack 47248, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 47247. As an illustration, we have ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) (see itcoval3 47253). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 47248: ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)). That Definition df-ack 47248 is equivalent to Péter's definition is proven by the following three theorems: ackval0val 47274: ((Ack‘0)‘𝑀) = (𝑀 + 1); ackvalsuc0val 47275: ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1); ackvalsucsucval 47276: ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 47277: 𝐴(0, 0) = 1, 𝐴(0, 1) = 2, 𝐴(0, 2) = 3; ackval1012 47278: 𝐴(1, 0) = 2, 𝐴(1, 1) = 3, 𝐴(1, 3) = 4; ackval2012 47279: 𝐴(2, 0) = 3, 𝐴(2, 1) = 5, 𝐴(2, 3) = 7; ackval3012 47280: 𝐴(3, 0) = 5, 𝐴(3, 1) = ;13, 𝐴(3, 3) = ;29. | ||
Syntax | citco 47245 | Extend the definition of a class to include iterated functions. |
class IterComp | ||
Syntax | cack 47246 | Extend the definition of a class to include the Ackermann function operator. |
class Ack | ||
Definition | df-itco 47247* | Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.) |
⊢ IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)))) | ||
Definition | df-ack 47248* | Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.) |
⊢ Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖))) | ||
Theorem | itcoval 47249* | The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024.) |
⊢ (𝐹 ∈ 𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹)))) | ||
Theorem | itcoval0 47250 | A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.) |
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹)) | ||
Theorem | itcoval1 47251 | A function iterated once. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹) | ||
Theorem | itcoval2 47252 | A function iterated twice. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹)) | ||
Theorem | itcoval3 47253 | A function iterated three times. (Contributed by AV, 2-May-2024.) |
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) | ||
Theorem | itcoval0mpt 47254* | A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛)) | ||
Theorem | itcovalsuc 47255* | The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹 ∘ 𝑔))𝐹)) | ||
Theorem | itcovalsucov 47256 | The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑌 ∈ ℕ0 ∧ ((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐹 ∘ 𝐺)) | ||
Theorem | itcovalendof 47257 | The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴) | ||
Theorem | itcovalpclem1 47258* | Lemma 1 for itcovalpc 47260: induction basis. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0)))) | ||
Theorem | itcovalpclem2 47259* | Lemma 2 for itcovalpc 47260: induction step. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1)))))) | ||
Theorem | itcovalpc 47260* | The value of the function that returns the n-th iterate of the "plus a constant" function with regard to composition. (Contributed by AV, 4-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ ((𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝐼)))) | ||
Theorem | itcovalt2lem2lem1 47261 | Lemma 1 for itcovalt2lem2 47264. (Contributed by AV, 6-May-2024.) |
⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0) | ||
Theorem | itcovalt2lem2lem2 47262 | Lemma 2 for itcovalt2lem2 47264. (Contributed by AV, 7-May-2024.) |
⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) | ||
Theorem | itcovalt2lem1 47263* | Lemma 1 for itcovalt2 47265: induction basis. (Contributed by AV, 5-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))) | ||
Theorem | itcovalt2lem2 47264* | Lemma 2 for itcovalt2 47265: induction step. (Contributed by AV, 7-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) | ||
Theorem | itcovalt2 47265* | The value of the function that returns the n-th iterate of the "times 2 plus a constant" function with regard to composition. (Contributed by AV, 7-May-2024.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ ((𝐼 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶))) | ||
Theorem | ackvalsuc1mpt 47266* | The Ackermann function at a successor of the first argument as a mapping of the second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.) |
⊢ (𝑀 ∈ ℕ0 → (Ack‘(𝑀 + 1)) = (𝑛 ∈ ℕ0 ↦ (((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1))) | ||
Theorem | ackvalsuc1 47267 | The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)) | ||
Theorem | ackval0 47268 | The Ackermann function at 0. (Contributed by AV, 2-May-2024.) |
⊢ (Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)) | ||
Theorem | ackval1 47269 | The Ackermann function at 1. (Contributed by AV, 4-May-2024.) |
⊢ (Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2)) | ||
Theorem | ackval2 47270 | The Ackermann function at 2. (Contributed by AV, 4-May-2024.) |
⊢ (Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3)) | ||
Theorem | ackval3 47271 | The Ackermann function at 3. (Contributed by AV, 7-May-2024.) |
⊢ (Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3)) | ||
Theorem | ackendofnn0 47272 | The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024.) |
⊢ (𝑀 ∈ ℕ0 → (Ack‘𝑀):ℕ0⟶ℕ0) | ||
Theorem | ackfnnn0 47273 | The Ackermann function at any nonnegative integer is a function on the nonnegative integers. (Contributed by AV, 4-May-2024.) (Proof shortened by AV, 8-May-2024.) |
⊢ (𝑀 ∈ ℕ0 → (Ack‘𝑀) Fn ℕ0) | ||
Theorem | ackval0val 47274 | The Ackermann function at 0 (for the first argument). This is the first equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.) |
⊢ (𝑀 ∈ ℕ0 → ((Ack‘0)‘𝑀) = (𝑀 + 1)) | ||
Theorem | ackvalsuc0val 47275 | The Ackermann function at a successor (of the first argument). This is the second equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.) |
⊢ (𝑀 ∈ ℕ0 → ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1)) | ||
Theorem | ackvalsucsucval 47276 | The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁))) | ||
Theorem | ackval0012 47277 | The Ackermann function at (0,0), (0,1), (0,2). (Contributed by AV, 2-May-2024.) |
⊢ 〈((Ack‘0)‘0), ((Ack‘0)‘1), ((Ack‘0)‘2)〉 = 〈1, 2, 3〉 | ||
Theorem | ackval1012 47278 | The Ackermann function at (1,0), (1,1), (1,2). (Contributed by AV, 4-May-2024.) |
⊢ 〈((Ack‘1)‘0), ((Ack‘1)‘1), ((Ack‘1)‘2)〉 = 〈2, 3, 4〉 | ||
Theorem | ackval2012 47279 | The Ackermann function at (2,0), (2,1), (2,2). (Contributed by AV, 4-May-2024.) |
⊢ 〈((Ack‘2)‘0), ((Ack‘2)‘1), ((Ack‘2)‘2)〉 = 〈3, 5, 7〉 | ||
Theorem | ackval3012 47280 | The Ackermann function at (3,0), (3,1), (3,2). (Contributed by AV, 7-May-2024.) |
⊢ 〈((Ack‘3)‘0), ((Ack‘3)‘1), ((Ack‘3)‘2)〉 = 〈5, ;13, ;29〉 | ||
Theorem | ackval40 47281 | The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘0) = ;13 | ||
Theorem | ackval41a 47282 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3) | ||
Theorem | ackval41 47283 | The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘1) = ;;;;65533 | ||
Theorem | ackval42 47284 | The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3) | ||
Theorem | ackval42a 47285 | The Ackermann function at (4,2), expressed with powers of 2. (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘4)‘2) = ((2↑(2↑(2↑(2↑2)))) − 3) | ||
Theorem | ackval50 47286 | The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.) |
⊢ ((Ack‘5)‘0) = ;;;;65533 | ||
Theorem | fv1prop 47287 | The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023.) |
⊢ (𝐴 ∈ 𝑉 → ({〈1, 𝐴〉, 〈2, 𝐵〉}‘1) = 𝐴) | ||
Theorem | fv2prop 47288 | The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023.) |
⊢ (𝐵 ∈ 𝑉 → ({〈1, 𝐴〉, 〈2, 𝐵〉}‘2) = 𝐵) | ||
Theorem | submuladdmuld 47289 | Transformation of a sum of a product of a difference and a product with the subtrahend of the difference. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐵) · 𝐶) + (𝐵 · 𝐷)) = ((𝐴 · 𝐶) + (𝐵 · (𝐷 − 𝐶)))) | ||
Theorem | affinecomb1 47290* | Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) & ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵)) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹))) | ||
Theorem | affinecomb2 47291* | Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ℝ) & ⊢ (𝜑 → 𝐺 ∈ ℝ) ⇒ ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺))))) | ||
Theorem | affineid 47292 | Identity of an affine combination. (Contributed by AV, 2-Feb-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑇 ∈ ℂ) ⇒ ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴) | ||
Theorem | 1subrec1sub 47293 | Subtract the reciprocal of 1 minus a number from 1 results in the number divided by the number minus 1. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 1) → (1 − (1 / (1 − 𝐴))) = (𝐴 / (𝐴 − 1))) | ||
Theorem | resum2sqcl 47294 | The sum of two squares of real numbers is a real number. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ) | ||
Theorem | resum2sqgt0 47295 | The sum of the square of a nonzero real number and the square of another real number is greater than zero. (Contributed by AV, 7-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 0 < 𝑄) | ||
Theorem | resum2sqrp 47296 | The sum of the square of a nonzero real number and the square of another real number is a positive real number. (Contributed by AV, 2-May-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 𝑄 ∈ ℝ+) | ||
Theorem | resum2sqorgt0 47297 | The sum of the square of two real numbers is greater than zero if at least one of the real numbers is nonzero. (Contributed by AV, 26-Feb-2023.) |
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < 𝑄) | ||
Theorem | reorelicc 47298 | Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 < 𝐴 ∨ 𝐶 ∈ (𝐴[,]𝐵) ∨ 𝐵 < 𝐶)) | ||
Theorem | rrx2pxel 47299 | The x-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) | ||
Theorem | rrx2pyel 47300 | The y-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝐼 = {1, 2} & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |