HomeTheorem List (p. 492 of 504)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 492 of 504) | < 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-31065) |
Hilbert Space Explorer
(31066-32588) |
Users' Mathboxes
(32589-50379) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nneop 49101 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ)) | ||
| Theorem | nneom 49102 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
| Theorem | nn0eo 49103 | A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0)) | ||
| Theorem | nnpw2even 49104 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ) | ||
| Theorem | zefldiv2 49105 | The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = (𝑁 / 2)) | ||
| Theorem | zofldiv2 49106 | The floor of an odd integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2)) | ||
| Theorem | nn0ofldiv2 49107 | The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) (Proof shortened by AV, 7-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2)) | ||
| Theorem | flnn0div2ge 49108 | The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2))) | ||
| Theorem | flnn0ohalf 49109 | The floor of the half of an odd positive integer is equal to the floor of the half of the integer decreased by 1. (Contributed by AV, 5-Jun-2012.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = (⌊‘((𝑁 − 1) / 2))) | ||
| Theorem | logcxp0 49110 | Logarithm of a complex power. Generalization of logcxp 26709. (Contributed by AV, 22-May-2020.) |
| ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
| Theorem | regt1loggt0 49111 | The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.) |
| ⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵)) | ||
| Syntax | cfdiv 49112 | Extend class notation with the division operator of two functions. |
| class /f | ||
| Definition | df-fdiv 49113* | Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
| ⊢ /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0))) | ||
| Theorem | fdivval 49114 | The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 /f 𝐺) = ((𝐹 ∘f / 𝐺) ↾ (𝐺 supp 0))) | ||
| Theorem | fdivmpt 49115* | The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.) |
| ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) = (𝑥 ∈ (𝐺 supp 0) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥)))) | ||
| Theorem | fdivmptf 49116 | The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020.) |
| ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℂ) | ||
| Theorem | refdivmptf 49117 | The quotient of two functions into the real numbers is a function into the real numbers. (Contributed by AV, 16-May-2020.) |
| ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ) | ||
| Theorem | fdivpm 49118 | The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.) |
| ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℂ ↑pm 𝐴)) | ||
| Theorem | refdivpm 49119 | The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.) |
| ⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴)) | ||
| Theorem | fdivmptfv 49120 | The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.) |
| ⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
| Theorem | refdivmptfv 49121 | The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.) |
| ⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
| Syntax | cbigo 49122 | Extend class notation with the class of the "big-O" function. |
| class Ο | ||
| Definition | df-bigo 49123* | 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 15498 and df-lo1 15499. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 49132. (Contributed by AV, 15-May-2020.) |
| ⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))}) | ||
| Theorem | bigoval 49124* | Set of functions of order G(x). (Contributed by AV, 15-May-2020.) |
| ⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))}) | ||
| Theorem | elbigofrcl 49125 | Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.) |
| ⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ)) | ||
| Theorem | elbigo 49126* | Properties of a function of order G(x). (Contributed by AV, 16-May-2020.) |
| ⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) | ||
| Theorem | elbigo2 49127* | Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.) |
| ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) | ||
| Theorem | elbigo2r 49128* | Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.) |
| ⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ (𝑀 · (𝐺‘𝑥))))) → 𝐹 ∈ (Ο‘𝐺)) | ||
| Theorem | elbigof 49129 | A function of order G(x) is a function. (Contributed by AV, 18-May-2020.) |
| ⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐹:dom 𝐹⟶ℝ) | ||
| Theorem | elbigodm 49130 | The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.) |
| ⊢ (𝐹 ∈ (Ο‘𝐺) → dom 𝐹 ⊆ ℝ) | ||
| Theorem | elbigoimp 49131* | The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.) |
| ⊢ ((𝐹 ∈ (Ο‘𝐺) ∧ 𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ dom 𝐺) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) | ||
| Theorem | elbigolo1 49132 | 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 49133 | 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 49134 | 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 49135 | 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 49136 | 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 49137 | 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 49138 | 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 49139 | 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 49140 | 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 49141 | 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 49142 | 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 49143 | 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 49144 | Extend class notation with the class of the binary length function. |
| class #b | ||
| Definition | df-blen 49145 | 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 49146 | The binary length of an integer. (Contributed by AV, 20-May-2020.) |
| ⊢ (𝑁 ∈ 𝑉 → (#b‘𝑁) = if(𝑁 = 0, 1, ((⌊‘(2 logb (abs‘𝑁))) + 1))) | ||
| Theorem | blen0 49147 | The binary length of 0. (Contributed by AV, 20-May-2020.) |
| ⊢ (#b‘0) = 1 | ||
| Theorem | blenn0 49148 | The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.) |
| ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 0) → (#b‘𝑁) = ((⌊‘(2 logb (abs‘𝑁))) + 1)) | ||
| Theorem | blenre 49149 | The binary length of a positive real number. (Contributed by AV, 20-May-2020.) |
| ⊢ (𝑁 ∈ ℝ+ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) | ||
| Theorem | blennn 49150 | The binary length of a positive integer. (Contributed by AV, 21-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) | ||
| Theorem | blennnelnn 49151 | The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.) |
| ⊢ (𝑁 ∈ ℕ → (#b‘𝑁) ∈ ℕ) | ||
| Theorem | blennn0elnn 49152 | The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.) |
| ⊢ (𝑁 ∈ ℕ0 → (#b‘𝑁) ∈ ℕ) | ||
| Theorem | blenpw2 49153 | 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 49154 | The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.) |
| ⊢ (𝐼 ∈ ℕ → (#b‘((2↑𝐼) − 1)) = 𝐼) | ||
| Theorem | nnpw2blen 49155 | 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 49156 | 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 49157 | 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 49158 | 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 49159 | The binary length of 1. (Contributed by AV, 21-May-2020.) |
| ⊢ (#b‘1) = 1 | ||
| Theorem | blen2 49160 | The binary length of 2. (Contributed by AV, 21-May-2020.) |
| ⊢ (#b‘2) = 2 | ||
| Theorem | nnpw2p 49161* | 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 49162* | 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 49163 | 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 49164 | 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 49165 | 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 49166 | 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 49167 | 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 49168 | 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 49169 | 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 16437. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 49189: if 𝐾 and 𝑁 are nonnegative integers, then ((𝐾(digit‘2)𝑁) = 1 ↔ 𝐾 ∈ (bits‘𝑁)). | ||
| Syntax | cdig 49170 | Extend class notation with the class of the digit extraction operation. |
| class digit | ||
| Definition | df-dig 49171* | 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 14245. 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 49172* | 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 49173 | 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 49174 | 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 49175 | 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 49176 | The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖ ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = 0) | ||
| Theorem | dignn0ldlem 49177 | Lemma for dignnld 49178. (Contributed by AV, 25-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → 𝑁 < (𝐵↑𝐾)) | ||
| Theorem | dignnld 49178 | The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → (𝐾(digit‘𝐵)𝑁) = 0) | ||
| Theorem | dig2nn0ld 49179 | 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 49180 | 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 49181 | All digits of 0 are 0. (Contributed by AV, 24-May-2020.) |
| ⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)0) = 0) | ||
| Theorem | digexp 49182 | 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 49183 | All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)1) = if(𝐾 = 0, 1, 0)) | ||
| Theorem | 0dig1 49184 | 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 49185 | The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.) |
| ⊢ (𝑁 ∈ {0, 1} → (0(digit‘2)𝑁) = 𝑁) | ||
| Theorem | dig2nn0 49186 | 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 49187 | The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → (0(digit‘2)𝑁) = 0) | ||
| Theorem | 0dig2nn0o 49188 | 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 49189 | 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 49190 | Lemma 1 for dignn0flhalf 49193. (Contributed by AV, 7-Jun-2012.) |
| ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((𝐴 / (2↑𝑁)) − 1)) < (⌊‘((𝐴 − 1) / (2↑𝑁)))) | ||
| Theorem | dignn0flhalflem2 49191 | Lemma 2 for dignn0flhalf 49193. (Contributed by AV, 7-Jun-2012.) |
| ⊢ ((𝐴 ∈ ℤ ∧ ((𝐴 − 1) / 2) ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝑁 + 1)))) = (⌊‘((⌊‘(𝐴 / 2)) / (2↑𝑁)))) | ||
| Theorem | dignn0ehalf 49192 | 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 49193 | 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 49194* | Lemma for nn0sumshdig 49198 (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 49195* | Lemma for nn0sumshdig 49198 (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 49196* | Lemma 1 for nn0sumshdig 49198 (induction step). (Contributed by AV, 7-Jun-2020.) |
| ⊢ (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝑦 → 𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))) | ||
| Theorem | nn0sumshdiglem2 49197* | Lemma 2 for nn0sumshdig 49198. (Contributed by AV, 7-Jun-2020.) |
| ⊢ (𝐿 ∈ ℕ → ∀𝑎 ∈ ℕ0 ((#b‘𝑎) = 𝐿 → 𝑎 = Σ𝑘 ∈ (0..^𝐿)((𝑘(digit‘2)𝑎) · (2↑𝑘)))) | ||
| Theorem | nn0sumshdig 49198* | 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 49199* | 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 49200* | 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 16508. (Contributed by AV, 7-Jun-2020.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 · 𝐵) = Σ𝑘 ∈ (0..^(#b‘𝐴))(((𝑘(digit‘2)𝐴) · (2↑𝑘)) · 𝐵)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |