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	ceille 13901	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → (⌈‘𝐴) ≤ 𝐵)
Theorem	ceilid 13902	An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℤ → (⌈‘𝐴) = 𝐴)
Theorem	ceilidz 13903	A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴))
Theorem	flleceil 13904	The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ (⌈‘𝐴))
Theorem	fleqceilz 13905	A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴)))
Theorem	quoremz 13906	Quotient and remainder of an integer divided by a positive integer. TODO - is this really needed for anything? Should we use mod to simplify it? Remark (AV): This is a special case of divalg 16451. (Contributed by NM, 14-Aug-2008.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	quoremnn0 13907	Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	quoremnn0ALT 13908	Alternate proof of quoremnn0 13907 not using quoremz 13906. TODO - Keep either quoremnn0ALT 13908 (if we don't keep quoremz 13906) or quoremnn0 13907? (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	intfrac2 13909	Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 13937? (Contributed by NM, 16-Aug-2008.)
⊢ 𝑍 = (⌊‘𝐴)    &   ⊢ 𝐹 = (𝐴 − 𝑍)    ⇒   ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹)))
Theorem	intfracq 13910	Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 13909. (Contributed by NM, 16-Aug-2008.)
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁))    &   ⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹)))
Theorem	fldiv 13911	Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁)))
Theorem	fldiv2 13912	Cancellation of an embedded floor of a ratio. Generalization of Equation 2.4 in [CormenLeisersonRivest] p. 33 (where 𝐴 must be an integer). (Contributed by NM, 9-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘(𝐴 / 𝑀)) / 𝑁)) = (⌊‘(𝐴 / (𝑀 · 𝑁))))
Theorem	fznnfl 13913	Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ (𝑁 ∈ ℝ → (𝐾 ∈ (1...(⌊‘𝑁)) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
Theorem	uzsup 13914	An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞)
Theorem	ioopnfsup 13915	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴(,)+∞), ℝ*, < ) = +∞)
Theorem	icopnfsup 13916	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴[,)+∞), ℝ*, < ) = +∞)
Theorem	rpsup 13917	The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ+, ℝ*, < ) = +∞
Theorem	resup 13918	The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ, ℝ*, < ) = +∞
Theorem	xrsup 13919	The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ*, ℝ*, < ) = +∞
5.6.2  The modulo (remainder) operation
Syntax	cmo 13920	Extend class notation with the modulo operation.
class mod
Definition	df-mod 13921*	Define the modulo (remainder) operation. See modval 13922 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 30481). (Contributed by NM, 10-Nov-2008.)
⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Theorem	modval 13922	The value of the modulo operation. The modulo congruence notation of number theory, 𝐽≡𝐾 (modulo 𝑁), can be expressed in our notation as (𝐽 mod 𝑁) = (𝐾 mod 𝑁). Definition 1 in Knuth, The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive reals to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) (Contributed by NM, 10-Nov-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵)))))
Theorem	modvalr 13923	The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵)))
Theorem	modcl 13924	Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ ℝ)
Theorem	flpmodeq 13925	Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴)
Theorem	modcld 13926	Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℝ)
Theorem	mod0 13927	𝐴 mod 𝐵 is zero iff 𝐴 is evenly divisible by 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ (𝐴 / 𝐵) ∈ ℤ))
Theorem	mulmod0 13928	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 13929	𝐴 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 13930	The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵))
Theorem	modlt 13931	The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵)
Theorem	modelico 13932	Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵))
Theorem	moddiffl 13933	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 13934	The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ)
Theorem	modfrac 13935	The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴)))
Theorem	flmod 13936	The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1)))
Theorem	intfrac 13937	Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.)
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1)))
Theorem	zmod10 13938	An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0)
Theorem	zmod1congr 13939	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 13940	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 13941	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 13942	Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ ℕ0)
Theorem	zmodcld 13943	Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℕ0)
Theorem	zmodfz 13944	An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...(𝐵 − 1)))
Theorem	zmodfzo 13945	An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0..^𝐵))
Theorem	zmodfzp1 13946	An integer mod 𝐵 lies in the first 𝐵 + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...𝐵))
Theorem	modid 13947	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴)
Theorem	modid0 13948	A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.)
⊢ (𝑁 ∈ ℝ+ → (𝑁 mod 𝑁) = 0)
Theorem	modid2 13949	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 𝐴 ↔ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	zmodid2 13950	Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0...(𝑁 − 1))))
Theorem	zmodidfzo 13951	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0..^𝑁)))
Theorem	zmodidfzoimp 13952	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
⊢ (𝑀 ∈ (0..^𝑁) → (𝑀 mod 𝑁) = 𝑀)
Theorem	0mod 13953	Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014.)
⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0)
Theorem	1mod 13954	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 13955	Absorption law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) ∧ 𝐵 ≤ 𝐶) → ((𝐴 mod 𝐵) mod 𝐶) = (𝐴 mod 𝐵))
Theorem	modabs2 13956	Absorption law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modcyc 13957	The modulo operation is periodic. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modcyc2 13958	The modulo operation is periodic. (Contributed by NM, 12-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 − (𝐵 · 𝑁)) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modadd1 13959	Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))
Theorem	modaddabs 13960	Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶))
Theorem	modaddmod 13961	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 13962	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 13963	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	modmuladd 13964*	Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵)))
Theorem	modmuladdim 13965*	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 13966*	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 13967	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 13968	Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑀 ∈ ℕ → (-1 mod 𝑀) = (𝑀 − 1))
Theorem	m1modge3gt1 13969	Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑀 ∈ (ℤ≥‘3) → 1 < (-1 mod 𝑀))
Theorem	addmodid 13970	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 13971	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 13972	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 13973	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 13974	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 13975	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 13976	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 13977	Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐶) = (𝐵 mod 𝐶))    ⇒   ⊢ (𝜑 → (-𝐴 mod 𝐶) = (-𝐵 mod 𝐶))
Theorem	modadd12d 13978	Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐸) = ((𝐵 + 𝐷) mod 𝐸))
Theorem	modsub12d 13979	Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) mod 𝐸) = ((𝐵 − 𝐷) mod 𝐸))
Theorem	modsubmod 13980	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 13981	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 13982	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 13983	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 13984	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 13985	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 13986	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 13987	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 13988	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 13989	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 13990	Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (𝐴 · (𝐵 mod 𝐶)) = ((𝐴 · 𝐵) mod (𝐴 · 𝐶)))
Theorem	modsubdir 13991	Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → ((𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))))
Theorem	modeqmodmin 13992	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 13993	A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐴 / 𝐵) ∈ (ℝ ∖ ℚ)) → (𝐴 mod 𝐵) ≠ 0)
Theorem	modfzo0difsn 13994*	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 13995	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 13996	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 13997	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 13998*	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 13999*	The value of 𝐺 (see om2uz0i 13998) at a successor. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ 𝐶 ∈ ℤ    &   ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) + 1))
Theorem	om2uzuzi 14000*	The value 𝐺 (see om2uz0i 13998) 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)), 𝐶) ↾ ω)    ⇒   ⊢ (𝐴 ∈ ω → (𝐺‘𝐴) ∈ (ℤ≥‘𝐶))