P. 164 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16301-16400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	m1expe 16301	Exponentiation of -1 by an even power. Variant of m1expeven 14032. (Contributed by AV, 25-Jun-2021.)
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1)
Theorem	m1expo 16302	Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1)
Theorem	m1exp1 16303	Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.)
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁))
Theorem	nn0enne 16304	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 16305	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 16306	The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ)
Theorem	nn0onn 16307	An odd nonnegative integer is positive. (Contributed by Steven Nguyen, 25-Mar-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁) → 𝑁 ∈ ℕ)
Theorem	nn0o1gt2 16308	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 16309	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 16310	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 16311	Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nn0oddm1d2 16312	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 16313	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 16314*	If every term in a sum is even, then so is the sum. (Contributed by AV, 14-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 2 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	sumodd 16315*	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 16316*	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 16317*	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 16318*	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 16319*	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 16320	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    ⇒   ⊢ ((𝑅 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐷 ∥ (𝑁 − 𝑅) → 𝐷 ∥ (𝑁 − (𝑅 − (𝐾 · (abs‘𝐷))))))
Theorem	divalglem1 16321	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    ⇒   ⊢ 0 ≤ (𝑁 + (abs‘(𝑁 · 𝐷)))
Theorem	divalglem2 16322*	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)}    ⇒   ⊢ inf(𝑆, ℝ, < ) ∈ 𝑆
Theorem	divalglem4 16323*	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)}    ⇒   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ ∃𝑞 ∈ ℤ 𝑁 = ((𝑞 · 𝐷) + 𝑟)}
Theorem	divalglem5 16324*	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)}    &   ⊢ 𝑅 = inf(𝑆, ℝ, < )    ⇒   ⊢ (0 ≤ 𝑅 ∧ 𝑅 < (abs‘𝐷))
Theorem	divalglem6 16325	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑋 ∈ (0...(𝐴 − 1))    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · 𝐴)) ∈ (0...(𝐴 − 1)))
Theorem	divalglem7 16326	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    ⇒   ⊢ ((𝑋 ∈ (0...((abs‘𝐷) − 1)) ∧ 𝐾 ∈ ℤ) → (𝐾 ≠ 0 → ¬ (𝑋 + (𝐾 · (abs‘𝐷))) ∈ (0...((abs‘𝐷) − 1))))
Theorem	divalglem8 16327*	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)}    ⇒   ⊢ (((𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑋 < (abs‘𝐷) ∧ 𝑌 < (abs‘𝐷))) → (𝐾 ∈ ℤ → ((𝐾 · (abs‘𝐷)) = (𝑌 − 𝑋) → 𝑋 = 𝑌)))
Theorem	divalglem9 16328*	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by AV, 2-Oct-2020.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)}    &   ⊢ 𝑅 = inf(𝑆, ℝ, < )    ⇒   ⊢ ∃!𝑥 ∈ 𝑆 𝑥 < (abs‘𝐷)
Theorem	divalglem10 16329*	Lemma for divalg 16330. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by AV, 2-Oct-2020.)
⊢ 𝑁 ∈ ℤ    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝑆 = {𝑟 ∈ ℕ0 ∣ 𝐷 ∥ (𝑁 − 𝑟)}    ⇒   ⊢ ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))
Theorem	divalg 16330*	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 16331*	Express the division algorithm as stated in divalg 16330 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
Theorem	divalg2 16332*	The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)))
Theorem	divalgmod 16333	The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 16332 and divalgb 16331). 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 16334	The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 16333. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))
Theorem	modremain 16335*	The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁))
Theorem	ndvdssub 16336	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 16337	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 16338	Special case of ndvdsadd 16337. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1)))
Theorem	ndvdsi 16339	A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑄 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ    &   ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵    &   ⊢ 𝑅 < 𝐴    ⇒   ⊢ ¬ 𝐴 ∥ 𝐵
Theorem	5ndvds3 16340	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
⊢ ¬ 5 ∥ 3
Theorem	5ndvds6 16341	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
⊢ ¬ 5 ∥ 6
Theorem	flodddiv4 16342	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 16343	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 16344	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 16345	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 16346	Define the binary bits of an integer.
class bits
Syntax	csad 16347	Define the sequence addition on bit sequences.
class sadd
Syntax	csmu 16348	Define the sequence multiplication on bit sequences.
class smul
Definition	df-bits 16349*	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 16350*	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))})
Theorem	bitsval 16351	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
Theorem	bitsval2 16352	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
Theorem	bitsss 16353	The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (bits‘𝑁) ⊆ ℕ0
Theorem	bitsf 16354	The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ bits:ℤ⟶𝒫 ℕ0
Theorem	bits0 16355	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁))
Theorem	bits0e 16356	The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁)))
Theorem	bits0o 16357	The zeroth bit of an odd number is one. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1)))
Theorem	bitsp1 16358	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 16359	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 16360	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 16361*	Lemma for bitsfzo 16362. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → (bits‘𝑁) ⊆ (0..^𝑀))    &   ⊢ 𝑆 = inf({𝑛 ∈ ℕ0 ∣ 𝑁 < (2↑𝑛)}, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑁 ∈ (0..^(2↑𝑀)))
Theorem	bitsfzo 16362	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 16363	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 16364	Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → (bits‘𝑁) ∈ Fin)
Theorem	bitscmp 16365	The bit complement of 𝑁 is -𝑁 − 1. (Thus, by bitsfi 16364, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (ℕ0 ∖ (bits‘𝑁)) = (bits‘(-𝑁 − 1)))
Theorem	0bits 16366	The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.)
⊢ (bits‘0) = ∅
Theorem	m1bits 16367	The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (bits‘-1) = ℕ0
Theorem	bitsinv1lem 16368	Lemma for bitsinv1 16369. (Contributed by Mario Carneiro, 22-Sep-2016.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑁 mod (2↑(𝑀 + 1))) = ((𝑁 mod (2↑𝑀)) + if(𝑀 ∈ (bits‘𝑁), (2↑𝑀), 0)))
Theorem	bitsinv1 16369*	There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 16365), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → Σ𝑛 ∈ (bits‘𝑁)(2↑𝑛) = 𝑁)
Theorem	bitsinv2 16370*	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 16371*	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 15751. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ ((bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ ◡(bits ↾ ℕ0) = (𝑥 ∈ (𝒫 ℕ0 ∩ Fin) ↦ Σ𝑛 ∈ 𝑥 (2↑𝑛)))
Theorem	bitsf1o 16372	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 15751. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ (bits ↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
Theorem	bitsf1 16373	The bits function is an injection from ℤ to 𝒫 ℕ0. It is obviously not a bijection (by Cantor's theorem canth2 9058), 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 16374	The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℕ0 → (bits‘(2↑𝑁)) = {𝑁})
Theorem	bitsinv 16375*	The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ 𝐾 = ◡(bits ↾ ℕ0)    ⇒   ⊢ (𝐴 ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘𝐴) = Σ𝑘 ∈ 𝐴 (2↑𝑘))
Theorem	bitsinvp1 16376	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 16377	The core of the proof of sadadd2 16387. 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 16378*	Define the addition of two bit sequences, using df-had 1595 and df-cad 1608 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 16379*	Define the addition of two bit sequences, using df-had 1595 and df-cad 1608 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 16380*	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 16381*	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 16382*	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 16383*	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 16384*	Lemma for sadcadd 16385. (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 16385*	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 16386*	Lemma for sadadd2 16387. (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 16387*	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 16388*	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 16389	The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
Theorem	sadcom 16390	The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴))
Theorem	saddisjlem 16391*	Lemma for sadadd 16394. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵)))
Theorem	saddisj 16392	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 16393*	Lemma for sadadd 16394. (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 16394	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 1595 and df-cad 1608. 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‘(𝐴 + 𝐵)))
Theorem	sadid1 16395	The adder sequence function has a left identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝐴 ⊆ ℕ0 → (𝐴 sadd ∅) = 𝐴)
Theorem	sadid2 16396	The adder sequence function has a right identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝐴 ⊆ ℕ0 → (∅ sadd 𝐴) = 𝐴)
Theorem	sadasslem 16397	Lemma for sadass 16398. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐶 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))
Theorem	sadass 16398	Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶)))
Theorem	sadeq 16399	Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))
Theorem	bitsres 16400	Restrict the bits of a number to an upper integer set. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((bits‘𝐴) ∩ (ℤ≥‘𝑁)) = (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁))))