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 12673 and zeo2 12674. (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 12673 and zeo2 12674. (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 14136. (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	5ndvds3 16461	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
⊢ ¬ 5 ∥ 3
Theorem	5ndvds6 16462	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
⊢ ¬ 5 ∥ 6
Theorem	flodddiv4 16463	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 16464	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 16465	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 16466	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 16467	Define the binary bits of an integer.
class bits
Syntax	csad 16468	Define the sequence addition on bit sequences.
class sadd
Syntax	csmu 16469	Define the sequence multiplication on bit sequences.
class smul
Definition	df-bits 16470*	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 16471*	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))})
Theorem	bitsval 16472	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
Theorem	bitsval2 16473	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
Theorem	bitsss 16474	The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (bits‘𝑁) ⊆ ℕ0
Theorem	bitsf 16475	The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ bits:ℤ⟶𝒫 ℕ0
Theorem	bits0 16476	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁))
Theorem	bits0e 16477	The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁)))
Theorem	bits0o 16478	The zeroth bit of an odd number is one. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1)))
Theorem	bitsp1 16479	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 16480	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 16481	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 16482*	Lemma for bitsfzo 16483. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → (bits‘𝑁) ⊆ (0..^𝑀))    &   ⊢ 𝑆 = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑁 ∈ (0..^(2↑𝑀)))
Theorem	bitsfzo 16483	The bits of a number are all at positions 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 16484	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 16485	Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → (bits‘𝑁) ∈ Fin)
Theorem	bitscmp 16486	The bit complement of 𝑁 is -𝑁 − 1. (Thus, by bitsfi 16485, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (ℕ0 ∖ (bits‘𝑁)) = (bits‘(-𝑁 − 1)))
Theorem	0bits 16487	The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.)
⊢ (bits‘0) = ∅
Theorem	m1bits 16488	The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (bits‘-1) = ℕ0
Theorem	bitsinv1lem 16489	Lemma for bitsinv1 16490. (Contributed by Mario Carneiro, 22-Sep-2016.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
Theorem	bitsinv1 16490*	There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 16486), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (bits‘𝑁)(2↑𝑛) = 𝑁)
Theorem	bitsinv2 16491*	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 16492*	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 15872. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ ◡(bits ↾ ℕ0) = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛)))
Theorem	bitsf1o 16493	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 15872. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
Theorem	bitsf1 16494	The bits function is an injection from ℤ to 𝒫 ℕ0. It is obviously not a bijection (by Cantor's theorem canth2 9106), 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 16495	The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → (bits‘(2↑𝑁)) = {𝑁})
Theorem	bitsinv 16496*	The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ 𝐾 = ◡(bits ↾ ℕ0)    ⇒   ⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘𝐴) = Σ𝑘 ∈ 𝐴 (2↑𝑘))
Theorem	bitsinvp1 16497	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 16498	The core of the proof of sadadd2 16508. 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 16499*	Define the addition of two bit sequences, using df-had 1617 and df-cad 1630 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 16500*	Define the addition of two bit sequences, using df-had 1617 and df-cad 1630 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    ⇒   ⊢ (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘 ∈ 𝐴, 𝑘 ∈ 𝐵, ∅ ∈ (𝐶‘𝑘))})