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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nn0ob 16201 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
β’ (π β β0 β (((π + 1) / 2) β β0 β ((π β 1) / 2) β β0)) | ||
Theorem | nn0oddm1d2 16202 | 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 16203 | 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 16204* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) & β’ ((π β§ π β π΄) β 2 β₯ π΅) β β’ (π β 2 β₯ Ξ£π β π΄ π΅) | ||
Theorem | sumodd 16205* | 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 16206* | 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 16207* | 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 16208* | 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 16209* | 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 16210 | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ β β’ ((π β β€ β§ πΎ β β€) β (π· β₯ (π β π ) β π· β₯ (π β (π β (πΎ Β· (absβπ·)))))) | ||
Theorem | divalglem1 16211 | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 β β’ 0 β€ (π + (absβ(π Β· π·))) | ||
Theorem | divalglem2 16212* | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ inf(π, β, < ) β π | ||
Theorem | divalglem4 16213* | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ π = {π β β0 β£ βπ β β€ π = ((π Β· π·) + π)} | ||
Theorem | divalglem5 16214* | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} & β’ π = inf(π, β, < ) β β’ (0 β€ π β§ π < (absβπ·)) | ||
Theorem | divalglem6 16215 | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π΄ β β & β’ π β (0...(π΄ β 1)) & β’ πΎ β β€ β β’ (πΎ β 0 β Β¬ (π + (πΎ Β· π΄)) β (0...(π΄ β 1))) | ||
Theorem | divalglem7 16216 | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π· β β€ & β’ π· β 0 β β’ ((π β (0...((absβπ·) β 1)) β§ πΎ β β€) β (πΎ β 0 β Β¬ (π + (πΎ Β· (absβπ·))) β (0...((absβπ·) β 1)))) | ||
Theorem | divalglem8 16217* | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ (((π β π β§ π β π) β§ (π < (absβπ·) β§ π < (absβπ·))) β (πΎ β β€ β ((πΎ Β· (absβπ·)) = (π β π) β π = π))) | ||
Theorem | divalglem9 16218* | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} & β’ π = inf(π, β, < ) β β’ β!π₯ β π π₯ < (absβπ·) | ||
Theorem | divalglem10 16219* | Lemma for divalg 16220. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
β’ π β β€ & β’ π· β β€ & β’ π· β 0 & β’ π = {π β β0 β£ π· β₯ (π β π)} β β’ β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π)) | ||
Theorem | divalg 16220* | 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 16221* | Express the division algorithm as stated in divalg 16220 in terms of β₯. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π· β β€ β§ π· β 0) β (β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π)) β β!π β β0 (π < (absβπ·) β§ π· β₯ (π β π)))) | ||
Theorem | divalg2 16222* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π· β β) β β!π β β0 (π < π· β§ π· β₯ (π β π))) | ||
Theorem | divalgmod 16223 | The result of the mod operator satisfies the requirements for the remainder π in the division algorithm for a positive divisor (compare divalg2 16222 and divalgb 16221). 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 16224 | The result of the mod operator satisfies the requirements for the remainder π in the division algorithm for a positive divisor. Variant of divalgmod 16223. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
β’ ((π β β€ β§ π· β β β§ π β β0) β (π = (π mod π·) β (π < π· β§ π· β₯ (π β π )))) | ||
Theorem | modremain 16225* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
β’ ((π β β€ β§ π· β β β§ (π β β0 β§ π < π·)) β ((π mod π·) = π β βπ§ β β€ ((π§ Β· π·) + π ) = π)) | ||
Theorem | ndvdssub 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 | ndvdsadd 16227 | 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 16228 | Special case of ndvdsadd 16227. If an integer π· greater than 1 divides π, it does not divide π + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π· β β β§ 1 < π·) β (π· β₯ π β Β¬ π· β₯ (π + 1))) | ||
Theorem | ndvdsi 16229 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ π΄ β β & β’ π β β0 & β’ π β β & β’ ((π΄ Β· π) + π ) = π΅ & β’ π < π΄ β β’ Β¬ π΄ β₯ π΅ | ||
Theorem | flodddiv4 16230 | 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 16231 | 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 16232 | 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 16233 | 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 16234 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 16235 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 16236 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 16237* | 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 16238* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β (bitsβπ) = {π β β0 β£ Β¬ 2 β₯ (ββ(π / (2βπ)))}) | ||
Theorem | bitsval 16239 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β (bitsβπ) β (π β β€ β§ π β β0 β§ Β¬ 2 β₯ (ββ(π / (2βπ))))) | ||
Theorem | bitsval2 16240 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π β β€ β§ π β β0) β (π β (bitsβπ) β Β¬ 2 β₯ (ββ(π / (2βπ))))) | ||
Theorem | bitsss 16241 | The set of bits of an integer is a subset of β0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (bitsβπ) β β0 | ||
Theorem | bitsf 16242 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ bits:β€βΆπ« β0 | ||
Theorem | bits0 16243 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β (0 β (bitsβπ) β Β¬ 2 β₯ π)) | ||
Theorem | bits0e 16244 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β Β¬ 0 β (bitsβ(2 Β· π))) | ||
Theorem | bits0o 16245 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β 0 β (bitsβ((2 Β· π) + 1))) | ||
Theorem | bitsp1 16246 | 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 16247 | 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 16248 | 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 16249* | Lemma for bitsfzo 16250. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β (bitsβπ) β (0..^π)) & β’ π = inf({π β β0 β£ π < (2βπ)}, β, < ) β β’ (π β π β (0..^(2βπ))) | ||
Theorem | bitsfzo 16250 | 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 16251 | 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 16252 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β0 β (bitsβπ) β Fin) | ||
Theorem | bitscmp 16253 | The bit complement of π is -π β 1. (Thus, by bitsfi 16252, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β€ β (β0 β (bitsβπ)) = (bitsβ(-π β 1))) | ||
Theorem | 0bits 16254 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
β’ (bitsβ0) = β | ||
Theorem | m1bits 16255 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (bitsβ-1) = β0 | ||
Theorem | bitsinv1lem 16256 | Lemma for bitsinv1 16257. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ ((π β β€ β§ π β β0) β (π mod (2β(π + 1))) = ((π mod (2βπ)) + if(π β (bitsβπ), (2βπ), 0))) | ||
Theorem | bitsinv1 16257* | There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 16253), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.) |
β’ (π β β0 β Ξ£π β (bitsβπ)(2βπ) = π) | ||
Theorem | bitsinv2 16258* | 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 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 15648. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ ((bits βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin) β§ β‘(bits βΎ β0) = (π₯ β (π« β0 β© Fin) β¦ Ξ£π β π₯ (2βπ))) | ||
Theorem | bitsf1o 16260 | 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 15648. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ (bits βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin) | ||
Theorem | bitsf1 16261 | The bits function is an injection from β€ to π« β0. It is obviously not a bijection (by Cantor's theorem canth2 9008), 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 16262 | The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β β0 β (bitsβ(2βπ)) = {π}) | ||
Theorem | bitsinv 16263* | The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ πΎ = β‘(bits βΎ β0) β β’ (π΄ β (π« β0 β© Fin) β (πΎβπ΄) = Ξ£π β π΄ (2βπ)) | ||
Theorem | bitsinvp1 16264 | 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 16265 | The core of the proof of sadadd2 16275. 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 16266* | Define the addition of two bit sequences, using df-had 1596 and df-cad 1609 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 16267* | Define the addition of two bit sequences, using df-had 1596 and df-cad 1609 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 16268* | 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 16269* | 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 16270* | 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 16271* | 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 16272* | Lemma for sadcadd 16273. (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 16273* | 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 16274* | Lemma for sadadd2 16275. (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 16275* | 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 16276* | 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 16277 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) β β0) | ||
Theorem | sadcom 16278 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) = (π΅ sadd π΄)) | ||
Theorem | saddisjlem 16279* | Lemma for sadadd 16282. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β (π΄ β© π΅) = β ) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ sadd π΅) β π β (π΄ βͺ π΅))) | ||
Theorem | saddisj 16280 | 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 16281* | Lemma for sadadd 16282. (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 16282 |
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 1596 and df-cad 1609.
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 16283 | 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 16284 | 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 16285 | Lemma for sadass 16286. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β πΆ β β0) & β’ (π β π β β0) β β’ (π β (((π΄ sadd π΅) sadd πΆ) β© (0..^π)) = ((π΄ sadd (π΅ sadd πΆ)) β© (0..^π))) | ||
Theorem | sadass 16286 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ πΆ β β0) β ((π΄ sadd π΅) sadd πΆ) = (π΄ sadd (π΅ sadd πΆ))) | ||
Theorem | sadeq 16287 | 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 16288 | 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 16289 | 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 16290* | 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 16291* | 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 16292* | 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 16293* | 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 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) = β ) | ||
Theorem | smupp1 16295* | 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 16296* | Define the addition of two bit sequences, using df-had 1596 and df-cad 1609 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 16297* | 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 16298* | 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 16299 | The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ smul π΅) β β0) | ||
Theorem | smu01lem 16300* | Lemma for smu01 16301 and smu02 16302. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ ((π β§ (π β β0 β§ π β β0)) β Β¬ (π β π΄ β§ (π β π) β π΅)) β β’ (π β (π΄ smul π΅) = β ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |