![]() |
Metamath
Proof Explorer Theorem List (p. 476 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pw2m1lepw2m1 47501 | 2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020.) |
β’ (πΌ β β β (2β(πΌ β 1)) β€ ((2βπΌ) β 1)) | ||
Theorem | zgtp1leeq 47502 | If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.) |
β’ ((πΌ β β€ β§ π΄ β β€) β (((π΄ β 1) < πΌ β§ πΌ β€ π΄) β πΌ = π΄)) | ||
Theorem | flsubz 47503 | An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.) |
β’ ((π΄ β β β§ π β β€) β (ββ(π΄ β π)) = ((ββπ΄) β π)) | ||
Theorem | fldivmod 47504 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
β’ ((π΄ β β β§ π΅ β β+) β (ββ(π΄ / π΅)) = ((π΄ β (π΄ mod π΅)) / π΅)) | ||
Theorem | mod0mul 47505* | If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020.) |
β’ ((π΄ β β€ β§ π β β) β ((π΄ mod π) = 0 β βπ₯ β β€ π΄ = (π₯ Β· π))) | ||
Theorem | modn0mul 47506* | If an integer is not 0 modulo a positive integer, this integer must be the sum of the product of another integer and the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020.) |
β’ ((π΄ β β€ β§ π β β) β ((π΄ mod π) β 0 β βπ₯ β β€ βπ¦ β (1..^π)π΄ = ((π₯ Β· π) + π¦))) | ||
Theorem | m1modmmod 47507 | An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020.) |
β’ ((π΄ β β€ β§ π β β) β (((π΄ β 1) mod π) β (π΄ mod π)) = if((π΄ mod π) = 0, (π β 1), -1)) | ||
Theorem | difmodm1lt 47508 | The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd π΄ and π = 2, since ((π΄ mod π) β ((π΄ β 1) mod π)) would be (1 β 0) = 1 which is not less than (π β 1) = 1. (Contributed by AV, 6-Jun-2012.) |
β’ ((π΄ β β€ β§ π β β β§ 2 < π) β ((π΄ mod π) β ((π΄ β 1) mod π)) < (π β 1)) | ||
Theorem | nn0onn0ex 47509* | For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.) |
β’ ((π β β0 β§ ((π + 1) / 2) β β0) β βπ β β0 π = ((2 Β· π) + 1)) | ||
Theorem | nn0enn0ex 47510* | For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.) |
β’ ((π β β0 β§ (π / 2) β β0) β βπ β β0 π = (2 Β· π)) | ||
Theorem | nnennex 47511* | For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023.) |
β’ ((π β β β§ (π / 2) β β) β βπ β β π = (2 Β· π)) | ||
Theorem | nneop 47512 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
β’ (π β β β ((π / 2) β β β¨ ((π + 1) / 2) β β)) | ||
Theorem | nneom 47513 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
β’ (π β β β ((π / 2) β β β¨ ((π β 1) / 2) β β0)) | ||
Theorem | nn0eo 47514 | A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.) |
β’ (π β β0 β ((π / 2) β β0 β¨ ((π + 1) / 2) β β0)) | ||
Theorem | nnpw2even 47515 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) |
β’ (π β β β ((2βπ) / 2) β β) | ||
Theorem | zefldiv2 47516 | 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 47517 | 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 47518 | 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 47519 | 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 47520 | 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 47521 | Logarithm of a complex power. Generalization of logcxp 26577. (Contributed by AV, 22-May-2020.) |
β’ ((π΄ β (β β {0}) β§ π΅ β β β§ (π΅ Β· (logβπ΄)) β ran log) β (logβ(π΄βππ΅)) = (π΅ Β· (logβπ΄))) | ||
Theorem | regt1loggt0 47522 | 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 47523 | Extend class notation with the division operator of two functions. |
class /f | ||
Definition | df-fdiv 47524* | Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
β’ /f = (π β V, π β V β¦ ((π βf / π) βΎ (π supp 0))) | ||
Theorem | fdivval 47525 | The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
β’ ((πΉ β π β§ πΊ β π) β (πΉ /f πΊ) = ((πΉ βf / πΊ) βΎ (πΊ supp 0))) | ||
Theorem | fdivmpt 47526* | The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.) |
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΉ /f πΊ) = (π₯ β (πΊ supp 0) β¦ ((πΉβπ₯) / (πΊβπ₯)))) | ||
Theorem | fdivmptf 47527 | 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 47528 | 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 47529 | The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.) |
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΉ /f πΊ) β (β βpm π΄)) | ||
Theorem | refdivpm 47530 | The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.) |
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΉ /f πΊ) β (β βpm π΄)) | ||
Theorem | fdivmptfv 47531 | The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.) |
β’ (((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β§ π β (πΊ supp 0)) β ((πΉ /f πΊ)βπ) = ((πΉβπ) / (πΊβπ))) | ||
Theorem | refdivmptfv 47532 | The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.) |
β’ (((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β§ π β (πΊ supp 0)) β ((πΉ /f πΊ)βπ) = ((πΉβπ) / (πΊβπ))) | ||
Syntax | cbigo 47533 | Extend class notation with the class of the "big-O" function. |
class Ξ | ||
Definition | df-bigo 47534* | 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 15452 and df-lo1 15453. As explained in the comment of df-o1 , any big-O can be represented in terms of π(1) and division, see elbigolo1 47543. (Contributed by AV, 15-May-2020.) |
β’ Ξ = (π β (β βpm β) β¦ {π β (β βpm β) β£ βπ₯ β β βπ β β βπ¦ β (dom π β© (π₯[,)+β))(πβπ¦) β€ (π Β· (πβπ¦))}) | ||
Theorem | bigoval 47535* | Set of functions of order G(x). (Contributed by AV, 15-May-2020.) |
β’ (πΊ β (β βpm β) β (ΞβπΊ) = {π β (β βpm β) β£ βπ₯ β β βπ β β βπ¦ β (dom π β© (π₯[,)+β))(πβπ¦) β€ (π Β· (πΊβπ¦))}) | ||
Theorem | elbigofrcl 47536 | Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.) |
β’ (πΉ β (ΞβπΊ) β πΊ β (β βpm β)) | ||
Theorem | elbigo 47537* | Properties of a function of order G(x). (Contributed by AV, 16-May-2020.) |
β’ (πΉ β (ΞβπΊ) β (πΉ β (β βpm β) β§ πΊ β (β βpm β) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ (π Β· (πΊβπ¦)))) | ||
Theorem | elbigo2 47538* | Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.) |
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄)) β (πΉ β (ΞβπΊ) β βπ₯ β β βπ β β βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦))))) | ||
Theorem | elbigo2r 47539* | Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.) |
β’ (((πΊ:π΄βΆβ β§ π΄ β β) β§ (πΉ:π΅βΆβ β§ π΅ β π΄) β§ (πΆ β β β§ π β β β§ βπ₯ β π΅ (πΆ β€ π₯ β (πΉβπ₯) β€ (π Β· (πΊβπ₯))))) β πΉ β (ΞβπΊ)) | ||
Theorem | elbigof 47540 | A function of order G(x) is a function. (Contributed by AV, 18-May-2020.) |
β’ (πΉ β (ΞβπΊ) β πΉ:dom πΉβΆβ) | ||
Theorem | elbigodm 47541 | The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.) |
β’ (πΉ β (ΞβπΊ) β dom πΉ β β) | ||
Theorem | elbigoimp 47542* | The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.) |
β’ ((πΉ β (ΞβπΊ) β§ πΉ:π΄βΆβ β§ π΄ β dom πΊ) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ (π Β· (πΊβπ¦)))) | ||
Theorem | elbigolo1 47543 | 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 47544 | 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 47545 | 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 47546 | 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 47547 | 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 47548 | 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 47549 | 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 47550 | 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 47551 | 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 47552 | 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 47553 | 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 47554 | 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 47555 | Extend class notation with the class of the binary length function. |
class #b | ||
Definition | df-blen 47556 | 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 47557 | The binary length of an integer. (Contributed by AV, 20-May-2020.) |
β’ (π β π β (#bβπ) = if(π = 0, 1, ((ββ(2 logb (absβπ))) + 1))) | ||
Theorem | blen0 47558 | The binary length of 0. (Contributed by AV, 20-May-2020.) |
β’ (#bβ0) = 1 | ||
Theorem | blenn0 47559 | The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.) |
β’ ((π β π β§ π β 0) β (#bβπ) = ((ββ(2 logb (absβπ))) + 1)) | ||
Theorem | blenre 47560 | The binary length of a positive real number. (Contributed by AV, 20-May-2020.) |
β’ (π β β+ β (#bβπ) = ((ββ(2 logb π)) + 1)) | ||
Theorem | blennn 47561 | The binary length of a positive integer. (Contributed by AV, 21-May-2020.) |
β’ (π β β β (#bβπ) = ((ββ(2 logb π)) + 1)) | ||
Theorem | blennnelnn 47562 | The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.) |
β’ (π β β β (#bβπ) β β) | ||
Theorem | blennn0elnn 47563 | The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.) |
β’ (π β β0 β (#bβπ) β β) | ||
Theorem | blenpw2 47564 | 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 47565 | The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.) |
β’ (πΌ β β β (#bβ((2βπΌ) β 1)) = πΌ) | ||
Theorem | nnpw2blen 47566 | 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 47567 | 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 47568 | 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 47569 | 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 47570 | The binary length of 1. (Contributed by AV, 21-May-2020.) |
β’ (#bβ1) = 1 | ||
Theorem | blen2 47571 | The binary length of 2. (Contributed by AV, 21-May-2020.) |
β’ (#bβ2) = 2 | ||
Theorem | nnpw2p 47572* | 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 47573* | 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 47574 | 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 47575 | 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 47576 | 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 47577 | 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 47578 | 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 47579 | 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 47580 | 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 16382. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 47600: if πΎ and π are nonnegative integers, then ((πΎ(digitβ2)π) = 1 β πΎ β (bitsβπ)). | ||
Syntax | cdig 47581 | Extend class notation with the class of the digit extraction operation. |
class digit | ||
Definition | df-dig 47582* | 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 14217. 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 47583* | 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 47584 | 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 47585 | 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 47586 | 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 47587 | The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.) |
β’ ((π΅ β β β§ πΎ β (β€ β β0) β§ π β β0) β (πΎ(digitβπ΅)π) = 0) | ||
Theorem | dignn0ldlem 47588 | Lemma for dignnld 47589. (Contributed by AV, 25-May-2020.) |
β’ ((π΅ β (β€β₯β2) β§ π β β β§ πΎ β (β€β₯β((ββ(π΅ logb π)) + 1))) β π < (π΅βπΎ)) | ||
Theorem | dignnld 47589 | The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.) |
β’ ((π΅ β (β€β₯β2) β§ π β β β§ πΎ β (β€β₯β((ββ(π΅ logb π)) + 1))) β (πΎ(digitβπ΅)π) = 0) | ||
Theorem | dig2nn0ld 47590 | 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 47591 | 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 47592 | All digits of 0 are 0. (Contributed by AV, 24-May-2020.) |
β’ ((π΅ β β β§ πΎ β β€) β (πΎ(digitβπ΅)0) = 0) | ||
Theorem | digexp 47593 | 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 47594 | All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.) |
β’ ((π΅ β (β€β₯β2) β§ πΎ β β€) β (πΎ(digitβπ΅)1) = if(πΎ = 0, 1, 0)) | ||
Theorem | 0dig1 47595 | 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 47596 | The integers 0 and 1 correspond to their last bit. (Contributed by AV, 28-May-2010.) |
β’ (π β {0, 1} β (0(digitβ2)π) = π) | ||
Theorem | dig2nn0 47597 | 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 47598 | The last bit of an even integer is 0. (Contributed by AV, 3-Jun-2010.) |
β’ ((π β β0 β§ (π / 2) β β0) β (0(digitβ2)π) = 0) | ||
Theorem | 0dig2nn0o 47599 | 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 47600 | 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βπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |