Home | Metamath
Proof Explorer Theorem List (p. 158 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | halfleoddlt 15701 | An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) | ||
Theorem | opoe 15702 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵)) | ||
Theorem | omoe 15703 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 − 𝐵)) | ||
Theorem | opeo 15704 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 + 𝐵)) | ||
Theorem | omeo 15705 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 − 𝐵)) | ||
Theorem | z0even 15706 | 2 divides 0. That means 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 0 | ||
Theorem | n2dvds1 15707 | 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 | n2dvds1OLD 15708 | Obsolete version of n2dvds1 15707 as of 3-May-2023. 2 does not divide 1. That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 2 ∥ 1 | ||
Theorem | n2dvdsm1 15709 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
⊢ ¬ 2 ∥ -1 | ||
Theorem | z2even 15710 | 2 divides 2. That means 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 2 | ||
Theorem | n2dvds3 15711 | 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 | n2dvds3OLD 15712 | Obsolete version of n2dvds3 15711 as of 3-May-2023. 2 does not divide 3. That means 3 is odd. (Contributed by AV, 28-Feb-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 2 ∥ 3 | ||
Theorem | z4even 15713 | 2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
⊢ 2 ∥ 4 | ||
Theorem | 4dvdseven 15714 | 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 15715 | Exponentiation of -1 by an even power. Variant of m1expeven 13466. (Contributed by AV, 25-Jun-2021.) |
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1) | ||
Theorem | m1expo 15716 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1) | ||
Theorem | m1exp1 15717 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁)) | ||
Theorem | nn0enne 15718 | 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 15719 | 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 15720 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) | ||
Theorem | nn0onn 15721 | An odd nonnegative integer is positive. (Contributed by Steven Nguyen, 25-Mar-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁) → 𝑁 ∈ ℕ) | ||
Theorem | nn0o1gt2 15722 | 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 15723 | 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 15724 | 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 15725 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nn0oddm1d2 15726 | 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 15727 | 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 15728* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 2 ∥ 𝐵) ⇒ ⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | sumodd 15729* | 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 15730* | 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 15731* | 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 15732* | 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 15733* | 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 15734 | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ ⇒ ⊢ ((𝑅 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (𝐾 · (abs‘𝐷)))))) | ||
Theorem | divalglem1 15735 | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ 0 ≤ (𝑁 + (abs‘(𝑁 · 𝐷))) | ||
Theorem | divalglem2 15736* | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 | ||
Theorem | divalglem4 15737* | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)} | ||
Theorem | divalglem5 15738* | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ (0 ≤ 𝑅 ∧ 𝑅 < (abs‘𝐷)) | ||
Theorem | divalglem6 15739 | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑋 ∈ (0...(𝐴 − 1)) & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) | ||
Theorem | divalglem7 15740 | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) | ||
Theorem | divalglem8 15741* | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌))) | ||
Theorem | divalglem9 15742* | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ ∃!𝑥 ∈ 𝑆 𝑥 < (abs‘𝐷) | ||
Theorem | divalglem10 15743* | Lemma for divalg 15744. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) | ||
Theorem | divalg 15744* | 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 15745* | Express the division algorithm as stated in divalg 15744 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) | ||
Theorem | divalg2 15746* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) | ||
Theorem | divalgmod 15747 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 15746 and divalgb 15745). 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 15748 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 15747. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | ||
Theorem | modremain 15749* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) | ||
Theorem | ndvdssub 15750 | 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 15751 | 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 15752 | Special case of ndvdsadd 15751. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) | ||
Theorem | ndvdsi 15753 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵 & ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 | ||
Theorem | flodddiv4 15754 | 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 15755 | 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 15756 | 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 15757 | 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 15758 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 15759 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 15760 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 15761* | 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 15762* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))}) | ||
Theorem | bitsval 15763 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsval2 15764 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsss 15765 | The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘𝑁) ⊆ ℕ0 | ||
Theorem | bitsf 15766 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ bits:ℤ⟶𝒫 ℕ0 | ||
Theorem | bits0 15767 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁)) | ||
Theorem | bits0e 15768 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁))) | ||
Theorem | bits0o 15769 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1))) | ||
Theorem | bitsp1 15770 | 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 15771 | 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 15772 | 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 15773* | Lemma for bitsfzo 15774. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → (bits‘𝑁) ⊆ (0..^𝑀)) & ⊢ 𝑆 = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) ⇒ ⊢ (𝜑 → 𝑁 ∈ (0..^(2↑𝑀))) | ||
Theorem | bitsfzo 15774 | 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 15775 | 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 15776 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘𝑁) ∈ Fin) | ||
Theorem | bitscmp 15777 | The bit complement of 𝑁 is -𝑁 − 1. (Thus, by bitsfi 15776, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (ℕ0 ∖ (bits‘𝑁)) = (bits‘(-𝑁 − 1))) | ||
Theorem | 0bits 15778 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
⊢ (bits‘0) = ∅ | ||
Theorem | m1bits 15779 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘-1) = ℕ0 | ||
Theorem | bitsinv1lem 15780 | Lemma for bitsinv1 15781. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0))) | ||
Theorem | bitsinv1 15781* | There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 15777), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (bits‘𝑁)(2↑𝑛) = 𝑁) | ||
Theorem | bitsinv2 15782* | 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 15783* | 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 15173. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ ◡(bits ↾ ℕ0) = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛))) | ||
Theorem | bitsf1o 15784 | 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 15173. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) | ||
Theorem | bitsf1 15785 | The bits function is an injection from ℤ to 𝒫 ℕ0. It is obviously not a bijection (by Cantor's theorem canth2 8659), 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 15786 | The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘(2↑𝑁)) = {𝑁}) | ||
Theorem | bitsinv 15787* | The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.) |
⊢ 𝐾 = ◡(bits ↾ ℕ0) ⇒ ⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘𝐴) = Σ𝑘 ∈ 𝐴 (2↑𝑘)) | ||
Theorem | bitsinvp1 15788 | 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 15789 | The core of the proof of sadadd2 15799. 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 15790* | Define the addition of two bit sequences, using df-had 1585 and df-cad 1599 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 15791* | Define the addition of two bit sequences, using df-had 1585 and df-cad 1599 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 15792* | 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 15793* | 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 15794* | 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 15795* | 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 15796* | Lemma for sadcadd 15797. (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 15797* | 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 15798* | Lemma for sadadd2 15799. (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 15799* | 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 15800* | 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↑𝑁))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |