P. 165 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16401-16500   *Has distinct variable group(s)

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