P. 495 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49401-49500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	relogbdivb 49401	The logarithm of the quotient of a positive real number and the base is the logarithm of the number minus 1. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (𝐴 / 𝐵)) = ((𝐵 logb 𝐴) − 1))
Theorem	logbge0b 49402	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (0 ≤ (𝐵 logb 𝑋) ↔ 1 ≤ 𝑋))
Theorem	logblt1b 49403	The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → ((𝐵 logb 𝑋) < 1 ↔ 𝑋 < 𝐵))
21.50.22.7  The binary logarithm If the binary logarithm is used more often, a separate symbol/definition could be provided for it, e.g., log2 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (2 logb 𝑋)). Then we can write "( log2 ` x )" (analogous to (log𝑥) for the natural logarithm) instead of (2 logb 𝑥).
Theorem	fldivexpfllog2 49404	The floor of a positive real number divided by 2 to the power of the floor of the logarithm to base 2 of the number is 1. (Contributed by AV, 26-May-2020.)
⊢ (𝑋 ∈ ℝ+ → (⌊‘(𝑋 / (2↑(⌊‘(2 logb 𝑋))))) = 1)
Theorem	nnlog2ge0lt1 49405	A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ↔ (0 ≤ (2 logb 𝑁) ∧ (2 logb 𝑁) < 1)))
Theorem	logbpw2m1 49406	The floor of the binary logarithm of 2 to the power of a positive integer minus 1 is equal to the integer minus 1. (Contributed by AV, 31-May-2020.)
⊢ (𝐼 ∈ ℕ → (⌊‘(2 logb ((2↑𝐼) − 1))) = (𝐼 − 1))
Theorem	fllog2 49407	The floor of the binary logarithm of 2 to the power of an element of a half-open integer interval bounded by powers of 2 is equal to the integer. (Contributed by AV, 31-May-2020.)
⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘(2 logb 𝑁)) = 𝐼)
21.50.22.8  Binary length
Syntax	cblen 49408	Extend class notation with the class of the binary length function.
class #b
Definition	df-blen 49409	Define the binary length of an integer. Definition in section 1.3 of [AhoHopUll] p. 12. Although not restricted to integers, this definition is only meaningful for 𝑛 ∈ ℤ or even for 𝑛 ∈ ℂ. (Contributed by AV, 16-May-2020.)
⊢ #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
Theorem	blenval 49410	The binary length of an integer. (Contributed by AV, 20-May-2020.)
⊢ (𝑁 ∈ 𝑉 → (#b‘𝑁) = if(𝑁 = 0, 1, ((⌊‘(2 logb (abs‘𝑁))) + 1)))
Theorem	blen0 49411	The binary length of 0. (Contributed by AV, 20-May-2020.)
⊢ (#b‘0) = 1
Theorem	blenn0 49412	The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.)
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 0) → (#b‘𝑁) = ((⌊‘(2 logb (abs‘𝑁))) + 1))
Theorem	blenre 49413	The binary length of a positive real number. (Contributed by AV, 20-May-2020.)
⊢ (𝑁 ∈ ℝ+ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
Theorem	blennn 49414	The binary length of a positive integer. (Contributed by AV, 21-May-2020.)
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
Theorem	blennnelnn 49415	The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.)
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) ∈ ℕ)
Theorem	blennn0elnn 49416	The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (#b‘𝑁) ∈ ℕ)
Theorem	blenpw2 49417	The binary length of a power of 2 is the exponent plus 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐼 ∈ ℕ0 → (#b‘(2↑𝐼)) = (𝐼 + 1))
Theorem	blenpw2m1 49418	The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.)
⊢ (𝐼 ∈ ℕ → (#b‘((2↑𝐼) − 1)) = 𝐼)
Theorem	nnpw2blen 49419	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 49420	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 49421	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 49422	Every positive integer can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → 𝑁 = ((2↑((#b‘𝑁) − 1)) + (𝑁 mod (2↑((#b‘𝑁) − 1)))))
Theorem	blen1 49423	The binary length of 1. (Contributed by AV, 21-May-2020.)
⊢ (#b‘1) = 1
Theorem	blen2 49424	The binary length of 2. (Contributed by AV, 21-May-2020.)
⊢ (#b‘2) = 2
Theorem	nnpw2p 49425*	Every positive integer can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟))
Theorem	nnpw2pb 49426*	A number is a positive integer iff it can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ ↔ ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟))
Theorem	blen1b 49427	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 49428	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 49429	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 49430	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 49431	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 49432	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 49433	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))
21.50.22.9  Digits Generalization of df-bits 16504. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 49453: if 𝐾 and 𝑁 are nonnegative integers, then ((𝐾(digit‘2)𝑁) = 1 ↔ 𝐾 ∈ (bits‘𝑁)).
Syntax	cdig 49434	Extend class notation with the class of the digit extraction operation.
class digit
Definition	df-dig 49435*	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 14293. 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 49436*	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 49437	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 49438	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 49439	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 49440	The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖ ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = 0)
Theorem	dignn0ldlem 49441	Lemma for dignnld 49442. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → 𝑁 < (𝐵↑𝐾))
Theorem	dignnld 49442	The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → (𝐾(digit‘𝐵)𝑁) = 0)
Theorem	dig2nn0ld 49443	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 49444	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 49445	All digits of 0 are 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)0) = 0)
Theorem	digexp 49446	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 49447	All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)1) = if(𝐾 = 0, 1, 0))
Theorem	0dig1 49448	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 49449	The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.)
⊢ (𝑁 ∈ {0, 1} → (0(digit‘2)𝑁) = 𝑁)
Theorem	dig2nn0 49450	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 49451	The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → (0(digit‘2)𝑁) = 0)
Theorem	0dig2nn0o 49452	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 49453	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.50.22.10  Nonnegative integer as sum of its shifted digits
Theorem	dignn0flhalflem1 49454	Lemma 1 for dignn0flhalf 49457. (Contributed by AV, 7-Jun-2012.)
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁))))
Theorem	dignn0flhalflem2 49455	Lemma 2 for dignn0flhalf 49457. (Contributed by AV, 7-Jun-2012.)
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁))))
Theorem	dignn0ehalf 49456	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 49457	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 49458*	Lemma for nn0sumshdig 49462 (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 49459*	Lemma for nn0sumshdig 49462 (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 49460*	Lemma 1 for nn0sumshdig 49462 (induction step). (Contributed by AV, 7-Jun-2020.)
⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Theorem	nn0sumshdiglem2 49461*	Lemma 2 for nn0sumshdig 49462. (Contributed by AV, 7-Jun-2020.)
⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘))))
Theorem	nn0sumshdig 49462*	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.50.22.11  Algorithms for the multiplication of nonnegative integers
Theorem	nn0mulfsum 49463*	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 49464*	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 16575. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (0..^(#b‘𝐴))(((𝑘(digit‘2)𝐴) · (2↑𝑘)) · 𝐵))
21.50.22.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 8832) 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 49474 and mapsn 8892: (𝑋 ↑m {∅}) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 49484 and efmndbas 18969: (𝑋 ↑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 18969): "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 49495 and compare with df-clintop 49024: (𝑋 ↑m (𝑋 × 𝑋)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (𝑈↑↑𝑁) (see df-finxp 38089) 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 49468 shows that both definitions are equivalent.
Syntax	cnaryf 49465	Extend the definition of a class to include the n-ary functions.
class -aryF
Definition	df-naryf 49466*	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 49467	The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m (𝑋 ↑m 𝐼)))
Theorem	naryfvalixp 49468*	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 49469	An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m 𝐼)⟶𝑋))
Theorem	naryrcl 49470	Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V))
Theorem	naryfvalelfv 49471	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 49472*	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 49473*	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 49474. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐹 = {⟨∅, 𝑥⟩}))
Theorem	0aryfvalelfv 49474*	The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.)
⊢ (𝐹 ∈ (0-aryF 𝑋) → ∃𝑥 ∈ 𝑋 (𝐹‘∅) = 𝑥)
Theorem	1aryfvalel 49475	A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0})⟶𝑋))
Theorem	fv1arycl 49476	Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.)
⊢ ((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐺‘{⟨0, 𝐴⟩}) ∈ 𝑋)
Theorem	1arympt1 49477*	A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴:𝑋⟶𝑋) → 𝐹 ∈ (1-aryF 𝑋))
Theorem	1arympt1fv 49478*	The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{⟨0, 𝐵⟩}) = (𝐴‘𝐵))
Theorem	1arymaptfv 49479*	The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.)
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{⟨0, 𝑥⟩})))    ⇒   ⊢ (𝐹 ∈ (1-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐹‘{⟨0, 𝑥⟩})))
Theorem	1arymaptf 49480*	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 49481*	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 49482*	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 49483*	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 49484	The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.)
⊢ (1-aryF 𝑋) ≈ (𝑋 ↑m 𝑋)
Theorem	1aryenefmnd 49485	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 49486	A binary (endo)function on a set 𝑋. (Contributed by AV, 20-May-2024.)
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (2-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0, 1})⟶𝑋))
Theorem	fv2arycl 49487	Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.)
⊢ ((𝐺 ∈ (2-aryF 𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐺‘{⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) ∈ 𝑋)
Theorem	2arympt 49488*	A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.)
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑂:(𝑋 × 𝑋)⟶𝑋) → 𝐹 ∈ (2-aryF 𝑋))
Theorem	2arymptfv 49489*	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 49490*	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 49491*	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 49492*	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 49493*	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 49494*	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 49495	The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.)
⊢ (2-aryF 𝑋) ≈ (𝑋 ↑m (𝑋 × 𝑋))
21.50.22.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 49535)], 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 49499, based on a definition IterComp of "the n-th iterate of (a class/function) f", see df-itco 49498. As an illustration, we have ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹 ∘ 𝐹))) (see itcoval3 49504). The following recursive definition of the Ackermann function follows immediately from Definition df-ack 49499: ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1)). That Definition df-ack 49499 is equivalent to Péter's definition is proven by the following three theorems: ackval0val 49525: ((Ack‘0)‘𝑀) = (𝑀 + 1); ackvalsuc0val 49526: ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1); ackvalsucsucval 49527: ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)). The initial values of the Ackermann function are calculated in the following four theorems: ackval0012 49528: 𝐴(0, 0) = 1, 𝐴(0, 1) = 2, 𝐴(0, 2) = 3; ackval1012 49529: 𝐴(1, 0) = 2, 𝐴(1, 1) = 3, 𝐴(1, 3) = 4; ackval2012 49530: 𝐴(2, 0) = 3, 𝐴(2, 1) = 5, 𝐴(2, 3) = 7; ackval3012 49531: 𝐴(3, 0) = 5, 𝐴(3, 1) = ;13, 𝐴(3, 3) = ;29.
Syntax	citco 49496	Extend the definition of a class to include iterated functions.
class IterComp
Syntax	cack 49497	Extend the definition of a class to include the Ackermann function operator.
class Ack
Definition	df-itco 49498*	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 49499*	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 49500*	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 𝐹), 𝐹))))