P. 487 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48601-48700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dig0 48601	All digits of 0 are 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)0) = 0)
Theorem	digexp 48602	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 48603	All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)1) = if(𝐾 = 0, 1, 0))
Theorem	0dig1 48604	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 48605	The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.)
⊢ (𝑁 ∈ {0, 1} → (0(digit‘2)𝑁) = 𝑁)
Theorem	dig2nn0 48606	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 48607	The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → (0(digit‘2)𝑁) = 0)
Theorem	0dig2nn0o 48608	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 48609	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‘𝑁)))
21.48.21.10  Nonnegative integer as sum of its shifted digits
Theorem	dignn0flhalflem1 48610	Lemma 1 for dignn0flhalf 48613. (Contributed by AV, 7-Jun-2012.)
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁))))
Theorem	dignn0flhalflem2 48611	Lemma 2 for dignn0flhalf 48613. (Contributed by AV, 7-Jun-2012.)
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))))
Theorem	dignn0ehalf 48612	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 48613	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 48614*	Lemma for nn0sumshdig 48618 (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 48615*	Lemma for nn0sumshdig 48618 (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 48616*	Lemma 1 for nn0sumshdig 48618 (induction step). (Contributed by AV, 7-Jun-2020.)
⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Theorem	nn0sumshdiglem2 48617*	Lemma 2 for nn0sumshdig 48618. (Contributed by AV, 7-Jun-2020.)
⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
Theorem	nn0sumshdig 48618*	A nonnegative integer can be represented as sum of its shifted bits. (Contributed by AV, 7-Jun-2020.)
⊢ (𝐴 ∈ ℕ0 → 𝐴 = Σ𝑘 ∈ (0..^(#b‘𝐴))((𝑘(digit‘2)𝐴) · (2↑𝑘)))
21.48.21.11  Algorithms for the multiplication of nonnegative integers
Theorem	nn0mulfsum 48619*	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 48620*	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 16404. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (0..^(#b‘𝐴))(((𝑘(digit‘2)𝐴) · (2↑𝑘)) · 𝐵))
21.48.21.12  N-ary functions 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 an element of X1 , ... , xn is an 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 8755) 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 48630 and mapsn 8815: (𝑋 ↑m {∅}) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 48640 and efmndbas 18745: (𝑋 ↑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 18745): "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 48651 and compare with df-clintop 48194: (𝑋 ↑m (𝑋 × 𝑋)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (𝑈↑↑𝑁) (see df-finxp 37368) 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 48624 shows that both definitions are equivalent.
Syntax	cnaryf 48621	Extend the definition of a class to include the n-ary functions.
class -aryF
Definition	df-naryf 48622*	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 48623	The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m (𝑋 ↑m 𝐼)))
Theorem	naryfvalixp 48624*	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 48625	An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m 𝐼)⟶𝑋))
Theorem	naryrcl 48626	Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V))
Theorem	naryfvalelfv 48627	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 48628*	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 48629*	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 48630. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐹 = {⟨∅, 𝑥⟩}))
Theorem	0aryfvalelfv 48630*	The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.)
⊢ (𝐹 ∈ (0-aryF 𝑋) → ∃𝑥 ∈ 𝑋 (𝐹‘∅) = 𝑥)
Theorem	1aryfvalel 48631	A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0})⟶𝑋))
Theorem	fv1arycl 48632	Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.)
⊢ ((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐺‘{⟨0, 𝐴⟩}) ∈ 𝑋)
Theorem	1arympt1 48633*	A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴:𝑋⟶𝑋) → 𝐹 ∈ (1-aryF 𝑋))
Theorem	1arympt1fv 48634*	The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{⟨0, 𝐵⟩}) = (𝐴‘𝐵))
Theorem	1arymaptfv 48635*	The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.)
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{⟨0, 𝑥⟩})))    ⇒   ⊢ (𝐹 ∈ (1-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐹‘{⟨0, 𝑥⟩})))
Theorem	1arymaptf 48636*	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 48637*	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 48638*	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 48639*	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 48640	The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.)
⊢ (1-aryF 𝑋) ≈ (𝑋 ↑m 𝑋)
Theorem	1aryenefmnd 48641	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 48642	A binary (endo)function on a set 𝑋. (Contributed by AV, 20-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (2-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0, 1})⟶𝑋))
Theorem	fv2arycl 48643	Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.)
⊢ ((𝐺 ∈ (2-aryF 𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐺‘{⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) ∈ 𝑋)
Theorem	2arympt 48644*	A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑂:(𝑋 × 𝑋)⟶𝑋) → 𝐹 ∈ (2-aryF 𝑋))
Theorem	2arymptfv 48645*	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 48646*	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 48647*	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 48648*	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 48649*	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 48650*	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 48651	The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.)
⊢ (2-aryF 𝑋) ≈ (𝑋 ↑m (𝑋 × 𝑋))
21.48.21.13  The Ackermann function 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 48691)], 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 48655, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 48654. As an illustration, we have ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) (see itcoval3 48660). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 48655: ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)). That Definition df-ack 48655 is equivalent to Péter's definition is proven by the following three theorems: ackval0val 48681: ((Ack‘0)‘𝑀) = (𝑀 + 1); ackvalsuc0val 48682: ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1); ackvalsucsucval 48683: ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 48684: 𝐴(0, 0) = 1, 𝐴(0, 1) = 2, 𝐴(0, 2) = 3; ackval1012 48685: 𝐴(1, 0) = 2, 𝐴(1, 1) = 3, 𝐴(1, 3) = 4; ackval2012 48686: 𝐴(2, 0) = 3, 𝐴(2, 1) = 5, 𝐴(2, 3) = 7; ackval3012 48687: 𝐴(3, 0) = 5, 𝐴(3, 1) = ;13, 𝐴(3, 3) = ;29.
Syntax	citco 48652	Extend the definition of a class to include iterated functions.
class IterComp
Syntax	cack 48653	Extend the definition of a class to include the Ackermann function operator.
class Ack
Definition	df-itco 48654*	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 48655*	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 48656*	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 48657	A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.)
⊢ (𝐹 ∈ 𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹))
Theorem	itcoval1 48658	A function iterated once. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘1) = 𝐹)
Theorem	itcoval2 48659	A function iterated twice. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘2) = (𝐹 ∘ 𝐹))
Theorem	itcoval3 48660	A function iterated three times. (Contributed by AV, 2-May-2024.)
⊢ ((Rel 𝐹 ∧ 𝐹 ∈ 𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹)))
Theorem	itcoval0mpt 48661*	A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑊) → ((IterComp‘𝐹)‘0) = (𝑛 ∈ 𝐴 ↦ 𝑛))
Theorem	itcovalsuc 48662*	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 48663	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 48664	The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴⟶𝐴)
Theorem	itcovalpclem1 48665*	Lemma 1 for itcovalpc 48667: induction basis. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0))))
Theorem	itcovalpclem2 48666*	Lemma 2 for itcovalpc 48667: induction step. (Contributed by AV, 4-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))    ⇒   ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))))
Theorem	itcovalpc 48667*	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 48668	Lemma 1 for itcovalt2lem2 48671. (Contributed by AV, 6-May-2024.)
⊢ (((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0)
Theorem	itcovalt2lem2lem2 48669	Lemma 2 for itcovalt2lem2 48671. (Contributed by AV, 7-May-2024.)
⊢ (((𝑌 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶))
Theorem	itcovalt2lem1 48670*	Lemma 1 for itcovalt2 48672: induction basis. (Contributed by AV, 5-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶)))
Theorem	itcovalt2lem2 48671*	Lemma 2 for itcovalt2 48672: induction step. (Contributed by AV, 7-May-2024.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))    ⇒   ⊢ ((𝑦 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))
Theorem	itcovalt2 48672*	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 48673*	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 48674	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 48675	The Ackermann function at 0. (Contributed by AV, 2-May-2024.)
⊢ (Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
Theorem	ackval1 48676	The Ackermann function at 1. (Contributed by AV, 4-May-2024.)
⊢ (Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2))
Theorem	ackval2 48677	The Ackermann function at 2. (Contributed by AV, 4-May-2024.)
⊢ (Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3))
Theorem	ackval3 48678	The Ackermann function at 3. (Contributed by AV, 7-May-2024.)
⊢ (Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3))
Theorem	ackendofnn0 48679	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 48680	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 48681	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 48682	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 48683	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 48684	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 48685	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 48686	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 48687	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 48688	The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘0) = ;13
Theorem	ackval41a 48689	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ((2↑;16) − 3)
Theorem	ackval41 48690	The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘1) = ;;;;65533
Theorem	ackval42 48691	The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘4)‘2) = ((2↑;;;;65536) − 3)
Theorem	ackval42a 48692	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 48693	The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.)
⊢ ((Ack‘5)‘0) = ;;;;65533
21.48.22  Elementary geometry (extension)
21.48.22.1  Auxiliary theorems
Theorem	fv1prop 48694	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 48695	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 48696	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 48697*	Combination of two real affine combinations, one class variable resolved. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    &   ⊢ 𝑆 = ((𝐺 − 𝐹) / (𝐶 − 𝐵))    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ 𝐸 = ((𝑆 · (𝐴 − 𝐵)) + 𝐹)))
Theorem	affinecomb2 48698*	Combination of two real affine combinations, presented without fraction. (Contributed by AV, 22-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∃𝑡 ∈ ℝ (𝐴 = (((1 − 𝑡) · 𝐵) + (𝑡 · 𝐶)) ∧ 𝐸 = (((1 − 𝑡) · 𝐹) + (𝑡 · 𝐺))) ↔ ((𝐶 − 𝐵) · 𝐸) = (((𝐺 − 𝐹) · 𝐴) + ((𝐹 · 𝐶) − (𝐵 · 𝐺)))))
Theorem	affineid 48699	Identity of an affine combination. (Contributed by AV, 2-Feb-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐴)) = 𝐴)
Theorem	1subrec1sub 48700	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)))