Home | Metamath
Proof Explorer Theorem List (p. 460 of 466) | < 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: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | refdivpm 45901 | The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴)) | ||
Theorem | fdivmptfv 45902 | The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.) |
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
Theorem | refdivmptfv 45903 | The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.) |
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
Syntax | cbigo 45904 | Extend class notation with the class of the "big-O" function. |
class Ο | ||
Definition | df-bigo 45905* | Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalization of "big-O of one", see df-o1 15208 and df-lo1 15209. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 45914. (Contributed by AV, 15-May-2020.) |
⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))}) | ||
Theorem | bigoval 45906* | Set of functions of order G(x). (Contributed by AV, 15-May-2020.) |
⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))}) | ||
Theorem | elbigofrcl 45907 | Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ)) | ||
Theorem | elbigo 45908* | Properties of a function of order G(x). (Contributed by AV, 16-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) | ||
Theorem | elbigo2 45909* | Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.) |
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) | ||
Theorem | elbigo2r 45910* | Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.) |
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ (𝑀 · (𝐺‘𝑥))))) → 𝐹 ∈ (Ο‘𝐺)) | ||
Theorem | elbigof 45911 | A function of order G(x) is a function. (Contributed by AV, 18-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐹:dom 𝐹⟶ℝ) | ||
Theorem | elbigodm 45912 | The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → dom 𝐹 ⊆ ℝ) | ||
Theorem | elbigoimp 45913* | The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.) |
⊢ ((𝐹 ∈ (Ο‘𝐺) ∧ 𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ dom 𝐺) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) | ||
Theorem | elbigolo1 45914 | A function (into the positive reals) is of order G(x) iff the quotient of the function and G(x) (also a function into the positive reals) is an eventually upper bounded function. (Contributed by AV, 20-May-2020.) (Proof shortened by II, 16-Feb-2023.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1))) | ||
Theorem | rege1logbrege0 45915 | The general logarithm, with a real base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.) |
⊢ ((𝐵 ∈ (1(,)+∞) ∧ 𝑋 ∈ (1[,)+∞)) → 0 ≤ (𝐵 logb 𝑋)) | ||
Theorem | rege1logbzge0 45916 | The general logarithm, with an integer base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ (1[,)+∞)) → 0 ≤ (𝐵 logb 𝑋)) | ||
Theorem | fllogbd 45917 | A real number is between the base of a logarithm to the power of the floor of the logarithm of the number and the base of the logarithm to the power of the floor of the logarithm of the number plus one. (Contributed by AV, 23-May-2020.) |
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) & ⊢ 𝐸 = (⌊‘(𝐵 logb 𝑋)) ⇒ ⊢ (𝜑 → ((𝐵↑𝐸) ≤ 𝑋 ∧ 𝑋 < (𝐵↑(𝐸 + 1)))) | ||
Theorem | relogbmulbexp 45918 | The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020.) |
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐵↑𝑐𝐶))) = ((𝐵 logb 𝐴) + 𝐶)) | ||
Theorem | relogbdivb 45919 | 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 45920 | 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 45921 | 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 ↔ 𝑋 < 𝐵)) | ||
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 45922 | 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 45923 | 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 45924 | 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 45925 | 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 𝑁)) = 𝐼) | ||
Syntax | cblen 45926 | Extend class notation with the class of the binary length function. |
class #b | ||
Definition | df-blen 45927 | 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 45928 | The binary length of an integer. (Contributed by AV, 20-May-2020.) |
⊢ (𝑁 ∈ 𝑉 → (#b‘𝑁) = if(𝑁 = 0, 1, ((⌊‘(2 logb (abs‘𝑁))) + 1))) | ||
Theorem | blen0 45929 | The binary length of 0. (Contributed by AV, 20-May-2020.) |
⊢ (#b‘0) = 1 | ||
Theorem | blenn0 45930 | The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.) |
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 0) → (#b‘𝑁) = ((⌊‘(2 logb (abs‘𝑁))) + 1)) | ||
Theorem | blenre 45931 | The binary length of a positive real number. (Contributed by AV, 20-May-2020.) |
⊢ (𝑁 ∈ ℝ+ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) | ||
Theorem | blennn 45932 | The binary length of a positive integer. (Contributed by AV, 21-May-2020.) |
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) | ||
Theorem | blennnelnn 45933 | The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.) |
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) ∈ ℕ) | ||
Theorem | blennn0elnn 45934 | The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#b‘𝑁) ∈ ℕ) | ||
Theorem | blenpw2 45935 | 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 45936 | The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.) |
⊢ (𝐼 ∈ ℕ → (#b‘((2↑𝐼) − 1)) = 𝐼) | ||
Theorem | nnpw2blen 45937 | 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 45938 | 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 45939 | 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 45940 | 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 45941 | The binary length of 1. (Contributed by AV, 21-May-2020.) |
⊢ (#b‘1) = 1 | ||
Theorem | blen2 45942 | The binary length of 2. (Contributed by AV, 21-May-2020.) |
⊢ (#b‘2) = 2 | ||
Theorem | nnpw2p 45943* | 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 45944* | 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 45945 | 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 45946 | 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 45947 | 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 45948 | 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 45949 | 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 45950 | 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 45951 | 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 16138. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 45971: if 𝐾 and 𝑁 are nonnegative integers, then ((𝐾(digit‘2)𝑁) = 1 ↔ 𝐾 ∈ (bits‘𝑁)). | ||
Syntax | cdig 45952 | Extend class notation with the class of the digit extraction operation. |
class digit | ||
Definition | df-dig 45953* | 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 13961. 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 45954* | 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 45955 | 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 45956 | 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 45957 | 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 45958 | The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.) |
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖ ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = 0) | ||
Theorem | dignn0ldlem 45959 | Lemma for dignnld 45960. (Contributed by AV, 25-May-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → 𝑁 < (𝐵↑𝐾)) | ||
Theorem | dignnld 45960 | The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → (𝐾(digit‘𝐵)𝑁) = 0) | ||
Theorem | dig2nn0ld 45961 | 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 45962 | 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 45963 | All digits of 0 are 0. (Contributed by AV, 24-May-2020.) |
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)0) = 0) | ||
Theorem | digexp 45964 | 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 45965 | All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.) |
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)1) = if(𝐾 = 0, 1, 0)) | ||
Theorem | 0dig1 45966 | 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 45967 | The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.) |
⊢ (𝑁 ∈ {0, 1} → (0(digit‘2)𝑁) = 𝑁) | ||
Theorem | dig2nn0 45968 | 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 45969 | The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → (0(digit‘2)𝑁) = 0) | ||
Theorem | 0dig2nn0o 45970 | 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 45971 | 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 45972 | Lemma 1 for dignn0flhalf 45975. (Contributed by AV, 7-Jun-2012.) |
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁)))) | ||
Theorem | dignn0flhalflem2 45973 | Lemma 2 for dignn0flhalf 45975. (Contributed by AV, 7-Jun-2012.) |
⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) | ||
Theorem | dignn0ehalf 45974 | 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 45975 | 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 45976* | Lemma for nn0sumshdig 45980 (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 45977* | Lemma for nn0sumshdig 45980 (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 45978* | Lemma 1 for nn0sumshdig 45980 (induction step). (Contributed by AV, 7-Jun-2020.) |
⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) | ||
Theorem | nn0sumshdiglem2 45979* | Lemma 2 for nn0sumshdig 45980. (Contributed by AV, 7-Jun-2020.) |
⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) | ||
Theorem | nn0sumshdig 45980* | 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 45981* | 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 45982* | 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 16209. (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 8626) 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 45992 and mapsn 8685: (𝑋 ↑m {∅}) - n = 1 (unary functions): These correspond actually to usual endofunctions, see 1aryenef 46002 and efmndbas 18519: (𝑋 ↑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 18519): "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 46013 and compare with df-clintop 45405: (𝑋 ↑m (𝑋 × 𝑋)). Instead of using indexed arguments (represented by a mapping as described above), elements of Cartesian exponentiations (𝑈↑↑𝑁) (see df-finxp 35564) 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 45986 shows that both definitions are equivalent. | ||
Syntax | cnaryf 45983 | Extend the definition of a class to include the n-ary functions. |
class -aryF | ||
Definition | df-naryf 45984* | 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 45985 | The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋 ↑m (𝑋 ↑m 𝐼))) | ||
Theorem | naryfvalixp 45986* | 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 45987 | An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m 𝐼)⟶𝑋)) | ||
Theorem | naryrcl 45988 | Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.) |
⊢ 𝐼 = (0..^𝑁) ⇒ ⊢ (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ V)) | ||
Theorem | naryfvalelfv 45989 | 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 45990* | 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 45991* | 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 45992. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.) |
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥 ∈ 𝑋 𝐹 = {〈∅, 𝑥〉})) | ||
Theorem | 0aryfvalelfv 45992* | The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.) |
⊢ (𝐹 ∈ (0-aryF 𝑋) → ∃𝑥 ∈ 𝑋 (𝐹‘∅) = 𝑥) | ||
Theorem | 1aryfvalel 45993 | A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.) |
⊢ (𝑋 ∈ 𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋 ↑m {0})⟶𝑋)) | ||
Theorem | fv1arycl 45994 | Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.) |
⊢ ((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐺‘{〈0, 𝐴〉}) ∈ 𝑋) | ||
Theorem | 1arympt1 45995* | A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴:𝑋⟶𝑋) → 𝐹 ∈ (1-aryF 𝑋)) | ||
Theorem | 1arympt1fv 45996* | The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.) |
⊢ 𝐹 = (𝑥 ∈ (𝑋 ↑m {0}) ↦ (𝐴‘(𝑥‘0))) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → (𝐹‘{〈0, 𝐵〉}) = (𝐴‘𝐵)) | ||
Theorem | 1arymaptfv 45997* | The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.) |
⊢ 𝐻 = (ℎ ∈ (1-aryF 𝑋) ↦ (𝑥 ∈ 𝑋 ↦ (ℎ‘{〈0, 𝑥〉}))) ⇒ ⊢ (𝐹 ∈ (1-aryF 𝑋) → (𝐻‘𝐹) = (𝑥 ∈ 𝑋 ↦ (𝐹‘{〈0, 𝑥〉}))) | ||
Theorem | 1arymaptf 45998* | 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 45999* | 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 46000* | 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 𝑋)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |