Home | Metamath
Proof Explorer Theorem List (p. 150 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zeneo 14901 | No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. This variant of zneo 11336 follows immediately from the fact that a contradiction implies anything, see pm2.21i 115. (Contributed by AV, 22-Jun-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵)) | ||
Theorem | odd2np1lem 14902* | Lemma for odd2np1 14903. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) | ||
Theorem | odd2np1 14903* | An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) | ||
Theorem | even2n 14904* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁) | ||
Theorem | oddm1even 14905 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1))) | ||
Theorem | oddp1even 14906 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) | ||
Theorem | oexpneg 14907 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) | ||
Theorem | mod2eq0even 14908 | An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.) |
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 0 ↔ 2 ∥ 𝑁)) | ||
Theorem | mod2eq1n2dvds 14909 | An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see example 3 in [ApostolNT] p. 107. (Contributed by AV, 24-May-2020.) (Proof shortened by AV, 5-Jul-2020.) |
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁)) | ||
Theorem | oddnn02np1 14910* | A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.) |
⊢ (𝑁 ∈ ℕ0 → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 ((2 · 𝑛) + 1) = 𝑁)) | ||
Theorem | oddge22np1 14911* | An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ ((2 · 𝑛) + 1) = 𝑁)) | ||
Theorem | evennn02n 14912* | A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 (2 · 𝑛) = 𝑁)) | ||
Theorem | evennn2n 14913* | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 · 𝑛) = 𝑁)) | ||
Theorem | 2tp1odd 14914 | A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵) | ||
Theorem | mulsucdiv2z 14915 | An integer multiplied with its successor divided by 2 yields an integer, i.e. an integer multiplied with its successor is even. (Contributed by AV, 19-Jul-2021.) |
⊢ (𝑁 ∈ ℤ → ((𝑁 · (𝑁 + 1)) / 2) ∈ ℤ) | ||
Theorem | sqoddm1div8z 14916 | A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈ ℤ) | ||
Theorem | 2teven 14917 | A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵) | ||
Theorem | zeo5 14918 | An integer is either even or odd, version of zeo3 14899 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ 2 ∥ (𝑁 + 1))) | ||
Theorem | evend2 14919 | An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo 11339 and zeo2 11340. (Contributed by AV, 22-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ)) | ||
Theorem | oddp1d2 14920 | An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo 11339 and zeo2 11340. (Contributed by AV, 22-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℤ)) | ||
Theorem | zob 14921 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈ ℤ)) | ||
Theorem | oddm1d2 14922 | An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℤ)) | ||
Theorem | ltoddhalfle 14923 | An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) | ||
Theorem | halfleoddlt 14924 | 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 14925 | 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 14926 | 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 14927 | 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 14928 | 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 | m1expe 14929 | Exponentiation of -1 by an even power. Variant of m1expeven 12769. (Contributed by AV, 25-Jun-2021.) |
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1) | ||
Theorem | m1expo 14930 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1) | ||
Theorem | m1exp1 14931 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁)) | ||
Theorem | nn0enne 14932 | 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 14933 | The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ0) | ||
Theorem | nnehalf 14934 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) | ||
Theorem | nn0o1gt2 14935 | 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 14936 | An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ((𝑁 − 1) / 2) ∈ ℕ) | ||
Theorem | nn0o 14937 | 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 14938 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nn0oddm1d2 14939 | 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 14940 | 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 14941 | 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 0 | ||
Theorem | n2dvds1 14942 | 2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ¬ 2 ∥ 1 | ||
Theorem | n2dvdsm1 14943 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
⊢ ¬ 2 ∥ -1 | ||
Theorem | z2even 14944 | 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 2 | ||
Theorem | n2dvds3 14945 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) |
⊢ ¬ 2 ∥ 3 | ||
Theorem | z4even 14946 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
⊢ 2 ∥ 4 | ||
Theorem | 4dvdseven 14947 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) |
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁) | ||
Theorem | sumeven 14948* | If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 2 ∥ 𝐵) ⇒ ⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | sumodd 14949* | 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 14950* | 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 14951* | 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 14952* | 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 14953* | 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 14954 | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ ⇒ ⊢ ((𝑅 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (𝐾 · (abs‘𝐷)))))) | ||
Theorem | divalglem1 14955 | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ 0 ≤ (𝑁 + (abs‘(𝑁 · 𝐷))) | ||
Theorem | divalglem2 14956* | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ inf(𝑆, ℝ, < ) ∈ 𝑆 | ||
Theorem | divalglem4 14957* | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)} | ||
Theorem | divalglem5 14958* | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ (0 ≤ 𝑅 ∧ 𝑅 < (abs‘𝐷)) | ||
Theorem | divalglem6 14959 | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑋 ∈ (0...(𝐴 − 1)) & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1))) | ||
Theorem | divalglem7 14960 | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 ⇒ ⊢ ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1)))) | ||
Theorem | divalglem8 14961* | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ (((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌))) | ||
Theorem | divalglem9 14962* | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} & ⊢ 𝑅 = inf(𝑆, ℝ, < ) ⇒ ⊢ ∃!𝑥 ∈ 𝑆 𝑥 < (abs‘𝐷) | ||
Theorem | divalglem10 14963* | Lemma for divalg 14964. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.) |
⊢ 𝑁 ∈ ℤ & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐷 ≠ 0 & ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)} ⇒ ⊢ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) | ||
Theorem | divalg 14964* | 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 14965* | Express the division algorithm as stated in divalg 14964 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) | ||
Theorem | divalg2 14966* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) | ||
Theorem | divalgmod 14967 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 14966 and divalgb 14965). 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 14968* | Obsolete proof of divalgmod 14967 as of 21-Aug-2021. (Contributed by Paul Chapman, 31-Mar-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑟 = (𝑁 mod 𝐷) ↔ (𝑟 ∈ ℕ0 ∧ (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))))) | ||
Theorem | divalgmodcl 14969 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 14967. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | ||
Theorem | modremain 14970* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) | ||
Theorem | ndvdssub 14971 | 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 14972 | 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 14973 | Special case of ndvdsadd 14972. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) | ||
Theorem | ndvdsi 14974 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵 & ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 | ||
Theorem | flodddiv4 14975 | 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 14976 | 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 14977 | 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 14978 | 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 14979 | Define the binary bits of an integer. |
class bits | ||
Syntax | csad 14980 | Define the sequence addition on bit sequences. |
class sadd | ||
Syntax | csmu 14981 | Define the sequence multiplication on bit sequences. |
class smul | ||
Definition | df-bits 14982* | 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 14983* | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))}) | ||
Theorem | bitsval 14984 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsval2 14985 | Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀))))) | ||
Theorem | bitsss 14986 | The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘𝑁) ⊆ ℕ0 | ||
Theorem | bitsf 14987 | The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ bits:ℤ⟶𝒫 ℕ0 | ||
Theorem | bits0 14988 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁)) | ||
Theorem | bits0e 14989 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁))) | ||
Theorem | bits0o 14990 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1))) | ||
Theorem | bitsp1 14991 | 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 14992 | 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 14993 | 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 14994* | Lemma for bitsfzo 14995. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → (bits‘𝑁) ⊆ (0..^𝑀)) & ⊢ 𝑆 = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < ) ⇒ ⊢ (𝜑 → 𝑁 ∈ (0..^(2↑𝑀))) | ||
Theorem | bitsfzo 14995 | 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 14996 | 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 14997 | Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℕ0 → (bits‘𝑁) ∈ Fin) | ||
Theorem | bitscmp 14998 | The bit complement of 𝑁 is -𝑁 − 1. (Thus, by bitsfi 14997, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (ℕ0 ∖ (bits‘𝑁)) = (bits‘(-𝑁 − 1))) | ||
Theorem | 0bits 14999 | The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.) |
⊢ (bits‘0) = ∅ | ||
Theorem | m1bits 15000 | The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (bits‘-1) = ℕ0 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |