![]() |
Metamath
Proof Explorer Theorem List (p. 164 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zob 16301 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) |
โข (๐ โ โค โ (((๐ + 1) / 2) โ โค โ ((๐ โ 1) / 2) โ โค)) | ||
Theorem | oddm1d2 16302 | An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ ((๐ โ 1) / 2) โ โค)) | ||
Theorem | ltoddhalfle 16303 | An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ โ โค) โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))) | ||
Theorem | halfleoddlt 16304 | An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ โ โค) โ ((๐ / 2) โค ๐ โ (๐ / 2) < ๐)) | ||
Theorem | opoe 16305 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (((๐ด โ โค โง ยฌ 2 โฅ ๐ด) โง (๐ต โ โค โง ยฌ 2 โฅ ๐ต)) โ 2 โฅ (๐ด + ๐ต)) | ||
Theorem | omoe 16306 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (((๐ด โ โค โง ยฌ 2 โฅ ๐ด) โง (๐ต โ โค โง ยฌ 2 โฅ ๐ต)) โ 2 โฅ (๐ด โ ๐ต)) | ||
Theorem | opeo 16307 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (((๐ด โ โค โง ยฌ 2 โฅ ๐ด) โง (๐ต โ โค โง 2 โฅ ๐ต)) โ ยฌ 2 โฅ (๐ด + ๐ต)) | ||
Theorem | omeo 16308 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (((๐ด โ โค โง ยฌ 2 โฅ ๐ด) โง (๐ต โ โค โง 2 โฅ ๐ต)) โ ยฌ 2 โฅ (๐ด โ ๐ต)) | ||
Theorem | z0even 16309 | 2 divides 0. That means 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
โข 2 โฅ 0 | ||
Theorem | n2dvds1 16310 | 2 does not divide 1. That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) (Proof shortened by Steven Nguyen, 3-May-2023.) |
โข ยฌ 2 โฅ 1 | ||
Theorem | n2dvdsm1 16311 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
โข ยฌ 2 โฅ -1 | ||
Theorem | z2even 16312 | 2 divides 2. That means 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
โข 2 โฅ 2 | ||
Theorem | n2dvds3 16313 | 2 does not divide 3. That means 3 is odd. (Contributed by AV, 28-Feb-2021.) (Proof shortened by Steven Nguyen, 3-May-2023.) |
โข ยฌ 2 โฅ 3 | ||
Theorem | z4even 16314 | 2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
โข 2 โฅ 4 | ||
Theorem | 4dvdseven 16315 | An integer which is divisible by 4 is divisible by 2, that is, is even. (Contributed by AV, 4-Jul-2021.) |
โข (4 โฅ ๐ โ 2 โฅ ๐) | ||
Theorem | m1expe 16316 | Exponentiation of -1 by an even power. Variant of m1expeven 14074. (Contributed by AV, 25-Jun-2021.) |
โข (2 โฅ ๐ โ (-1โ๐) = 1) | ||
Theorem | m1expo 16317 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ (-1โ๐) = -1) | ||
Theorem | m1exp1 16318 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) |
โข (๐ โ โค โ ((-1โ๐) = 1 โ 2 โฅ ๐)) | ||
Theorem | nn0enne 16319 | A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.) |
โข (๐ โ โ โ ((๐ / 2) โ โ0 โ (๐ / 2) โ โ)) | ||
Theorem | nn0ehalf 16320 | The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.) (Proof shortened by AV, 10-Jul-2022.) |
โข ((๐ โ โ0 โง 2 โฅ ๐) โ (๐ / 2) โ โ0) | ||
Theorem | nnehalf 16321 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) |
โข ((๐ โ โ โง 2 โฅ ๐) โ (๐ / 2) โ โ) | ||
Theorem | nn0onn 16322 | An odd nonnegative integer is positive. (Contributed by Steven Nguyen, 25-Mar-2023.) |
โข ((๐ โ โ0 โง ยฌ 2 โฅ ๐) โ ๐ โ โ) | ||
Theorem | nn0o1gt2 16323 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) |
โข ((๐ โ โ0 โง ((๐ + 1) / 2) โ โ0) โ (๐ = 1 โจ 2 < ๐)) | ||
Theorem | nno 16324 | An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) (Proof shortened by AV, 10-Jul-2022.) |
โข ((๐ โ (โคโฅโ2) โง ((๐ + 1) / 2) โ โ0) โ ((๐ โ 1) / 2) โ โ) | ||
Theorem | nn0o 16325 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.) |
โข ((๐ โ โ0 โง ((๐ + 1) / 2) โ โ0) โ ((๐ โ 1) / 2) โ โ0) | ||
Theorem | nn0ob 16326 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
โข (๐ โ โ0 โ (((๐ + 1) / 2) โ โ0 โ ((๐ โ 1) / 2) โ โ0)) | ||
Theorem | nn0oddm1d2 16327 | A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) (Proof shortened by AV, 10-Jul-2022.) |
โข (๐ โ โ0 โ (ยฌ 2 โฅ ๐ โ ((๐ โ 1) / 2) โ โ0)) | ||
Theorem | nnoddm1d2 16328 | A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
โข (๐ โ โ โ (ยฌ 2 โฅ ๐ โ ((๐ + 1) / 2) โ โ)) | ||
Theorem | sumeven 16329* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) & โข ((๐ โง ๐ โ ๐ด) โ 2 โฅ ๐ต) โ โข (๐ โ 2 โฅ ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | sumodd 16330* | If every term in a sum is odd, then the sum is even iff the number of terms in the sum is even. (Contributed by AV, 14-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) & โข ((๐ โง ๐ โ ๐ด) โ ยฌ 2 โฅ ๐ต) โ โข (๐ โ (2 โฅ (โฏโ๐ด) โ 2 โฅ ฮฃ๐ โ ๐ด ๐ต)) | ||
Theorem | evensumodd 16331* | If every term in a sum with an even number of terms is odd, then the sum is even. (Contributed by AV, 14-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) & โข ((๐ โง ๐ โ ๐ด) โ ยฌ 2 โฅ ๐ต) & โข (๐ โ 2 โฅ (โฏโ๐ด)) โ โข (๐ โ 2 โฅ ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | oddsumodd 16332* | If every term in a sum with an odd number of terms is odd, then the sum is odd. (Contributed by AV, 14-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) & โข ((๐ โง ๐ โ ๐ด) โ ยฌ 2 โฅ ๐ต) & โข (๐ โ ยฌ 2 โฅ (โฏโ๐ด)) โ โข (๐ โ ยฌ 2 โฅ ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | pwp1fsum 16333* | The n-th power of a number increased by 1 expressed by a product with a finite sum. (Contributed by AV, 15-Aug-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ) โ โข (๐ โ (((-1โ(๐ โ 1)) ยท (๐ดโ๐)) + 1) = ((๐ด + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) | ||
Theorem | oddpwp1fsum 16334* | An odd power of a number increased by 1 expressed by a product with a finite sum. (Contributed by AV, 15-Aug-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ยฌ 2 โฅ ๐) โ โข (๐ โ ((๐ดโ๐) + 1) = ((๐ด + 1) ยท ฮฃ๐ โ (0...(๐ โ 1))((-1โ๐) ยท (๐ดโ๐)))) | ||
Theorem | divalglem0 16335 | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ โ โค & โข ๐ท โ โค โ โข ((๐ โ โค โง ๐พ โ โค) โ (๐ท โฅ (๐ โ ๐ ) โ ๐ท โฅ (๐ โ (๐ โ (๐พ ยท (absโ๐ท)))))) | ||
Theorem | divalglem1 16336 | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 โ โข 0 โค (๐ + (absโ(๐ ยท ๐ท))) | ||
Theorem | divalglem2 16337* | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 & โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} โ โข inf(๐, โ, < ) โ ๐ | ||
Theorem | divalglem4 16338* | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 & โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} โ โข ๐ = {๐ โ โ0 โฃ โ๐ โ โค ๐ = ((๐ ยท ๐ท) + ๐)} | ||
Theorem | divalglem5 16339* | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 & โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} & โข ๐ = inf(๐, โ, < ) โ โข (0 โค ๐ โง ๐ < (absโ๐ท)) | ||
Theorem | divalglem6 16340 | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ด โ โ & โข ๐ โ (0...(๐ด โ 1)) & โข ๐พ โ โค โ โข (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท ๐ด)) โ (0...(๐ด โ 1))) | ||
Theorem | divalglem7 16341 | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ท โ โค & โข ๐ท โ 0 โ โข ((๐ โ (0...((absโ๐ท) โ 1)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) | ||
Theorem | divalglem8 16342* | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 & โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} โ โข (((๐ โ ๐ โง ๐ โ ๐) โง (๐ < (absโ๐ท) โง ๐ < (absโ๐ท))) โ (๐พ โ โค โ ((๐พ ยท (absโ๐ท)) = (๐ โ ๐) โ ๐ = ๐))) | ||
Theorem | divalglem9 16343* | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 & โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} & โข ๐ = inf(๐, โ, < ) โ โข โ!๐ฅ โ ๐ ๐ฅ < (absโ๐ท) | ||
Theorem | divalglem10 16344* | Lemma for divalg 16345. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
โข ๐ โ โค & โข ๐ท โ โค & โข ๐ท โ 0 & โข ๐ = {๐ โ โ0 โฃ ๐ท โฅ (๐ โ ๐)} โ โข โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) | ||
Theorem | divalg 16345* | The division algorithm (theorem). Dividing an integer ๐ by a nonzero integer ๐ท produces a (unique) quotient ๐ and a unique remainder 0 โค ๐ < (absโ๐ท). Theorem 1.14 in [ApostolNT] p. 19. The proof does not use / or โ or mod. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ท โ โค โง ๐ท โ 0) โ โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐))) | ||
Theorem | divalgb 16346* | Express the division algorithm as stated in divalg 16345 in terms of โฅ. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ท โ โค โง ๐ท โ 0) โ (โ!๐ โ โค โ๐ โ โค (0 โค ๐ โง ๐ < (absโ๐ท) โง ๐ = ((๐ ยท ๐ท) + ๐)) โ โ!๐ โ โ0 (๐ < (absโ๐ท) โง ๐ท โฅ (๐ โ ๐)))) | ||
Theorem | divalg2 16347* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ท โ โ) โ โ!๐ โ โ0 (๐ < ๐ท โง ๐ท โฅ (๐ โ ๐))) | ||
Theorem | divalgmod 16348 | The result of the mod operator satisfies the requirements for the remainder ๐ in the division algorithm for a positive divisor (compare divalg2 16347 and divalgb 16346). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.) |
โข ((๐ โ โค โง ๐ท โ โ) โ (๐ = (๐ mod ๐ท) โ (๐ โ โ0 โง (๐ < ๐ท โง ๐ท โฅ (๐ โ ๐ ))))) | ||
Theorem | divalgmodcl 16349 | The result of the mod operator satisfies the requirements for the remainder ๐ in the division algorithm for a positive divisor. Variant of divalgmod 16348. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
โข ((๐ โ โค โง ๐ท โ โ โง ๐ โ โ0) โ (๐ = (๐ mod ๐ท) โ (๐ < ๐ท โง ๐ท โฅ (๐ โ ๐ )))) | ||
Theorem | modremain 16350* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
โข ((๐ โ โค โง ๐ท โ โ โง (๐ โ โ0 โง ๐ < ๐ท)) โ ((๐ mod ๐ท) = ๐ โ โ๐ง โ โค ((๐ง ยท ๐ท) + ๐ ) = ๐)) | ||
Theorem | ndvdssub 16351 | Corollary of the division algorithm. If an integer ๐ท greater than 1 divides ๐, then it does not divide any of ๐ โ 1, ๐ โ 2... ๐ โ (๐ท โ 1). (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ท โ โ โง (๐พ โ โ โง ๐พ < ๐ท)) โ (๐ท โฅ ๐ โ ยฌ ๐ท โฅ (๐ โ ๐พ))) | ||
Theorem | ndvdsadd 16352 | Corollary of the division algorithm. If an integer ๐ท greater than 1 divides ๐, then it does not divide any of ๐ + 1, ๐ + 2... ๐ + (๐ท โ 1). (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ท โ โ โง (๐พ โ โ โง ๐พ < ๐ท)) โ (๐ท โฅ ๐ โ ยฌ ๐ท โฅ (๐ + ๐พ))) | ||
Theorem | ndvdsp1 16353 | Special case of ndvdsadd 16352. If an integer ๐ท greater than 1 divides ๐, it does not divide ๐ + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ท โ โ โง 1 < ๐ท) โ (๐ท โฅ ๐ โ ยฌ ๐ท โฅ (๐ + 1))) | ||
Theorem | ndvdsi 16354 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ & โข ๐ โ โ0 & โข ๐ โ โ & โข ((๐ด ยท ๐) + ๐ ) = ๐ต & โข ๐ < ๐ด โ โข ยฌ ๐ด โฅ ๐ต | ||
Theorem | flodddiv4 16355 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) |
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (โโ(๐ / 4)) = if(2 โฅ ๐, (๐ / 2), ((๐ โ 1) / 2))) | ||
Theorem | fldivndvdslt 16356 | The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.) |
โข ((๐พ โ โค โง (๐ฟ โ โค โง ๐ฟ โ 0) โง ยฌ ๐ฟ โฅ ๐พ) โ (โโ(๐พ / ๐ฟ)) < (๐พ / ๐ฟ)) | ||
Theorem | flodddiv4lt 16357 | The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ (โโ(๐ / 4)) < (๐ / 4)) | ||
Theorem | flodddiv4t2lthalf 16358 | The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.) (Proof shortened by AV, 10-Jul-2022.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ ((โโ(๐ / 4)) ยท 2) < (๐ / 2)) | ||
Syntax | cbits 16359 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 16360 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 16361 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 16362* | Define the binary bits of an integer. The expression ๐ โ (bitsโ๐) means that the ๐-th bit of ๐ is 1 (and its negation means the bit is 0). (Contributed by Mario Carneiro, 4-Sep-2016.) |
โข bits = (๐ โ โค โฆ {๐ โ โ0 โฃ ยฌ 2 โฅ (โโ(๐ / (2โ๐)))}) | ||
Theorem | bitsfval 16363* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (bitsโ๐) = {๐ โ โ0 โฃ ยฌ 2 โฅ (โโ(๐ / (2โ๐)))}) | ||
Theorem | bitsval 16364 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ (bitsโ๐) โ (๐ โ โค โง ๐ โ โ0 โง ยฌ 2 โฅ (โโ(๐ / (2โ๐))))) | ||
Theorem | bitsval2 16365 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข ((๐ โ โค โง ๐ โ โ0) โ (๐ โ (bitsโ๐) โ ยฌ 2 โฅ (โโ(๐ / (2โ๐))))) | ||
Theorem | bitsss 16366 | The set of bits of an integer is a subset of โ0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (bitsโ๐) โ โ0 | ||
Theorem | bitsf 16367 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข bits:โคโถ๐ซ โ0 | ||
Theorem | bits0 16368 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (0 โ (bitsโ๐) โ ยฌ 2 โฅ ๐)) | ||
Theorem | bits0e 16369 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ ยฌ 0 โ (bitsโ(2 ยท ๐))) | ||
Theorem | bits0o 16370 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ 0 โ (bitsโ((2 ยท ๐) + 1))) | ||
Theorem | bitsp1 16371 | The ๐ + 1-th bit of ๐ is the ๐-th bit of โ(๐ / 2). (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข ((๐ โ โค โง ๐ โ โ0) โ ((๐ + 1) โ (bitsโ๐) โ ๐ โ (bitsโ(โโ(๐ / 2))))) | ||
Theorem | bitsp1e 16372 | The ๐ + 1-th bit of 2๐ is the ๐-th bit of ๐. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข ((๐ โ โค โง ๐ โ โ0) โ ((๐ + 1) โ (bitsโ(2 ยท ๐)) โ ๐ โ (bitsโ๐))) | ||
Theorem | bitsp1o 16373 | The ๐ + 1-th bit of 2๐ + 1 is the ๐-th bit of ๐. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข ((๐ โ โค โง ๐ โ โ0) โ ((๐ + 1) โ (bitsโ((2 ยท ๐) + 1)) โ ๐ โ (bitsโ๐))) | ||
Theorem | bitsfzolem 16374* | Lemma for bitsfzo 16375. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ โ0) & โข (๐ โ (bitsโ๐) โ (0..^๐)) & โข ๐ = inf({๐ โ โ0 โฃ ๐ < (2โ๐)}, โ, < ) โ โข (๐ โ ๐ โ (0..^(2โ๐))) | ||
Theorem | bitsfzo 16375 | The bits of a number are all less than ๐ iff the number is nonnegative and less than 2โ๐. (Contributed by Mario Carneiro, 5-Sep-2016.) (Proof shortened by AV, 1-Oct-2020.) |
โข ((๐ โ โค โง ๐ โ โ0) โ (๐ โ (0..^(2โ๐)) โ (bitsโ๐) โ (0..^๐))) | ||
Theorem | bitsmod 16376 | Truncating the bit sequence after some ๐ is equivalent to reducing the argument mod 2โ๐. (Contributed by Mario Carneiro, 6-Sep-2016.) |
โข ((๐ โ โค โง ๐ โ โ0) โ (bitsโ(๐ mod (2โ๐))) = ((bitsโ๐) โฉ (0..^๐))) | ||
Theorem | bitsfi 16377 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โ0 โ (bitsโ๐) โ Fin) | ||
Theorem | bitscmp 16378 | The bit complement of ๐ is -๐ โ 1. (Thus, by bitsfi 16377, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (โ0 โ (bitsโ๐)) = (bitsโ(-๐ โ 1))) | ||
Theorem | 0bits 16379 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
โข (bitsโ0) = โ | ||
Theorem | m1bits 16380 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (bitsโ-1) = โ0 | ||
Theorem | bitsinv1lem 16381 | Lemma for bitsinv1 16382. (Contributed by Mario Carneiro, 22-Sep-2016.) |
โข ((๐ โ โค โง ๐ โ โ0) โ (๐ mod (2โ(๐ + 1))) = ((๐ mod (2โ๐)) + if(๐ โ (bitsโ๐), (2โ๐), 0))) | ||
Theorem | bitsinv1 16382* | There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 16378), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.) |
โข (๐ โ โ0 โ ฮฃ๐ โ (bitsโ๐)(2โ๐) = ๐) | ||
Theorem | bitsinv2 16383* | There is an explicit inverse to the bits function for nonnegative integers, part 2. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข (๐ด โ (๐ซ โ0 โฉ Fin) โ (bitsโฮฃ๐ โ ๐ด (2โ๐)) = ๐ด) | ||
Theorem | bitsf1ocnv 16384* | The bits function restricted to nonnegative integers is a bijection from the integers to the finite sets of integers. It is in fact the inverse of the Ackermann bijection ackbijnn 15773. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข ((bits โพ โ0):โ0โ1-1-ontoโ(๐ซ โ0 โฉ Fin) โง โก(bits โพ โ0) = (๐ฅ โ (๐ซ โ0 โฉ Fin) โฆ ฮฃ๐ โ ๐ฅ (2โ๐))) | ||
Theorem | bitsf1o 16385 | The bits function restricted to nonnegative integers is a bijection from the integers to the finite sets of integers. It is in fact the inverse of the Ackermann bijection ackbijnn 15773. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข (bits โพ โ0):โ0โ1-1-ontoโ(๐ซ โ0 โฉ Fin) | ||
Theorem | bitsf1 16386 | The bits function is an injection from โค to ๐ซ โ0. It is obviously not a bijection (by Cantor's theorem canth2 9129), and in fact its range is the set of finite and cofinite subsets of โ0. (Contributed by Mario Carneiro, 22-Sep-2016.) |
โข bits:โคโ1-1โ๐ซ โ0 | ||
Theorem | 2ebits 16387 | The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โ0 โ (bitsโ(2โ๐)) = {๐}) | ||
Theorem | bitsinv 16388* | The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข ๐พ = โก(bits โพ โ0) โ โข (๐ด โ (๐ซ โ0 โฉ Fin) โ (๐พโ๐ด) = ฮฃ๐ โ ๐ด (2โ๐)) | ||
Theorem | bitsinvp1 16389 | Recursive definition of the inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข ๐พ = โก(bits โพ โ0) โ โข ((๐ด โ โ0 โง ๐ โ โ0) โ (๐พโ(๐ด โฉ (0..^(๐ + 1)))) = ((๐พโ(๐ด โฉ (0..^๐))) + if(๐ โ ๐ด, (2โ๐), 0))) | ||
Theorem | sadadd2lem2 16390 | The core of the proof of sadadd2 16400. The intuitive justification for this is that cadd is true if at least two arguments are true, and hadd is true if an odd number of arguments are true, so altogether the result is ๐ ยท ๐ด where ๐ is the number of true arguments, which is equivalently obtained by adding together one ๐ด for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข (๐ด โ โ โ (if(hadd(๐, ๐, ๐), ๐ด, 0) + if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0))) | ||
Definition | df-sad 16391* | Define the addition of two bit sequences, using df-had 1595 and df-cad 1608 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข sadd = (๐ฅ โ ๐ซ โ0, ๐ฆ โ ๐ซ โ0 โฆ {๐ โ โ0 โฃ hadd(๐ โ ๐ฅ, ๐ โ ๐ฆ, โ โ (seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ฅ, ๐ โ ๐ฆ, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1))))โ๐))}) | ||
Theorem | sadfval 16392* | Define the addition of two bit sequences, using df-had 1595 and df-cad 1608 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) โ โข (๐ โ (๐ด sadd ๐ต) = {๐ โ โ0 โฃ hadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ (๐ถโ๐))}) | ||
Theorem | sadcf 16393* | The carry sequence is a sequence of elements of 2o encoding a "sequence of wffs". (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) โ โข (๐ โ ๐ถ:โ0โถ2o) | ||
Theorem | sadc0 16394* | The initial element of the carry sequence is โฅ. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) โ โข (๐ โ ยฌ โ โ (๐ถโ0)) | ||
Theorem | sadcp1 16395* | The carry sequence (which is a sequence of wffs, encoded as 1o and โ ) is defined recursively as the carry operation applied to the previous carry and the two current inputs. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (โ โ (๐ถโ(๐ + 1)) โ cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ (๐ถโ๐)))) | ||
Theorem | sadval 16396* | The full adder sequence is the half adder function applied to the inputs and the carry sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ โ (๐ด sadd ๐ต) โ hadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ (๐ถโ๐)))) | ||
Theorem | sadcaddlem 16397* | Lemma for sadcadd 16398. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) & โข (๐ โ ๐ โ โ0) & โข ๐พ = โก(bits โพ โ0) & โข (๐ โ (โ โ (๐ถโ๐) โ (2โ๐) โค ((๐พโ(๐ด โฉ (0..^๐))) + (๐พโ(๐ต โฉ (0..^๐)))))) โ โข (๐ โ (โ โ (๐ถโ(๐ + 1)) โ (2โ(๐ + 1)) โค ((๐พโ(๐ด โฉ (0..^(๐ + 1)))) + (๐พโ(๐ต โฉ (0..^(๐ + 1))))))) | ||
Theorem | sadcadd 16398* | Non-recursive definition of the carry sequence. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) & โข (๐ โ ๐ โ โ0) & โข ๐พ = โก(bits โพ โ0) โ โข (๐ โ (โ โ (๐ถโ๐) โ (2โ๐) โค ((๐พโ(๐ด โฉ (0..^๐))) + (๐พโ(๐ต โฉ (0..^๐)))))) | ||
Theorem | sadadd2lem 16399* | Lemma for sadadd2 16400. (Contributed by Mario Carneiro, 9-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) & โข (๐ โ ๐ โ โ0) & โข ๐พ = โก(bits โพ โ0) & โข (๐ โ ((๐พโ((๐ด sadd ๐ต) โฉ (0..^๐))) + if(โ โ (๐ถโ๐), (2โ๐), 0)) = ((๐พโ(๐ด โฉ (0..^๐))) + (๐พโ(๐ต โฉ (0..^๐))))) โ โข (๐ โ ((๐พโ((๐ด sadd ๐ต) โฉ (0..^(๐ + 1)))) + if(โ โ (๐ถโ(๐ + 1)), (2โ(๐ + 1)), 0)) = ((๐พโ(๐ด โฉ (0..^(๐ + 1)))) + (๐พโ(๐ต โฉ (0..^(๐ + 1)))))) | ||
Theorem | sadadd2 16400* | Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 8-Sep-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) & โข ๐ถ = seq0((๐ โ 2o, ๐ โ โ0 โฆ if(cadd(๐ โ ๐ด, ๐ โ ๐ต, โ โ ๐), 1o, โ )), (๐ โ โ0 โฆ if(๐ = 0, โ , (๐ โ 1)))) & โข (๐ โ ๐ โ โ0) & โข ๐พ = โก(bits โพ โ0) โ โข (๐ โ ((๐พโ((๐ด sadd ๐ต) โฉ (0..^๐))) + if(โ โ (๐ถโ๐), (2โ๐), 0)) = ((๐พโ(๐ด โฉ (0..^๐))) + (๐พโ(๐ต โฉ (0..^๐))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |