Home | Metamath
Proof Explorer Theorem List (p. 163 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nn0oddm1d2 16201 | 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 16202 | 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 16203* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) & β’ ((π β§ π β π΄) β 2 β₯ π΅) β β’ (π β 2 β₯ Ξ£π β π΄ π΅) | ||
Theorem | sumodd 16204* | 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 16205* | 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 16206* | 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 16207* | 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 16208* | 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 16209 | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ β β’ ((π β β€ β§ πΎ β β€) β (π· β₯ (π β π ) β π· β₯ (π β (π β (πΎ Β· (absβπ·)))))) | ||
Theorem | divalglem1 16210 | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 β β’ 0 β€ (π + (absβ(π Β· π·))) | ||
Theorem | divalglem2 16211* | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ inf(π, β, < ) β π | ||
Theorem | divalglem4 16212* | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ π = {π β β0 β£ βπ β β€ π = ((π Β· π·) + π)} | ||
Theorem | divalglem5 16213* | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} & β’ π = inf(π, β, < ) β β’ (0 β€ π β§ π < (absβπ·)) | ||
Theorem | divalglem6 16214 | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π΄ β β & β’ π β (0...(π΄ β 1)) & β’ πΎ β β€ β β’ (πΎ β 0 β Β¬ (π + (πΎ Β· π΄)) β (0...(π΄ β 1))) | ||
Theorem | divalglem7 16215 | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π· β β€ & β’ π· β 0 β β’ ((π β (0...((absβπ·) β 1)) β§ πΎ β β€) β (πΎ β 0 β Β¬ (π + (πΎ Β· (absβπ·))) β (0...((absβπ·) β 1)))) | ||
Theorem | divalglem8 16216* | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ (((π β π β§ π β π) β§ (π < (absβπ·) β§ π < (absβπ·))) β (πΎ β β€ β ((πΎ Β· (absβπ·)) = (π β π) β π = π))) | ||
Theorem | divalglem9 16217* | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} & β’ π = inf(π, β, < ) β β’ β!π₯ β π π₯ < (absβπ·) | ||
Theorem | divalglem10 16218* | Lemma for divalg 16219. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π)) | ||
Theorem | divalg 16219* | 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 16220* | Express the division algorithm as stated in divalg 16219 in terms of β₯. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π· β β€ β§ π· β 0) β (β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π)) β β!π β β0 (π < (absβπ·) β§ π· β₯ (π β π)))) | ||
Theorem | divalg2 16221* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π· β β) β β!π β β0 (π < π· β§ π· β₯ (π β π))) | ||
Theorem | divalgmod 16222 | The result of the mod operator satisfies the requirements for the remainder π in the division algorithm for a positive divisor (compare divalg2 16221 and divalgb 16220). 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 16223 | The result of the mod operator satisfies the requirements for the remainder π in the division algorithm for a positive divisor. Variant of divalgmod 16222. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
β’ ((π β β€ β§ π· β β β§ π β β0) β (π = (π mod π·) β (π < π· β§ π· β₯ (π β π )))) | ||
Theorem | modremain 16224* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
β’ ((π β β€ β§ π· β β β§ (π β β0 β§ π < π·)) β ((π mod π·) = π β βπ§ β β€ ((π§ Β· π·) + π ) = π)) | ||
Theorem | ndvdssub 16225 | 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 16226 | 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 16227 | Special case of ndvdsadd 16226. If an integer π· greater than 1 divides π, it does not divide π + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π· β β β§ 1 < π·) β (π· β₯ π β Β¬ π· β₯ (π + 1))) | ||
Theorem | ndvdsi 16228 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ π΄ β β & β’ π β β0 & β’ π β β & β’ ((π΄ Β· π) + π ) = π΅ & β’ π < π΄ β β’ Β¬ π΄ β₯ π΅ | ||
Theorem | flodddiv4 16229 | 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 16230 | 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 16231 | 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 16232 | 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 16233 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 16234 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 16235 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 16236* | 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 16237* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β (bitsβπ) = {π β β0 β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) | ||
Theorem | bitsval 16238 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β (bitsβπ) β (π β β€ β§ π β β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) | ||
Theorem | bitsval2 16239 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π β β€ β§ π β β0) β (π β (bitsβπ) β Β¬ 2 β₯ (ββ(π / (2βπ))))) | ||
Theorem | bitsss 16240 | The set of bits of an integer is a subset of β0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (bitsβπ) β β0 | ||
Theorem | bitsf 16241 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ bits:β€βΆπ« β0 | ||
Theorem | bits0 16242 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β (0 β (bitsβπ) β Β¬ 2 β₯ π)) | ||
Theorem | bits0e 16243 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β Β¬ 0 β (bitsβ(2 Β· π))) | ||
Theorem | bits0o 16244 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β 0 β (bitsβ((2 Β· π) + 1))) | ||
Theorem | bitsp1 16245 | 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 16246 | 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 16247 | 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 16248* | Lemma for bitsfzo 16249. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β (bitsβπ) β (0..^π)) & β’ π = inf({π β β0 β£ π < (2βπ)}, β, < ) β β’ (π β π β (0..^(2βπ))) | ||
Theorem | bitsfzo 16249 | 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 16250 | 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 16251 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β0 β (bitsβπ) β Fin) | ||
Theorem | bitscmp 16252 | The bit complement of π is -π β 1. (Thus, by bitsfi 16251, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β (β0 β (bitsβπ)) = (bitsβ(-π β 1))) | ||
Theorem | 0bits 16253 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
β’ (bitsβ0) = β | ||
Theorem | m1bits 16254 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (bitsβ-1) = β0 | ||
Theorem | bitsinv1lem 16255 | Lemma for bitsinv1 16256. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ ((π β β€ β§ π β β0) β (π mod (2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) | ||
Theorem | bitsinv1 16256* | There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 16252), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.) |
β’ (π β β0 β Ξ£π β (bitsβπ)(2βπ) = π) | ||
Theorem | bitsinv2 16257* | 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 16258* | 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 15647. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ ((bits βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin) β§ β‘(bits βΎ β0) = (π₯ β (π« β0 β© Fin) β¦ Ξ£π β π₯ (2βπ))) | ||
Theorem | bitsf1o 16259 | 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 15647. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ (bits βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin) | ||
Theorem | bitsf1 16260 | The bits function is an injection from β€ to π« β0. It is obviously not a bijection (by Cantor's theorem canth2 9007), 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 16261 | The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β0 β (bitsβ(2βπ)) = {π}) | ||
Theorem | bitsinv 16262* | The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ πΎ = β‘(bits βΎ β0) β β’ (π΄ β (π« β0 β© Fin) β (πΎβπ΄) = Ξ£π β π΄ (2βπ)) | ||
Theorem | bitsinvp1 16263 | 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 16264 | The core of the proof of sadadd2 16274. 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 16265* | 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 16266* | 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 16267* | 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 16268* | 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 16269* | 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 16270* | 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 16271* | Lemma for sadcadd 16272. (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 16272* | 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 16273* | Lemma for sadadd2 16274. (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 16274* | 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..^π))))) | ||
Theorem | sadadd3 16275* | Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ πΎ = β‘(bits βΎ β0) β β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) mod (2βπ)) = (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) mod (2βπ))) | ||
Theorem | sadcl 16276 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) β β0) | ||
Theorem | sadcom 16277 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) = (π΅ sadd π΄)) | ||
Theorem | saddisjlem 16278* | Lemma for sadadd 16281. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β (π΄ β© π΅) = β ) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ sadd π΅) β π β (π΄ βͺ π΅))) | ||
Theorem | saddisj 16279 | The sum of disjoint sequences is the union of the sequences. (In this case, there are no carried bits.) (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β (π΄ β© π΅) = β ) β β’ (π β (π΄ sadd π΅) = (π΄ βͺ π΅)) | ||
Theorem | sadaddlem 16280* | Lemma for sadadd 16281. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β (bitsβπ΄), π β (bitsβπ΅), β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ πΎ = β‘(bits βΎ β0) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) β β’ (π β (((bitsβπ΄) sadd (bitsβπ΅)) β© (0..^π)) = (bitsβ((π΄ + π΅) mod (2βπ)))) | ||
Theorem | sadadd 16281 |
For sequences that correspond to valid integers, the adder sequence
function produces the sequence for the sum. This is effectively a proof
of the correctness of the ripple carry adder, implemented with logic
gates corresponding to df-had 1595 and df-cad 1608.
It is interesting to consider in what sense the sadd function can be said to be "adding" things outside the range of the bits function, that is, when adding sequences that are not eventually constant and so do not denote any integer. The correct interpretation is that the sequences are representations of 2-adic integers, which have a natural ring structure. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((bitsβπ΄) sadd (bitsβπ΅)) = (bitsβ(π΄ + π΅))) | ||
Theorem | sadid1 16282 | The adder sequence function has a left identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π΄ β β0 β (π΄ sadd β ) = π΄) | ||
Theorem | sadid2 16283 | The adder sequence function has a right identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π΄ β β0 β (β sadd π΄) = π΄) | ||
Theorem | sadasslem 16284 | Lemma for sadass 16285. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β πΆ β β0) & β’ (π β π β β0) β β’ (π β (((π΄ sadd π΅) sadd πΆ) β© (0..^π)) = ((π΄ sadd (π΅ sadd πΆ)) β© (0..^π))) | ||
Theorem | sadass 16285 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ πΆ β β0) β ((π΄ sadd π΅) sadd πΆ) = (π΄ sadd (π΅ sadd πΆ))) | ||
Theorem | sadeq 16286 | Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β0) β β’ (π β ((π΄ sadd π΅) β© (0..^π)) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) | ||
Theorem | bitsres 16287 | Restrict the bits of a number to an upper integer set. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β€ β§ π β β0) β ((bitsβπ΄) β© (β€β₯βπ)) = (bitsβ((ββ(π΄ / (2βπ))) Β· (2βπ)))) | ||
Theorem | bitsuz 16288 | The bits of a number are all at least π iff the number is divisible by 2βπ. (Contributed by Mario Carneiro, 21-Sep-2016.) |
β’ ((π΄ β β€ β§ π β β0) β ((2βπ) β₯ π΄ β (bitsβπ΄) β (β€β₯βπ))) | ||
Theorem | bitsshft 16289* | Shifting a bit sequence to the left (toward the more significant bits) causes the number to be multiplied by a power of two. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ ((π΄ β β€ β§ π β β0) β {π β β0 β£ (π β π) β (bitsβπ΄)} = (bitsβ(π΄ Β· (2βπ)))) | ||
Definition | df-smu 16290* | Define the multiplication of two bit sequences, using repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ smul = (π₯ β π« β0, π¦ β π« β0 β¦ {π β β0 β£ π β (seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π₯ β§ (π β π) β π¦)})), (π β β0 β¦ if(π = 0, β , (π β 1))))β(π + 1))}) | ||
Theorem | smufval 16291* | The multiplication of two bit sequences as repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β (π΄ smul π΅) = {π β β0 β£ π β (πβ(π + 1))}) | ||
Theorem | smupf 16292* | The sequence of partial sums of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β π:β0βΆπ« β0) | ||
Theorem | smup0 16293* | The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β (πβ0) = β ) | ||
Theorem | smupp1 16294* | The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (πβ(π + 1)) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) | ||
Theorem | smuval 16295* | Define the addition of two bit sequences, using df-had 1595 and df-cad 1608 bit operations. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ smul π΅) β π β (πβ(π + 1)))) | ||
Theorem | smuval2 16296* | The partial sum sequence stabilizes at π after the π + 1-th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ (π β π β (β€β₯β(π + 1))) β β’ (π β (π β (π΄ smul π΅) β π β (πβπ))) | ||
Theorem | smupvallem 16297* | If π΄ only has elements less than π, then all elements of the partial sum sequence past π already equal the final value. (Contributed by Mario Carneiro, 20-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ (π β π΄ β (0..^π)) & β’ (π β π β (β€β₯βπ)) β β’ (π β (πβπ) = (π΄ smul π΅)) | ||
Theorem | smucl 16298 | The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ smul π΅) β β0) | ||
Theorem | smu01lem 16299* | Lemma for smu01 16300 and smu02 16301. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ ((π β§ (π β β0 β§ π β β0)) β Β¬ (π β π΄ β§ (π β π) β π΅)) β β’ (π β (π΄ smul π΅) = β ) | ||
Theorem | smu01 16300 | Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π΄ β β0 β (π΄ smul β ) = β ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |