P. 127 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12601-12700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvdsflip 12601*	An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.)
⊢ 𝐴 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝑁 / 𝑦))    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	dvdsssfz1 12602*	The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴))
Theorem	dvds1 12603	The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑀 ∈ ℕ0 → (𝑀 ∥ 1 ↔ 𝑀 = 1))
Theorem	alzdvds 12604*	Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (∀𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0))
Theorem	dvdsext 12605*	Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℕ0 (𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥)))
Theorem	fzm1ndvds 12606	No number between 1 and 𝑀 − 1 divides 𝑀. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ∥ 𝑁)
Theorem	fzo0dvdseq 12607	Zero is the only one of the first 𝐴 nonnegative integers that is divisible by 𝐴. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝐵 ∈ (0..^𝐴) → (𝐴 ∥ 𝐵 ↔ 𝐵 = 0))
Theorem	fzocongeq 12608	Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐷 − 𝐶) ∥ (𝐴 − 𝐵) ↔ 𝐴 = 𝐵))
Theorem	addmodlteqALT 12609	Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq 10818 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))
Theorem	dvdsfac 12610	A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁))
Theorem	dvdsexp 12611	A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ∥ (𝐴↑𝑁))
Theorem	dvdsmod 12612	Any number 𝐾 whose mod base 𝑁 is divisible by a divisor 𝑃 of the base is also divisible by 𝑃. This means that primes will also be relatively prime to the base when reduced mod 𝑁 for any base. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ (𝐾 mod 𝑁) ↔ 𝑃 ∥ 𝐾))
Theorem	mulmoddvds 12613	If an integer is divisible by a positive integer, the product of this integer with another integer modulo the positive integer is 0. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 ∥ 𝐴 → ((𝐴 · 𝐵) mod 𝑁) = 0))
Theorem	3dvds 12614*	A rule for divisibility by 3 of a number written in base 10. This is Metamath 100 proof #85. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.) (Revised by AV, 8-Sep-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))
Theorem	3dvdsdec 12615	A decimal number is divisible by three iff the sum of its two "digits" is divisible by three. The term "digits" in its narrow sense is only correct if 𝐴 and 𝐵 actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers 𝐴 and 𝐵, especially if 𝐴 is itself a decimal number, e.g., 𝐴 = ;𝐶𝐷. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (3 ∥ ;𝐴𝐵 ↔ 3 ∥ (𝐴 + 𝐵))
Theorem	3dvds2dec 12616	A decimal number is divisible by three iff the sum of its three "digits" is divisible by three. The term "digits" in its narrow sense is only correct if 𝐴, 𝐵 and 𝐶 actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers 𝐴, 𝐵 and 𝐶. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (3 ∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((𝐴 + 𝐵) + 𝐶))
5.1.2  Even and odd numbers The set ℤ of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 12620. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom 2 ∥ 𝑁 to say that "𝑁 is even" (which implies 𝑁 ∈ ℤ, see evenelz 12617) and ¬ 2 ∥ 𝑁 to say that "𝑁 is odd" (under the assumption that 𝑁 ∈ ℤ). The previously proven theorems about even and odd numbers, like zneo 9730, zeo 9734, zeo2 9735, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 12639 and oddp1d2 12640. The corresponding theorems are zeneo 12621, zeo3 12618 and zeo4 12620.
Theorem	evenelz 12617	An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 12542. (Contributed by AV, 22-Jun-2021.)
⊢ (2 ∥ 𝑁 → 𝑁 ∈ ℤ)
Theorem	zeo3 12618	An integer is even or odd. (Contributed by AV, 17-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁))
Theorem	zeoxor 12619	An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ⊻ ¬ 2 ∥ 𝑁))
Theorem	zeo4 12620	An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))
Theorem	zeneo 12621	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 9730 follows immediately from the fact that a contradiction implies anything, see pm2.21i 655. (Contributed by AV, 22-Jun-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵))
Theorem	odd2np1lem 12622*	Lemma for odd2np1 12623. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
Theorem	odd2np1 12623*	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 12624*	An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.)
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁)
Theorem	oddm1even 12625	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1)))
Theorem	oddp1even 12626	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1)))
Theorem	oexpneg 12627	The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁))
Theorem	mod2eq0even 12628	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 12629	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.)
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁))
Theorem	oddnn02np1 12630*	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 12631*	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 12632*	A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 (2 · 𝑛) = 𝑁))
Theorem	evennn2n 12633*	A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.)
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 · 𝑛) = 𝑁))
Theorem	2tp1odd 12634	A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵)
Theorem	mulsucdiv2z 12635	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 12636	A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈ ℤ)
Theorem	2teven 12637	A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵)
Theorem	zeo5 12638	An integer is either even or odd, version of zeo3 12618 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 12639	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 9734 and zeo2 9735. (Contributed by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ))
Theorem	oddp1d2 12640	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 9734 and zeo2 9735. (Contributed by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	zob 12641	Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈ ℤ))
Theorem	oddm1d2 12642	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 12643	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 12644	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 12645	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 12646	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 12647	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 12648	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 12649	Exponentiation of -1 by an even power. Variant of m1expeven 11006. (Contributed by AV, 25-Jun-2021.)
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1)
Theorem	m1expo 12650	Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1)
Theorem	m1exp1 12651	Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.)
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁))
Theorem	nn0enne 12652	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 12653	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 12654	The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ)
Theorem	nn0o1gt2 12655	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 12656	An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ((𝑁 − 1) / 2) ∈ ℕ)
Theorem	nn0o 12657	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 12658	Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nn0oddm1d2 12659	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 12660	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 12661	0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
⊢ 2 ∥ 0
Theorem	n2dvds1 12662	2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ¬ 2 ∥ 1
Theorem	n2dvdsm1 12663	2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
⊢ ¬ 2 ∥ -1
Theorem	z2even 12664	2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
⊢ 2 ∥ 2
Theorem	n2dvds3 12665	2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.)
⊢ ¬ 2 ∥ 3
Theorem	z4even 12666	4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
⊢ 2 ∥ 4
Theorem	4dvdseven 12667	An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.)
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁)
5.1.3  The division algorithm
Theorem	divalglemnn 12668*	Lemma for divalg 12674. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalglemqt 12669	Lemma for divalg 12674. The 𝑄 = 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.)
⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → 𝑅 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℤ)    &   ⊢ (𝜑 → 𝑇 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 = 𝑇)    &   ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆))    ⇒   ⊢ (𝜑 → 𝑅 = 𝑆)
Theorem	divalglemnqt 12670	Lemma for divalg 12674. The 𝑄 < 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.)
⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℤ)    &   ⊢ (𝜑 → 𝑇 ∈ ℤ)    &   ⊢ (𝜑 → 0 ≤ 𝑆)    &   ⊢ (𝜑 → 𝑅 < 𝐷)    &   ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆))    ⇒   ⊢ (𝜑 → ¬ 𝑄 < 𝑇)
Theorem	divalglemeunn 12671*	Lemma for divalg 12674. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalglemex 12672*	Lemma for divalg 12674. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalglemeuneg 12673*	Lemma for divalg 12674. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalg 12674*	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. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalgb 12675*	Express the division algorithm as stated in divalg 12674 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
Theorem	divalg2 12676*	The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)))
Theorem	divalgmod 12677	The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 12676 and divalgb 12675). 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 12678	The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 12677. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))
Theorem	modremain 12679*	The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁))
Theorem	ndvdssub 12680	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 12681	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 12682	Special case of ndvdsadd 12681. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1)))
Theorem	ndvdsi 12683	A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑄 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ    &   ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵    &   ⊢ 𝑅 < 𝐴    ⇒   ⊢ ¬ 𝐴 ∥ 𝐵
Theorem	5ndvds3 12684	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
⊢ ¬ 5 ∥ 3
Theorem	5ndvds6 12685	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
⊢ ¬ 5 ∥ 6
Theorem	flodddiv4 12686	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 12687	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 12688	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 12689	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))
5.1.4  Bit sequences
Syntax	cbits 12690	Define the binary bits of an integer.
class bits
Definition	df-bits 12691*	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 12692*	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (bits‘𝑁) = {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑚)))})
Theorem	bitsval 12693	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑀 ∈ (bits‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
Theorem	bitsval2 12694	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑𝑀)))))
Theorem	bitsss 12695	The set of bits of an integer is a subset of ℕ0. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (bits‘𝑁) ⊆ ℕ0
Theorem	bitsf 12696	The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ bits:ℤ⟶𝒫 ℕ0
Theorem	bitsdc 12697	Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → DECID 𝑀 ∈ (bits‘𝑁))
Theorem	bits0 12698	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ ¬ 2 ∥ 𝑁))
Theorem	bits0e 12699	The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → ¬ 0 ∈ (bits‘(2 · 𝑁)))
Theorem	bits0o 12700	The zeroth bit of an odd number is one. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → 0 ∈ (bits‘((2 · 𝑁) + 1)))