P. 140 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13901-14000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulmod0 13901	The product of an integer and a positive real number is 0 modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) (Revised by AV, 5-Jul-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → ((𝐴 · 𝑀) mod 𝑀) = 0)
Theorem	negmod0 13902	𝐴 is divisible by 𝐵 iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ (-𝐴 mod 𝐵) = 0))
Theorem	modge0 13903	The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵))
Theorem	modlt 13904	The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵)
Theorem	modelico 13905	Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵))
Theorem	moddiffl 13906	Value of the modulo operation rewritten to give two ways of expressing the quotient when "𝐴 is divided by 𝐵 using Euclidean division." Multiplying both sides by 𝐵, this implies that 𝐴 mod 𝐵 differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 6-Sep-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) = (⌊‘(𝐴 / 𝐵)))
Theorem	moddifz 13907	The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ)
Theorem	modfrac 13908	The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴)))
Theorem	flmod 13909	The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1)))
Theorem	intfrac 13910	Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.)
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1)))
Theorem	zmod10 13911	An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0)
Theorem	zmod1congr 13912	Two arbitrary integers are congruent modulo 1, see example 4 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 mod 1) = (𝐵 mod 1))
Theorem	modmulnn 13913	Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by NM, 2-Jan-2009.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀)))
Theorem	modvalp1 13914	The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 + 𝐵) − (((⌊‘(𝐴 / 𝐵)) + 1) · 𝐵)) = (𝐴 mod 𝐵))
Theorem	zmodcl 13915	Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ ℕ0)
Theorem	zmodcld 13916	Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℕ0)
Theorem	zmodfz 13917	An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...(𝐵 − 1)))
Theorem	zmodfzo 13918	An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0..^𝐵))
Theorem	zmodfzp1 13919	An integer mod 𝐵 lies in the first 𝐵 + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...𝐵))
Theorem	modid 13920	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴)
Theorem	modid0 13921	A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.)
⊢ (𝑁 ∈ ℝ+ → (𝑁 mod 𝑁) = 0)
Theorem	modid2 13922	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 𝐴 ↔ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	zmodid2 13923	Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0...(𝑁 − 1))))
Theorem	zmodidfzo 13924	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0..^𝑁)))
Theorem	zmodidfzoimp 13925	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
⊢ (𝑀 ∈ (0..^𝑁) → (𝑀 mod 𝑁) = 𝑀)
Theorem	0mod 13926	Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014.)
⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0)
Theorem	1mod 13927	Special case: 1 modulo a real number greater than 1 is 1. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
Theorem	modabs 13928	Absorption law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) ∧ 𝐵 ≤ 𝐶) → ((𝐴 mod 𝐵) mod 𝐶) = (𝐴 mod 𝐵))
Theorem	modabs2 13929	Absorption law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modcyc 13930	The modulo operation is periodic. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modcyc2 13931	The modulo operation is periodic. (Contributed by NM, 12-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 − (𝐵 · 𝑁)) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modadd1 13932	Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))
Theorem	modaddb 13933	Addition property of the modulo operation. Biconditional version of modadd1 13932 by applying modadd1 13932 twice. (Contributed by AV, 14-Nov-2025.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+)) → ((𝐴 mod 𝐷) = (𝐵 mod 𝐷) ↔ ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)))
Theorem	modaddid 13934	The sums of two nonnegative integers less than the modulus and an integer are equal iff the two nonnegative integers are equal. (Contributed by AV, 14-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) ∧ 𝐾 ∈ ℤ) → (((𝑋 + 𝐾) mod 𝑁) = ((𝑌 + 𝐾) mod 𝑁) ↔ 𝑋 = 𝑌))
Theorem	modaddabs 13935	Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶))
Theorem	modaddmod 13936	The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) + 𝐵) mod 𝑀) = ((𝐴 + 𝐵) mod 𝑀))
Theorem	muladdmodid 13937	The sum of a positive real number less than an upper bound and the product of an integer and the upper bound is the positive real number modulo the upper bound. (Contributed by AV, 5-Jul-2020.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ∧ 𝐴 ∈ (0[,)𝑀)) → (((𝑁 · 𝑀) + 𝐴) mod 𝑀) = 𝐴)
Theorem	mulp1mod1 13938	The product of an integer and an integer greater than 1 increased by 1 is 1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘2)) → (((𝑁 · 𝐴) + 1) mod 𝑁) = 1)
Theorem	muladdmod 13939	A real number is the sum of the number and a multiple of a positive real number modulo the positive real number. (Contributed by AV, 7-Sep-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (((𝑁 · 𝑀) + 𝐴) mod 𝑀) = (𝐴 mod 𝑀))
Theorem	modmuladd 13940*	Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵)))
Theorem	modmuladdim 13941*	Implication of a decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵)))
Theorem	modmuladdnn0 13942*	Implication of a decomposition of a nonnegative integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵)))
Theorem	negmod 13943	The negation of a number modulo a positive number is equal to the difference of the modulus and the number modulo the modulus. (Contributed by AV, 5-Jul-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (-𝐴 mod 𝑁) = ((𝑁 − 𝐴) mod 𝑁))
Theorem	m1modnnsub1 13944	Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑀 ∈ ℕ → (-1 mod 𝑀) = (𝑀 − 1))
Theorem	m1modge3gt1 13945	Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑀 ∈ (ℤ≥‘3) → 1 < (-1 mod 𝑀))
Theorem	addmodid 13946	The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by Alexander van der Vekens, 30-Oct-2018.) (Proof shortened by AV, 5-Jul-2020.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀) → ((𝑀 + 𝐴) mod 𝑀) = 𝐴)
Theorem	addmodidr 13947	The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀) → ((𝐴 + 𝑀) mod 𝑀) = 𝐴)
Theorem	modadd2mod 13948	The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀))
Theorem	modm1p1mod0 13949	If a real number modulo a positive real number equals the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals 0. (Contributed by AV, 2-Nov-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = (𝑀 − 1) → ((𝐴 + 1) mod 𝑀) = 0))
Theorem	modltm1p1mod 13950	If a real number modulo a positive real number is less than the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals the real number modulo the positive real number increased by 1. (Contributed by AV, 2-Nov-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ (𝐴 mod 𝑀) < (𝑀 − 1)) → ((𝐴 + 1) mod 𝑀) = ((𝐴 mod 𝑀) + 1))
Theorem	modmul1 13951	Multiplication property of the modulo operation. Note that the multiplier 𝐶 must be an integer. (Contributed by NM, 12-Nov-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 · 𝐶) mod 𝐷) = ((𝐵 · 𝐶) mod 𝐷))
Theorem	modmul12d 13952	Multiplication property of the modulo operation, see theorem 5.2(b) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 5-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) mod 𝐸) = ((𝐵 · 𝐷) mod 𝐸))
Theorem	modnegd 13953	Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐶) = (𝐵 mod 𝐶))    ⇒   ⊢ (𝜑 → (-𝐴 mod 𝐶) = (-𝐵 mod 𝐶))
Theorem	modadd12d 13954	Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐸) = ((𝐵 + 𝐷) mod 𝐸))
Theorem	modsub12d 13955	Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) mod 𝐸) = ((𝐵 − 𝐷) mod 𝐸))
Theorem	modsubmod 13956	The difference of a real number modulo a positive real number and another real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) − 𝐵) mod 𝑀) = ((𝐴 − 𝐵) mod 𝑀))
Theorem	modsubmodmod 13957	The difference of a real number modulo a positive real number and another real number modulo this positive real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) − (𝐵 mod 𝑀)) mod 𝑀) = ((𝐴 − 𝐵) mod 𝑀))
Theorem	2txmodxeq0 13958	Two times a positive real number modulo the real number is zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝑋 ∈ ℝ+ → ((2 · 𝑋) mod 𝑋) = 0)
Theorem	2submod 13959	If a real number is between a positive real number and twice the positive real number, the real number modulo the positive real number equals the real number minus the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < (2 · 𝐵))) → (𝐴 mod 𝐵) = (𝐴 − 𝐵))
Theorem	modifeq2int 13960	If a nonnegative integer is less than twice a positive integer, the nonnegative integer modulo the positive integer equals the nonnegative integer or the nonnegative integer minus the positive integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < (2 · 𝐵)) → (𝐴 mod 𝐵) = if(𝐴 < 𝐵, 𝐴, (𝐴 − 𝐵)))
Theorem	modaddmodup 13961	The sum of an integer modulo a positive integer and another integer minus the positive integer equals the sum of the two integers modulo the positive integer if the other integer is in the upper part of the range between 0 and the positive integer. (Contributed by AV, 30-Oct-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + 𝐴) mod 𝑀)))
Theorem	modaddmodlo 13962	The sum of an integer modulo a positive integer and another integer equals the sum of the two integers modulo the positive integer if the other integer is in the lower part of the range between 0 and the positive integer. (Contributed by AV, 30-Oct-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → (𝐵 + (𝐴 mod 𝑀)) = ((𝐵 + 𝐴) mod 𝑀)))
Theorem	modmulmod 13963	The product of a real number modulo a positive real number and an integer equals the product of the real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) · 𝐵) mod 𝑀) = ((𝐴 · 𝐵) mod 𝑀))
Theorem	modmulmodr 13964	The product of an integer and a real number modulo a positive real number equals the product of the integer and the real number modulo the positive real number. (Contributed by Alexander van der Vekens, 9-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → ((𝐴 · (𝐵 mod 𝑀)) mod 𝑀) = ((𝐴 · 𝐵) mod 𝑀))
Theorem	modaddmulmod 13965	The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℤ) ∧ 𝑀 ∈ ℝ+) → ((𝐴 + ((𝐵 mod 𝑀) · 𝐶)) mod 𝑀) = ((𝐴 + (𝐵 · 𝐶)) mod 𝑀))
Theorem	moddi 13966	Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (𝐴 · (𝐵 mod 𝐶)) = ((𝐴 · 𝐵) mod (𝐴 · 𝐶)))
Theorem	modsubdir 13967	Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → ((𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))))
Theorem	modeqmodmin 13968	A real number equals the difference of the real number and a positive real number modulo the positive real number. (Contributed by AV, 3-Nov-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (𝐴 mod 𝑀) = ((𝐴 − 𝑀) mod 𝑀))
Theorem	modirr 13969	A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐴 / 𝐵) ∈ (ℝ ∖ ℚ)) → (𝐴 mod 𝐵) ≠ 0)
Theorem	modfzo0difsn 13970*	For a number within a half-open range of nonnegative integers with one excluded integer there is a positive integer so that the number is equal to the sum of the positive integer and the excluded integer modulo the upper bound of the range. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁))
Theorem	modsumfzodifsn 13971	The sum of a number within a half-open range of positive integers is an element of the corresponding open range of nonnegative integers with one excluded integer modulo the excluded integer. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽}))
Theorem	modlteq 13972	Two nonnegative integers less than the modulus are equal iff they are equal modulo the modulus. (Contributed by AV, 14-Mar-2021.)
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 mod 𝑁) = (𝐽 mod 𝑁) ↔ 𝐼 = 𝐽))
Theorem	addmodlteq 13973	Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. A much shorter proof exists if the "divides" relation ∥ can be used, see addmodlteqALT 16373. (Contributed by AV, 20-Mar-2021.)
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))
5.6.3  Miscellaneous theorems about integers
Theorem	om2uz0i 13974*	The mapping 𝐺 is a one-to-one mapping from ω onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number 𝐶 (normally 0 for the upper integers ℕ0 or 1 for the upper integers ℕ), 1 maps to 𝐶 + 1, etc. This theorem shows the value of 𝐺 at ordinal natural number zero. (This series of theorems generalizes an earlier series for ℕ0 contributed by Raph Levien, 10-Apr-2004.) (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ (𝐺‘∅) = 𝐶
Theorem	om2uzsuci 13975*	The value of 𝐺 (see om2uz0i 13974) at a successor. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) + 1))
Theorem	om2uzuzi 13976*	The value 𝐺 (see om2uz0i 13974) at an ordinal natural number is in the upper integers. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘𝐴) ∈ (ℤ≥‘𝐶))
Theorem	om2uzlti 13977*	Less-than relation for 𝐺 (see om2uz0i 13974). (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) < (𝐺‘𝐵)))
Theorem	om2uzlt2i 13978*	The mapping 𝐺 (see om2uz0i 13974) preserves order. (Contributed by NM, 4-May-2005.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) < (𝐺‘𝐵)))
Theorem	om2uzrani 13979*	Range of 𝐺 (see om2uz0i 13974). (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ ran 𝐺 = (ℤ≥‘𝐶)
Theorem	om2uzf1oi 13980*	𝐺 (see om2uz0i 13974) is a one-to-one onto mapping. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ 𝐺:ω–1-1-onto→(ℤ≥‘𝐶)
Theorem	om2uzisoi 13981*	𝐺 (see om2uz0i 13974) is an isomorphism from natural ordinals to upper integers. (Contributed by NM, 9-Oct-2008.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ 𝐺 Isom E , < (ω, (ℤ≥‘𝐶))
Theorem	om2uzoi 13982*	An alternative definition of 𝐺 in terms of df-oi 9460. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ 𝐺 = OrdIso( < , (ℤ≥‘𝐶))
Theorem	om2uzrdg 13983*	A helper lemma for the value of a recursive definition generator on upper integers (typically either ℕ or ℕ0) with characteristic function 𝐹(𝑥, 𝑦) and initial value 𝐴. Normally 𝐹 is a function on the partition, and 𝐴 is a member of the partition. See also comment in om2uz0i 13974. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)    ⇒   ⊢ (𝐵 ∈ ω → (𝑅‘𝐵) = ⟨(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))⟩)
Theorem	uzrdglem 13984*	A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)    ⇒   ⊢ (𝐵 ∈ (ℤ≥‘𝐶) → ⟨𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))⟩ ∈ ran 𝑅)
Theorem	uzrdgfni 13985*	The recursive definition generator on upper integers is a function. See comment in om2uzrdg 13983. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)    &   ⊢ 𝑆 = ran 𝑅    ⇒   ⊢ 𝑆 Fn (ℤ≥‘𝐶)
Theorem	uzrdg0i 13986*	Initial value of a recursive definition generator on upper integers. See comment in om2uzrdg 13983. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)    &   ⊢ 𝑆 = ran 𝑅    ⇒   ⊢ (𝑆‘𝐶) = 𝐴
Theorem	uzrdgsuci 13987*	Successor value of a recursive definition generator on upper integers. See comment in om2uzrdg 13983. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑥𝐹𝑦)⟩), ⟨𝐶, 𝐴⟩) ↾ ω)    &   ⊢ 𝑆 = ran 𝑅    ⇒   ⊢ (𝐵 ∈ (ℤ≥‘𝐶) → (𝑆‘(𝐵 + 1)) = (𝐵𝐹(𝑆‘𝐵)))
Theorem	ltweuz 13988	< is a well-founded relation on any sequence of upper integers. (Contributed by Andrew Salmon, 13-Nov-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ < We (ℤ≥‘𝐴)
Theorem	ltwenn 13989	Less than well-orders the naturals. (Contributed by Scott Fenton, 6-Aug-2013.)
⊢ < We ℕ
Theorem	ltwefz 13990	Less than well-orders a set of finite integers. (Contributed by Scott Fenton, 8-Aug-2013.)
⊢ < We (𝑀...𝑁)
Theorem	uzenom 13991	An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → 𝑍 ≈ ω)
Theorem	uzinf 13992	An upper integer set is infinite. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → ¬ 𝑍 ∈ Fin)
Theorem	nnnfi 13993	The set of positive integers is infinite. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ¬ ℕ ∈ Fin
Theorem	uzrdgxfr 13994*	Transfer the value of the recursive sequence builder from one base to another. (Contributed by Mario Carneiro, 1-Apr-2014.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐴) ↾ ω)    &   ⊢ 𝐻 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐵) ↾ ω)    &   ⊢ 𝐴 ∈ ℤ    &   ⊢ 𝐵 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ ω → (𝐺‘𝑁) = ((𝐻‘𝑁) + (𝐴 − 𝐵)))
Theorem	fzennn 13995	The cardinality of a finite set of sequential integers. (See om2uz0i 13974 for a description of the hypothesis.) (Contributed by Mario Carneiro, 12-Feb-2013.) (Revised by Mario Carneiro, 7-Mar-2014.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ≈ (◡𝐺‘𝑁))
Theorem	fzen2 13996	The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Mario Carneiro, 13-Feb-2014.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡𝐺‘((𝑁 + 1) − 𝑀)))
Theorem	cardfz 13997	The cardinality of a finite set of sequential integers. (See om2uz0i 13974 for a description of the hypothesis.) (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (card‘(1...𝑁)) = (◡𝐺‘𝑁))
Theorem	hashgf1o 13998	𝐺 maps ω one-to-one onto ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)    ⇒   ⊢ 𝐺:ω–1-1-onto→ℕ0
Theorem	fzfi 13999	A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)
⊢ (𝑀...𝑁) ∈ Fin
Theorem	fzfid 14000	Commonly used special case of fzfi 13999. (Contributed by Mario Carneiro, 25-May-2014.)
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin)