P. 139 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13801-13900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fldivle 13801	The floor function of a division of a real number by a positive real number is less than or equal to the division. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ+) → (⌊‘(𝐾 / 𝐿)) ≤ (𝐾 / 𝐿))
Theorem	fldivnn0le 13802	The floor function of a division of a nonnegative integer by a positive integer is less than or equal to the division. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (⌊‘(𝐾 / 𝐿)) ≤ (𝐾 / 𝐿))
Theorem	flltdivnn0lt 13803	The floor function of a division of a nonnegative integer by a positive integer is less than the division of a greater dividend by the same positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (𝐾 < 𝑁 → (⌊‘(𝐾 / 𝐿)) < (𝑁 / 𝐿)))
Theorem	ltdifltdiv 13804	If the dividend of a division is less than the difference between a real number and the divisor, the floor function of the division plus 1 is less than the division of the real number by the divisor. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐶 − 𝐵) → ((⌊‘(𝐴 / 𝐵)) + 1) < (𝐶 / 𝐵)))
Theorem	fldiv4p1lem1div2 13805	The floor of an integer equal to 3 or greater than 4, increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.)
⊢ ((𝑁 = 3 ∨ 𝑁 ∈ (ℤ≥‘5)) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) / 2))
Theorem	fldiv4lem1div2uz2 13806	The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021.) (Proof shortened by AV, 9-Jul-2022.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2))
Theorem	fldiv4lem1div2 13807	The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021.)
⊢ (𝑁 ∈ ℕ → (⌊‘(𝑁 / 4)) ≤ ((𝑁 − 1) / 2))
Theorem	ceilval 13808	The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.)
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) = -(⌊‘-𝐴))
Theorem	dfceil2 13809*	Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.)
⊢ ⌈ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑥 ≤ 𝑦 ∧ 𝑦 < (𝑥 + 1))))
Theorem	ceilval2 13810*	The value of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.)
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) = (℩𝑦 ∈ ℤ (𝐴 ≤ 𝑦 ∧ 𝑦 < (𝐴 + 1))))
Theorem	ceicl 13811	The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007.)
⊢ (𝐴 ∈ ℝ → -(⌊‘-𝐴) ∈ ℤ)
Theorem	ceilcl 13812	Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.)
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) ∈ ℤ)
Theorem	ceilcld 13813	Closure of the ceiling function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (⌈‘𝐴) ∈ ℤ)
Theorem	ceige 13814	The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ -(⌊‘-𝐴))
Theorem	ceilge 13815	The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (⌈‘𝐴))
Theorem	ceilged 13816	The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (⌈‘𝐴))
Theorem	ceim1l 13817	One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007.)
⊢ (𝐴 ∈ ℝ → (-(⌊‘-𝐴) − 1) < 𝐴)
Theorem	ceilm1lt 13818	One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → ((⌈‘𝐴) − 1) < 𝐴)
Theorem	ceile 13819	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jeff Hankins, 10-Jun-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → -(⌊‘-𝐴) ≤ 𝐵)
Theorem	ceille 13820	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → (⌈‘𝐴) ≤ 𝐵)
Theorem	ceilid 13821	An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℤ → (⌈‘𝐴) = 𝐴)
Theorem	ceilidz 13822	A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴))
Theorem	flleceil 13823	The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ (⌈‘𝐴))
Theorem	fleqceilz 13824	A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴)))
Theorem	quoremz 13825	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 16351. (Contributed by NM, 14-Aug-2008.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	quoremnn0 13826	Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	quoremnn0ALT 13827	Alternate proof of quoremnn0 13826 not using quoremz 13825. TODO - Keep either quoremnn0ALT 13827 (if we don't keep quoremz 13825) or quoremnn0 13826? (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	intfrac2 13828	Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 13856? (Contributed by NM, 16-Aug-2008.)
⊢ 𝑍 = (⌊‘𝐴)    &   ⊢ 𝐹 = (𝐴 − 𝑍)    ⇒   ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹)))
Theorem	intfracq 13829	Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 13828. (Contributed by NM, 16-Aug-2008.)
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁))    &   ⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹)))
Theorem	fldiv 13830	Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁)))
Theorem	fldiv2 13831	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 13832	Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ (𝑁 ∈ ℝ → (𝐾 ∈ (1...(⌊‘𝑁)) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
Theorem	uzsup 13833	An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞)
Theorem	ioopnfsup 13834	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴(,)+∞), ℝ*, < ) = +∞)
Theorem	icopnfsup 13835	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴[,)+∞), ℝ*, < ) = +∞)
Theorem	rpsup 13836	The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ+, ℝ*, < ) = +∞
Theorem	resup 13837	The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ, ℝ*, < ) = +∞
Theorem	xrsup 13838	The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ*, ℝ*, < ) = +∞
5.6.2  The modulo (remainder) operation
Syntax	cmo 13839	Extend class notation with the modulo operation.
class mod
Definition	df-mod 13840*	Define the modulo (remainder) operation. See modval 13841 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 29966). (Contributed by NM, 10-Nov-2008.)
⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Theorem	modval 13841	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 13842	The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵)))
Theorem	modcl 13843	Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ ℝ)
Theorem	flpmodeq 13844	Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴)
Theorem	modcld 13845	Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℝ)
Theorem	mod0 13846	𝐴 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 13847	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 13848	𝐴 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 13849	The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵))
Theorem	modlt 13850	The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵)
Theorem	modelico 13851	Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵))
Theorem	moddiffl 13852	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 13853	The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ)
Theorem	modfrac 13854	The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴)))
Theorem	flmod 13855	The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1)))
Theorem	intfrac 13856	Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.)
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1)))
Theorem	zmod10 13857	An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0)
Theorem	zmod1congr 13858	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 13859	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 13860	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 13861	Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ ℕ0)
Theorem	zmodcld 13862	Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℕ0)
Theorem	zmodfz 13863	An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...(𝐵 − 1)))
Theorem	zmodfzo 13864	An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0..^𝐵))
Theorem	zmodfzp1 13865	An integer mod 𝐵 lies in the first 𝐵 + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...𝐵))
Theorem	modid 13866	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴)
Theorem	modid0 13867	A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.)
⊢ (𝑁 ∈ ℝ+ → (𝑁 mod 𝑁) = 0)
Theorem	modid2 13868	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 𝐴 ↔ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)))
Theorem	zmodid2 13869	Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0...(𝑁 − 1))))
Theorem	zmodidfzo 13870	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0..^𝑁)))
Theorem	zmodidfzoimp 13871	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
⊢ (𝑀 ∈ (0..^𝑁) → (𝑀 mod 𝑁) = 𝑀)
Theorem	0mod 13872	Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014.)
⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0)
Theorem	1mod 13873	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 13874	Absorption law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) ∧ 𝐵 ≤ 𝐶) → ((𝐴 mod 𝐵) mod 𝐶) = (𝐴 mod 𝐵))
Theorem	modabs2 13875	Absorption law for modulo. (Contributed by NM, 29-Dec-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modcyc 13876	The modulo operation is periodic. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modcyc2 13877	The modulo operation is periodic. (Contributed by NM, 12-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 − (𝐵 · 𝑁)) mod 𝐵) = (𝐴 mod 𝐵))
Theorem	modadd1 13878	Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷))
Theorem	modaddabs 13879	Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶))
Theorem	modaddmod 13880	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 13881	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 13882	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 13883*	Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵)))
Theorem	modmuladdim 13884*	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 13885*	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 13886	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 13887	Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑀 ∈ ℕ → (-1 mod 𝑀) = (𝑀 − 1))
Theorem	m1modge3gt1 13888	Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑀 ∈ (ℤ≥‘3) → 1 < (-1 mod 𝑀))
Theorem	addmodid 13889	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 13890	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 13891	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 13892	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 13893	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 13894	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 13895	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 13896	Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐶) = (𝐵 mod 𝐶))    ⇒   ⊢ (𝜑 → (-𝐴 mod 𝐶) = (-𝐵 mod 𝐶))
Theorem	modadd12d 13897	Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐸) = ((𝐵 + 𝐷) mod 𝐸))
Theorem	modsub12d 13898	Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸))    &   ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐶) mod 𝐸) = ((𝐵 − 𝐷) mod 𝐸))
Theorem	modsubmod 13899	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 13900	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 𝑀))