| Metamath
Proof Explorer Theorem List (p. 486 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 | nnpw2blen 48501 | A positive integer is between 2 to the power of its binary length minus 1 and 2 to the power of its binary length. (Contributed by AV, 31-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → ((2↑((#b‘𝑁) − 1)) ≤ 𝑁 ∧ 𝑁 < (2↑(#b‘𝑁)))) | ||
| Theorem | nnpw2blenfzo 48502 | A positive integer is between 2 to the power of the binary length of the integer minus 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ((2↑((#b‘𝑁) − 1))..^(2↑(#b‘𝑁)))) | ||
| Theorem | nnpw2blenfzo2 48503 | A positive integer is either 2 to the power of the binary length of the integer minus 1, or between 2 to the power of the binary length of the integer minus 1, increased by 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → (𝑁 = (2↑((#b‘𝑁) − 1)) ∨ 𝑁 ∈ (((2↑((#b‘𝑁) − 1)) + 1)..^(2↑(#b‘𝑁))))) | ||
| Theorem | nnpw2pmod 48504 | Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → 𝑁 = ((2↑((#b‘𝑁) − 1)) + (𝑁 mod (2↑((#b‘𝑁) − 1))))) | ||
| Theorem | blen1 48505 | The binary length of 1. (Contributed by AV, 21-May-2020.) |
| ⊢ (#b‘1) = 1 | ||
| Theorem | blen2 48506 | The binary length of 2. (Contributed by AV, 21-May-2020.) |
| ⊢ (#b‘2) = 2 | ||
| Theorem | nnpw2p 48507* | Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟)) | ||
| Theorem | nnpw2pb 48508* | A number is a positive integer iff it can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.) |
| ⊢ (𝑁 ∈ ℕ ↔ ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟)) | ||
| Theorem | blen1b 48509 | The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → ((#b‘𝑁) = 1 ↔ (𝑁 = 0 ∨ 𝑁 = 1))) | ||
| Theorem | blennnt2 48510 | The binary length of a positive integer, doubled and increased by 1, is the binary length of the integer plus 1. (Contributed by AV, 30-May-2010.) |
| ⊢ (𝑁 ∈ ℕ → (#b‘(2 · 𝑁)) = ((#b‘𝑁) + 1)) | ||
| Theorem | nnolog2flm1 48511 | The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ) → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb (𝑁 − 1)))) | ||
| Theorem | blennn0em1 48512 | The binary length of the half of an even positive integer is the binary length of the integer minus 1. (Contributed by AV, 30-May-2010.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ0) → (#b‘(𝑁 / 2)) = ((#b‘𝑁) − 1)) | ||
| Theorem | blennngt2o2 48513 | The binary length of an odd integer greater than 1 is the binary length of the half of the integer decreased by 1, increased by 1. (Contributed by AV, 3-Jun-2020.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (#b‘𝑁) = ((#b‘((𝑁 − 1) / 2)) + 1)) | ||
| Theorem | blengt1fldiv2p1 48514 | The binary length of an integer greater than 1 is the binary length of the integer divided by 2, increased by one. (Contributed by AV, 3-Jun-2020.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) → (#b‘𝑁) = ((#b‘(⌊‘(𝑁 / 2))) + 1)) | ||
| Theorem | blennn0e2 48515 | The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ0) → (#b‘𝑁) = ((#b‘(𝑁 / 2)) + 1)) | ||
Generalization of df-bits 16459. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 48535: if 𝐾 and 𝑁 are nonnegative integers, then ((𝐾(digit‘2)𝑁) = 1 ↔ 𝐾 ∈ (bits‘𝑁)). | ||
| Syntax | cdig 48516 | Extend class notation with the class of the digit extraction operation. |
| class digit | ||
| Definition | df-dig 48517* | Definition of an operation to obtain the 𝑘 th digit of a nonnegative real number 𝑟 in the positional system with base 𝑏. 𝑘 = − 1 corresponds to the first digit of the fractional part (for 𝑏 = 10 the first digit after the decimal point), 𝑘 = 0 corresponds to the last digit of the integer part (for 𝑏 = 10 the first digit before the decimal point). See also digit1 14276. Examples (not formal): ( 234.567 ( digit ` 10 ) 0 ) = 4; ( 2.567 ( digit ` 10 ) -2 ) = 6; ( 2345.67 ( digit ` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020.) |
| ⊢ digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏))) | ||
| Theorem | digfval 48518* | Operation to obtain the 𝑘 th digit of a nonnegative real number 𝑟 in the positional system with base 𝐵. (Contributed by AV, 23-May-2020.) |
| ⊢ (𝐵 ∈ ℕ → (digit‘𝐵) = (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝐵↑-𝑘) · 𝑟)) mod 𝐵))) | ||
| Theorem | digval 48519 | The 𝐾 th digit of a nonnegative real number 𝑅 in the positional system with base 𝐵. (Contributed by AV, 23-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ (0[,)+∞)) → (𝐾(digit‘𝐵)𝑅) = ((⌊‘((𝐵↑-𝐾) · 𝑅)) mod 𝐵)) | ||
| Theorem | digvalnn0 48520 | The 𝐾 th digit of a nonnegative real number 𝑅 in the positional system with base 𝐵 is a nonnegative integer. (Contributed by AV, 28-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ (0[,)+∞)) → (𝐾(digit‘𝐵)𝑅) ∈ ℕ0) | ||
| Theorem | nn0digval 48521 | The 𝐾 th digit of a nonnegative real number 𝑅 in the positional system with base 𝐵. (Contributed by AV, 23-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ (0[,)+∞)) → (𝐾(digit‘𝐵)𝑅) = ((⌊‘(𝑅 / (𝐵↑𝐾))) mod 𝐵)) | ||
| Theorem | dignn0fr 48522 | The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖ ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = 0) | ||
| Theorem | dignn0ldlem 48523 | Lemma for dignnld 48524. (Contributed by AV, 25-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → 𝑁 < (𝐵↑𝐾)) | ||
| Theorem | dignnld 48524 | The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → (𝐾(digit‘𝐵)𝑁) = 0) | ||
| Theorem | dig2nn0ld 48525 | The leading digits of a positive integer in a binary system are 0. (Contributed by AV, 25-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘(#b‘𝑁))) → (𝐾(digit‘2)𝑁) = 0) | ||
| Theorem | dig2nn1st 48526 | The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → (((#b‘𝑁) − 1)(digit‘2)𝑁) = 1) | ||
| Theorem | dig0 48527 | All digits of 0 are 0. (Contributed by AV, 24-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)0) = 0) | ||
| Theorem | digexp 48528 | The 𝐾 th digit of a power to the base is either 1 or 0. (Contributed by AV, 24-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)(𝐵↑𝑁)) = if(𝐾 = 𝑁, 1, 0)) | ||
| Theorem | dig1 48529 | All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)1) = if(𝐾 = 0, 1, 0)) | ||
| Theorem | 0dig1 48530 | The 0 th digit of 1 is 1 in any positional system. (Contributed by AV, 28-May-2020.) |
| ⊢ (𝐵 ∈ (ℤ≥‘2) → (0(digit‘𝐵)1) = 1) | ||
| Theorem | 0dig2pr01 48531 | The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.) |
| ⊢ (𝑁 ∈ {0, 1} → (0(digit‘2)𝑁) = 𝑁) | ||
| Theorem | dig2nn0 48532 | A digit of a nonnegative integer 𝑁 in a binary system is either 0 or 1. (Contributed by AV, 24-May-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘2)𝑁) ∈ {0, 1}) | ||
| Theorem | 0dig2nn0e 48533 | The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → (0(digit‘2)𝑁) = 0) | ||
| Theorem | 0dig2nn0o 48534 | 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 48535 | 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 48536 | Lemma 1 for dignn0flhalf 48539. (Contributed by AV, 7-Jun-2012.) |
| ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁)))) | ||
| Theorem | dignn0flhalflem2 48537 | Lemma 2 for dignn0flhalf 48539. (Contributed by AV, 7-Jun-2012.) |
| ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) | ||
| Theorem | dignn0ehalf 48538 | 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 48539 | 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 48540* | Lemma for nn0sumshdig 48544 (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 48541* | Lemma for nn0sumshdig 48544 (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 48542* | Lemma 1 for nn0sumshdig 48544 (induction step). (Contributed by AV, 7-Jun-2020.) |
| ⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) | ||
| Theorem | nn0sumshdiglem2 48543* | Lemma 2 for nn0sumshdig 48544. (Contributed by AV, 7-Jun-2020.) |
| ⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) | ||
| Theorem | nn0sumshdig 48544* | 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 48545* | 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 48546* | 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 16530. (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 arguments. 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 8868) 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 48556 and mapsn 8928: (𝑋 ↑m {∅}) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 48566 and efmndbas 18884: (𝑋 ↑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 18884): "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 48577 and compare with df-clintop 48116: (𝑋 ↑m (𝑋 × 𝑋)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (𝑈↑↑𝑁) (see df-finxp 37385) 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 48550 shows that both definitions are equivalent. | ||
| Syntax | cnaryf 48547 | Extend the definition of a class to include the n-ary functions. |
| class -aryF | ||
| Definition | df-naryf 48548* | 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 48549 | The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.) |
| ⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m (𝑋 ↑m 𝐼))) | ||
| Theorem | naryfvalixp 48550* | 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 48551 | An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.) |
| ⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m 𝐼)⟶𝑋)) | ||
| Theorem | naryrcl 48552 | Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.) |
| ⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V)) | ||
| Theorem | naryfvalelfv 48553 | 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 48554* | 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 48555* | 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 48556. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐹 = {〈∅, 𝑥〉})) | ||
| Theorem | 0aryfvalelfv 48556* | The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.) |
| ⊢ (𝐹 ∈ (0-aryF 𝑋) → ∃𝑥 ∈ 𝑋 (𝐹‘∅) = 𝑥) | ||
| Theorem | 1aryfvalel 48557 | A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0})⟶𝑋)) | ||
| Theorem | fv1arycl 48558 | Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.) |
| ⊢ ((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐺‘{〈0, 𝐴〉}) ∈ 𝑋) | ||
| Theorem | 1arympt1 48559* | A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴:𝑋⟶𝑋) → 𝐹 ∈ (1-aryF 𝑋)) | ||
| Theorem | 1arympt1fv 48560* | The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{〈0, 𝐵〉}) = (𝐴‘𝐵)) | ||
| Theorem | 1arymaptfv 48561* | The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.) |
| ⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝐹 ∈ (1-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐹‘{〈0, 𝑥〉}))) | ||
| Theorem | 1arymaptf 48562* | 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 48563* | 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 48564* | 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 48565* | 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 48566 | The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.) |
| ⊢ (1-aryF 𝑋) ≈ (𝑋 ↑m 𝑋) | ||
| Theorem | 1aryenefmnd 48567 | 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 48568 | A binary (endo)function on a set 𝑋. (Contributed by AV, 20-May-2024.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (2-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0, 1})⟶𝑋)) | ||
| Theorem | fv2arycl 48569 | Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.) |
| ⊢ ((𝐺 ∈ (2-aryF 𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐺‘{〈0, 𝐴〉, 〈1, 𝐵〉}) ∈ 𝑋) | ||
| Theorem | 2arympt 48570* | A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.) |
| ⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑂:(𝑋 × 𝑋)⟶𝑋) → 𝐹 ∈ (2-aryF 𝑋)) | ||
| Theorem | 2arymptfv 48571* | 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 48572* | 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 48573* | 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 48574* | 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 48575* | 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 48576* | 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 48577 | 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 48617)], 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 48581, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 48580. As an illustration, we have ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) (see itcoval3 48586). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 48581: ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)). That Definition df-ack 48581 is equivalent to Péter's definition is proven by the following three theorems: ackval0val 48607: ((Ack‘0)‘𝑀) = (𝑀 + 1); ackvalsuc0val 48608: ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1); ackvalsucsucval 48609: ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 48610: 𝐴(0, 0) = 1, 𝐴(0, 1) = 2, 𝐴(0, 2) = 3; ackval1012 48611: 𝐴(1, 0) = 2, 𝐴(1, 1) = 3, 𝐴(1, 3) = 4; ackval2012 48612: 𝐴(2, 0) = 3, 𝐴(2, 1) = 5, 𝐴(2, 3) = 7; ackval3012 48613: 𝐴(3, 0) = 5, 𝐴(3, 1) = ;13, 𝐴(3, 3) = ;29. | ||
| Syntax | citco 48578 | Extend the definition of a class to include iterated functions. |
| class IterComp | ||
| Syntax | cack 48579 | Extend the definition of a class to include the Ackermann function operator. |
| class Ack | ||
| Definition | df-itco 48580* | 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 48581* | 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 48582* | 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 48583 | A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.) |
| ⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹)) | ||
| Theorem | itcoval1 48584 | A function iterated once. (Contributed by AV, 2-May-2024.) |
| ⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹) | ||
| Theorem | itcoval2 48585 | A function iterated twice. (Contributed by AV, 2-May-2024.) |
| ⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹)) | ||
| Theorem | itcoval3 48586 | A function iterated three times. (Contributed by AV, 2-May-2024.) |
| ⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) | ||
| Theorem | itcoval0mpt 48587* | A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.) |
| ⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛)) | ||
| Theorem | itcovalsuc 48588* | 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 48589 | 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 48590 | The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴) | ||
| Theorem | itcovalpclem1 48591* | Lemma 1 for itcovalpc 48593: induction basis. (Contributed by AV, 4-May-2024.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0)))) | ||
| Theorem | itcovalpclem2 48592* | Lemma 2 for itcovalpc 48593: induction step. (Contributed by AV, 4-May-2024.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1)))))) | ||
| Theorem | itcovalpc 48593* | 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 48594 | Lemma 1 for itcovalt2lem2 48597. (Contributed by AV, 6-May-2024.) |
| ⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0) | ||
| Theorem | itcovalt2lem2lem2 48595 | Lemma 2 for itcovalt2lem2 48597. (Contributed by AV, 7-May-2024.) |
| ⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶)) | ||
| Theorem | itcovalt2lem1 48596* | Lemma 1 for itcovalt2 48598: induction basis. (Contributed by AV, 5-May-2024.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶))) | ||
| Theorem | itcovalt2lem2 48597* | Lemma 2 for itcovalt2 48598: induction step. (Contributed by AV, 7-May-2024.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶)) ⇒ ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶)))) | ||
| Theorem | itcovalt2 48598* | 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 48599* | 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 48600 | 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)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |