Home | Metamath
Proof Explorer Theorem List (p. 152 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nn0oddm1d2 15101 | A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
⊢ (𝑁 ∈ ℕ0 → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nnoddm1d2 15102 | 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 | z0even 15103 | 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 0 | ||
Theorem | n2dvds1 15104 | 2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ¬ 2 ∥ 1 | ||
Theorem | n2dvdsm1 15105 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
⊢ ¬ 2 ∥ -1 | ||
Theorem | z2even 15106 | 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 2 | ||
Theorem | n2dvds3 15107 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) |
⊢ ¬ 2 ∥ 3 | ||
Theorem | z4even 15108 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
⊢ 2 ∥ 4 | ||
Theorem | 4dvdseven 15109 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) |
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁) | ||
Theorem | sumeven 15110* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 2 ∥ 𝐵) ⇒ ⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | sumodd 15111* | 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 15112* | 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 15113* | 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 15114* | 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 15115* | 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 15116 | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ ⇒ ⊢ ((𝑅 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (𝐾 · (abs‘𝐷)))))) | ||
Theorem | divalglem1 15117 | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ 0 ≤ (𝑁 + (abs‘(𝑁 · 𝐷))) | ||
Theorem | divalglem2 15118* | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 | ||
Theorem | divalglem4 15119* | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)} | ||
Theorem | divalglem5 15120* | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ (0 ≤ 𝑅 ∧ 𝑅 < (abs‘𝐷)) | ||
Theorem | divalglem6 15121 | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑋 ∈ (0...(𝐴 − 1)) & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) | ||
Theorem | divalglem7 15122 | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) | ||
Theorem | divalglem8 15123* | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌))) | ||
Theorem | divalglem9 15124* | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ ∃!𝑥 ∈ 𝑆 𝑥 < (abs‘𝐷) | ||
Theorem | divalglem10 15125* | Lemma for divalg 15126. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) | ||
Theorem | divalg 15126* | 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 mod. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||
Theorem | divalgb 15127* | Express the division algorithm as stated in divalg 15126 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) | ||
Theorem | divalg2 15128* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) | ||
Theorem | divalgmod 15129 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 15128 and divalgb 15127). 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 | divalgmodOLD 15130* | Obsolete proof of divalgmod 15129 as of 21-Aug-2021. (Contributed by Paul Chapman, 31-Mar-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑟 = (𝑁 mod 𝐷) ↔ (𝑟 ∈ ℕ0 ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))))) | ||
Theorem | divalgmodcl 15131 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 15129. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | ||
Theorem | modremain 15132* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) | ||
Theorem | ndvdssub 15133 | 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 15134 | 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 15135 | Special case of ndvdsadd 15134. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) | ||
Theorem | ndvdsi 15136 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵 & ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 | ||
Theorem | flodddiv4 15137 | 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 15138 | 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 15139 | 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 15140 | 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.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → ((⌊‘(𝑁 / 4)) · 2) < (𝑁 / 2)) | ||
Syntax | cbits 15141 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 15142 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 15143 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 15144* | 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 15145* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))}) | ||
Theorem | bitsval 15146 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsval2 15147 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsss 15148 | The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘𝑁) ⊆ ℕ0 | ||
Theorem | bitsf 15149 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ bits:ℤ⟶𝒫 ℕ0 | ||
Theorem | bits0 15150 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁)) | ||
Theorem | bits0e 15151 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁))) | ||
Theorem | bits0o 15152 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1))) | ||
Theorem | bitsp1 15153 | 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 15154 | 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 15155 | 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 15156* | Lemma for bitsfzo 15157. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → (bits‘𝑁) ⊆ (0..^𝑀)) & ⊢ 𝑆 = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) ⇒ ⊢ (𝜑 → 𝑁 ∈ (0..^(2↑𝑀))) | ||
Theorem | bitsfzo 15157 | 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 15158 | 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 15159 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘𝑁) ∈ Fin) | ||
Theorem | bitscmp 15160 | The bit complement of 𝑁 is -𝑁 − 1. (Thus, by bitsfi 15159, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (ℕ0 ∖ (bits‘𝑁)) = (bits‘(-𝑁 − 1))) | ||
Theorem | 0bits 15161 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
⊢ (bits‘0) = ∅ | ||
Theorem | m1bits 15162 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘-1) = ℕ0 | ||
Theorem | bitsinv1lem 15163 | Lemma for bitsinv1 15164. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))) | ||
Theorem | bitsinv1 15164* | There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 15160), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (bits‘𝑁)(2↑𝑛) = 𝑁) | ||
Theorem | bitsinv2 15165* | 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 15166* | 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 14560. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ ◡(bits ↾ ℕ0) = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛))) | ||
Theorem | bitsf1o 15167 | 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 14560. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) | ||
Theorem | bitsf1 15168 | The bits function is an injection from ℤ to 𝒫 ℕ0. It is obviously not a bijection (by Cantor's theorem canth2 8113), 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 15169 | The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘(2↑𝑁)) = {𝑁}) | ||
Theorem | bitsinv 15170* | The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ 𝐾 = ◡(bits ↾ ℕ0) ⇒ ⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘𝐴) = Σ𝑘 ∈ 𝐴 (2↑𝑘)) | ||
Theorem | bitsinvp1 15171 | 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 15172 | The core of the proof of sadadd2 15182. 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 15173* | Define the addition of two bit sequences, using df-had 1533 and df-cad 1546 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ sadd = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝑥, 𝑘 ∈ 𝑦, ∅ ∈ (seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝑥, 𝑚 ∈ 𝑦, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘))}) | ||
Theorem | sadfval 15174* | Define the addition of two bit sequences, using df-had 1533 and df-cad 1546 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))}) | ||
Theorem | sadcf 15175* | The carry sequence is a sequence of elements of 2𝑜 encoding a "sequence of wffs". (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → 𝐶:ℕ0⟶2𝑜) | ||
Theorem | sadc0 15176* | The initial element of the carry sequence is ⊥. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → ¬ ∅ ∈ (𝐶‘0)) | ||
Theorem | sadcp1 15177* | The carry sequence (which is a sequence of wffs, encoded as 1𝑜 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((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) | ||
Theorem | sadval 15178* | 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((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) | ||
Theorem | sadcaddlem 15179* | Lemma for sadcadd 15180. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐾 = ◡(bits ↾ ℕ0) & ⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))) ⇒ ⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))))) | ||
Theorem | sadcadd 15180* | Non-recursive definition of the carry sequence. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐾 = ◡(bits ↾ ℕ0) ⇒ ⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))) | ||
Theorem | sadadd2lem 15181* | Lemma for sadadd2 15182. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ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 15182* | Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐾 = ◡(bits ↾ ℕ0) ⇒ ⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) | ||
Theorem | sadadd3 15183* | Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝐾 = ◡(bits ↾ ℕ0) ⇒ ⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))) | ||
Theorem | sadcl 15184 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0) | ||
Theorem | sadcom 15185 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴)) | ||
Theorem | saddisjlem 15186* | Lemma for sadadd 15189. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵))) | ||
Theorem | saddisj 15187 | 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 15188* | Lemma for sadadd 15189. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ 𝐾 = ◡(bits ↾ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁)))) | ||
Theorem | sadadd 15189 |
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 1533 and df-cad 1546.
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 15190 | 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 15191 | 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 15192 | Lemma for sadass 15193. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝐶 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) | ||
Theorem | sadass 15193 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶))) | ||
Theorem | sadeq 15194 | 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 15195 | 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 15196 | 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 15197* | 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 15198* | 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 15199* | 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 15200* | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |