![]() |
Metamath
Proof Explorer Theorem List (p. 165 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | n2dvds1 16401 | 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 16402 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
⊢ ¬ 2 ∥ -1 | ||
Theorem | z2even 16403 | 2 divides 2. That means 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 2 | ||
Theorem | n2dvds3 16404 | 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 16405 | 2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
⊢ 2 ∥ 4 | ||
Theorem | 4dvdseven 16406 | 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 16407 | Exponentiation of -1 by an even power. Variant of m1expeven 14146. (Contributed by AV, 25-Jun-2021.) |
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1) | ||
Theorem | m1expo 16408 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1) | ||
Theorem | m1exp1 16409 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁)) | ||
Theorem | nn0enne 16410 | 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 16411 | 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 16412 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) | ||
Theorem | nn0onn 16413 | An odd nonnegative integer is positive. (Contributed by Steven Nguyen, 25-Mar-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁) → 𝑁 ∈ ℕ) | ||
Theorem | nn0o1gt2 16414 | 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 16415 | 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 16416 | 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 16417 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nn0oddm1d2 16418 | 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 16419 | 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 16420* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 2 ∥ 𝐵) ⇒ ⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | sumodd 16421* | 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 16422* | 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 16423* | 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 16424* | 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 16425* | 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 16426 | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ ⇒ ⊢ ((𝑅 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (𝐾 · (abs‘𝐷)))))) | ||
Theorem | divalglem1 16427 | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ 0 ≤ (𝑁 + (abs‘(𝑁 · 𝐷))) | ||
Theorem | divalglem2 16428* | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 | ||
Theorem | divalglem4 16429* | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)} | ||
Theorem | divalglem5 16430* | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ (0 ≤ 𝑅 ∧ 𝑅 < (abs‘𝐷)) | ||
Theorem | divalglem6 16431 | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑋 ∈ (0...(𝐴 − 1)) & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) | ||
Theorem | divalglem7 16432 | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) | ||
Theorem | divalglem8 16433* | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌))) | ||
Theorem | divalglem9 16434* | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ ∃!𝑥 ∈ 𝑆 𝑥 < (abs‘𝐷) | ||
Theorem | divalglem10 16435* | Lemma for divalg 16436. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) | ||
Theorem | divalg 16436* | 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 16437* | Express the division algorithm as stated in divalg 16436 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) | ||
Theorem | divalg2 16438* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) | ||
Theorem | divalgmod 16439 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 16438 and divalgb 16437). 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 16440 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 16439. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | ||
Theorem | modremain 16441* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) | ||
Theorem | ndvdssub 16442 | 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 16443 | 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 16444 | Special case of ndvdsadd 16443. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) | ||
Theorem | ndvdsi 16445 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵 & ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 | ||
Theorem | 5ndvds3 16446 | 5 does not divide 3. (Contributed by AV, 8-Sep-2025.) |
⊢ ¬ 5 ∥ 3 | ||
Theorem | 5ndvds6 16447 | 5 does not divide 6. (Contributed by AV, 8-Sep-2025.) |
⊢ ¬ 5 ∥ 6 | ||
Theorem | flodddiv4 16448 | 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 16449 | 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 16450 | 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 16451 | 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 16452 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 16453 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 16454 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 16455* | 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 16456* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))}) | ||
Theorem | bitsval 16457 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsval2 16458 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsss 16459 | The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘𝑁) ⊆ ℕ0 | ||
Theorem | bitsf 16460 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ bits:ℤ⟶𝒫 ℕ0 | ||
Theorem | bits0 16461 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁)) | ||
Theorem | bits0e 16462 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁))) | ||
Theorem | bits0o 16463 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1))) | ||
Theorem | bitsp1 16464 | 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 16465 | 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 16466 | 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 16467* | Lemma for bitsfzo 16468. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → (bits‘𝑁) ⊆ (0..^𝑀)) & ⊢ 𝑆 = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) ⇒ ⊢ (𝜑 → 𝑁 ∈ (0..^(2↑𝑀))) | ||
Theorem | bitsfzo 16468 | 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 16469 | 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 16470 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘𝑁) ∈ Fin) | ||
Theorem | bitscmp 16471 | The bit complement of 𝑁 is -𝑁 − 1. (Thus, by bitsfi 16470, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (ℕ0 ∖ (bits‘𝑁)) = (bits‘(-𝑁 − 1))) | ||
Theorem | 0bits 16472 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
⊢ (bits‘0) = ∅ | ||
Theorem | m1bits 16473 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘-1) = ℕ0 | ||
Theorem | bitsinv1lem 16474 | Lemma for bitsinv1 16475. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))) | ||
Theorem | bitsinv1 16475* | There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 16471), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (bits‘𝑁)(2↑𝑛) = 𝑁) | ||
Theorem | bitsinv2 16476* | 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 16477* | 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 15860. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ ◡(bits ↾ ℕ0) = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛))) | ||
Theorem | bitsf1o 16478 | 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 15860. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) | ||
Theorem | bitsf1 16479 | The bits function is an injection from ℤ to 𝒫 ℕ0. It is obviously not a bijection (by Cantor's theorem canth2 9168), 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 16480 | The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘(2↑𝑁)) = {𝑁}) | ||
Theorem | bitsinv 16481* | The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ 𝐾 = ◡(bits ↾ ℕ0) ⇒ ⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘𝐴) = Σ𝑘 ∈ 𝐴 (2↑𝑘)) | ||
Theorem | bitsinvp1 16482 | 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 16483 | The core of the proof of sadadd2 16493. 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 16484* | Define the addition of two bit sequences, using df-had 1590 and df-cad 1603 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 16485* | Define the addition of two bit sequences, using df-had 1590 and df-cad 1603 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 16486* | 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 16487* | 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 16488* | 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 16489* | 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 16490* | Lemma for sadcadd 16491. (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 16491* | 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 16492* | Lemma for sadadd2 16493. (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 16493* | 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 16494* | 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 16495 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0) | ||
Theorem | sadcom 16496 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴)) | ||
Theorem | saddisjlem 16497* | Lemma for sadadd 16500. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵))) | ||
Theorem | saddisj 16498 | 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 16499* | Lemma for sadadd 16500. (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 16500 |
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 1590 and df-cad 1603.
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‘(𝐴 + 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |