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	subfzo0 13801	The difference between two elements in a half-open range of nonnegative integers is greater than the negation of the upper bound and less than the upper bound of the range. (Contributed by AV, 20-Mar-2021.)
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → (-𝑁 < (𝐼 − 𝐽) ∧ (𝐼 − 𝐽) < 𝑁))
5.6  Elementary integer functions
5.6.1  The floor and ceiling functions
Syntax	cfl 13802	Extend class notation with floor (greatest integer) function.
class ⌊
Syntax	cceil 13803	Extend class notation to include the ceiling function.
class ⌈
Definition	df-fl 13804*	Define the floor (greatest integer less than or equal to) function. See flval 13806 for its value, fllelt 13809 for its basic property, and flcl 13807 for its closure. For example, (⌊‘(3 / 2)) = 1 while (⌊‘-(3 / 2)) = -2 (ex-fl 30375). The term "floor" was coined by Ken Iverson. He also invented a mathematical notation for floor, consisting of an L-shaped left bracket and its reflection as a right bracket. In APL, the left-bracket alone is used, and we borrow this idea. (Thanks to Paul Chapman for this information.) (Contributed by NM, 14-Nov-2004.)
⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))))
Definition	df-ceil 13805	The ceiling (least integer greater than or equal to) function. Defined in ISO 80000-2:2009(E) operation 2-9.18 and the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4. See ceilval 13850 for its value, ceilge 13857 and ceilm1lt 13860 for its basic properties, and ceilcl 13854 for its closure. For example, (⌈‘(3 / 2)) = 2 while (⌈‘-(3 / 2)) = -1 (ex-ceil 30376). The symbol ⌈ is inspired by the gamma shaped left bracket of the usual notation. (Contributed by David A. Wheeler, 19-May-2015.)
⊢ ⌈ = (𝑥 ∈ ℝ ↦ -(⌊‘-𝑥))
Theorem	flval 13806*	Value of the floor (greatest integer) function. The floor of 𝐴 is the (unique) integer less than or equal to 𝐴 whose successor is strictly greater than 𝐴. (Contributed by NM, 14-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))))
Theorem	flcl 13807	The floor (greatest integer) function is an integer (closure law). (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℤ)
Theorem	reflcl 13808	The floor (greatest integer) function is real. (Contributed by NM, 15-Jul-2008.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ)
Theorem	fllelt 13809	A basic property of the floor (greatest integer) function. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.)
⊢ (𝐴 ∈ ℝ → ((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)))
Theorem	flcld 13810	The floor (greatest integer) function is an integer (closure law). (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (⌊‘𝐴) ∈ ℤ)
Theorem	flle 13811	A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ 𝐴)
Theorem	flltp1 13812	A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005.)
⊢ (𝐴 ∈ ℝ → 𝐴 < ((⌊‘𝐴) + 1))
Theorem	fllep1 13813	A basic property of the floor (greatest integer) function. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1))
Theorem	fraclt1 13814	The fractional part of a real number is less than one. (Contributed by NM, 15-Jul-2008.)
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) < 1)
Theorem	fracle1 13815	The fractional part of a real number is less than or equal to one. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ (𝐴 ∈ ℝ → (𝐴 − (⌊‘𝐴)) ≤ 1)
Theorem	fracge0 13816	The fractional part of a real number is nonnegative. (Contributed by NM, 17-Jul-2008.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 − (⌊‘𝐴)))
Theorem	flge 13817	The floor function value is the greatest integer less than or equal to its argument. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 ↔ 𝐵 ≤ (⌊‘𝐴)))
Theorem	fllt 13818	The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (⌊‘𝐴) < 𝐵))
Theorem	flflp1 13819	Move floor function between strict and non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) ≤ 𝐵 ↔ 𝐴 < ((⌊‘𝐵) + 1)))
Theorem	flid 13820	An integer is its own floor. (Contributed by NM, 15-Nov-2004.)
⊢ (𝐴 ∈ ℤ → (⌊‘𝐴) = 𝐴)
Theorem	flidm 13821	The floor function is idempotent. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ ℝ → (⌊‘(⌊‘𝐴)) = (⌊‘𝐴))
Theorem	flidz 13822	A real number equals its floor iff it is an integer. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → ((⌊‘𝐴) = 𝐴 ↔ 𝐴 ∈ ℤ))
Theorem	flltnz 13823	The floor of a non-integer real is less than it. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℤ) → (⌊‘𝐴) < 𝐴)
Theorem	flwordi 13824	Ordering relation for the floor function. (Contributed by NM, 31-Dec-2005.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ (⌊‘𝐵))
Theorem	flword2 13825	Ordering relation for the floor function. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐵) ∈ (ℤ≥‘(⌊‘𝐴)))
Theorem	flval2 13826*	An alternate way to define the floor function. (Contributed by NM, 16-Nov-2004.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (℩𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))))
Theorem	flval3 13827*	An alternate way to define the floor function, as the supremum of all integers less than or equal to its argument. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = sup({𝑥 ∈ ℤ ∣ 𝑥 ≤ 𝐴}, ℝ, < ))
Theorem	flbi 13828	A condition equivalent to floor. (Contributed by NM, 11-Mar-2005.) (Revised by Mario Carneiro, 2-Nov-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → ((⌊‘𝐴) = 𝐵 ↔ (𝐵 ≤ 𝐴 ∧ 𝐴 < (𝐵 + 1))))
Theorem	flbi2 13829	A condition equivalent to floor. (Contributed by NM, 15-Aug-2008.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐹 ∈ ℝ) → ((⌊‘(𝑁 + 𝐹)) = 𝑁 ↔ (0 ≤ 𝐹 ∧ 𝐹 < 1)))
Theorem	adddivflid 13830	The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ) → (𝐵 < 𝐶 ↔ (⌊‘(𝐴 + (𝐵 / 𝐶))) = 𝐴))
Theorem	ico01fl0 13831	The floor of a real number in [0, 1) is 0. Remark: may shorten the proof of modid 13908 or a version of it where the antecedent is membership in an interval. (Contributed by BJ, 29-Jun-2019.)
⊢ (𝐴 ∈ (0[,)1) → (⌊‘𝐴) = 0)
Theorem	flge0nn0 13832	The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)
Theorem	flge1nn 13833	The floor of a number greater than or equal to 1 is a positive integer. (Contributed by NM, 26-Apr-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ)
Theorem	fldivnn0 13834	The floor function of a division of a nonnegative integer by a positive integer is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → (⌊‘(𝐾 / 𝐿)) ∈ ℕ0)
Theorem	refldivcl 13835	The floor function of a division of a real number by a positive real number is a real number. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ+) → (⌊‘(𝐾 / 𝐿)) ∈ ℝ)
Theorem	divfl0 13836	The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (⌊‘(𝐴 / 𝐵)) = 0))
Theorem	fladdz 13837	An integer can be moved in and out of the floor of a sum. (Contributed by NM, 27-Apr-2005.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 + 𝑁)) = ((⌊‘𝐴) + 𝑁))
Theorem	flzadd 13838	An integer can be moved in and out of the floor of a sum. (Contributed by NM, 2-Jan-2009.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (⌊‘(𝑁 + 𝐴)) = (𝑁 + (⌊‘𝐴)))
Theorem	flmulnn0 13839	Move a nonnegative integer in and out of a floor. (Contributed by NM, 2-Jan-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴)))
Theorem	btwnzge0 13840	A real bounded between an integer and its successor is nonnegative iff the integer is nonnegative. Second half of Lemma 13-4.1 of [Gleason] p. 217. (For the first half see rebtwnz 12975.) (Contributed by NM, 12-Mar-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ≤ 𝐴 ∧ 𝐴 < (𝑁 + 1))) → (0 ≤ 𝐴 ↔ 0 ≤ 𝑁))
Theorem	2tnp1ge0ge0 13841	Two times an integer plus one is not negative iff the integer is not negative. (Contributed by AV, 19-Jun-2021.) (Proof shortened by AV, 10-Jul-2022.)
⊢ (𝑁 ∈ ℤ → (0 ≤ ((2 · 𝑁) + 1) ↔ 0 ≤ 𝑁))
Theorem	flhalf 13842	Ordering relation for the floor of half of an integer. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (2 · (⌊‘((𝑁 + 1) / 2))))
Theorem	fldivle 13843	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 13844	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 13845	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 13846	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 13847	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 13848	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 13849	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 13850	The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.)
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) = -(⌊‘-𝐴))
Theorem	dfceil2 13851*	Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.)
⊢ ⌈ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑥 ≤ 𝑦 ∧ 𝑦 < (𝑥 + 1))))
Theorem	ceilval2 13852*	The value of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.)
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) = (℩𝑦 ∈ ℤ (𝐴 ≤ 𝑦 ∧ 𝑦 < (𝐴 + 1))))
Theorem	ceicl 13853	The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007.)
⊢ (𝐴 ∈ ℝ → -(⌊‘-𝐴) ∈ ℤ)
Theorem	ceilcl 13854	Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.)
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) ∈ ℤ)
Theorem	ceilcld 13855	Closure of the ceiling function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (⌈‘𝐴) ∈ ℤ)
Theorem	ceige 13856	The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ -(⌊‘-𝐴))
Theorem	ceilge 13857	The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (⌈‘𝐴))
Theorem	ceilged 13858	The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐴 ≤ (⌈‘𝐴))
Theorem	ceim1l 13859	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 13860	One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → ((⌈‘𝐴) − 1) < 𝐴)
Theorem	ceile 13861	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 13862	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → (⌈‘𝐴) ≤ 𝐵)
Theorem	ceilid 13863	An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℤ → (⌈‘𝐴) = 𝐴)
Theorem	ceilidz 13864	A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴))
Theorem	flleceil 13865	The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ (⌈‘𝐴))
Theorem	fleqceilz 13866	A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴)))
Theorem	quoremz 13867	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 16398. (Contributed by NM, 14-Aug-2008.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	quoremnn0 13868	Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	quoremnn0ALT 13869	Alternate proof of quoremnn0 13868 not using quoremz 13867. TODO - Keep either quoremnn0ALT 13869 (if we don't keep quoremz 13867) or quoremnn0 13868? (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵))    &   ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄))    ⇒   ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))))
Theorem	intfrac2 13870	Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 13898? (Contributed by NM, 16-Aug-2008.)
⊢ 𝑍 = (⌊‘𝐴)    &   ⊢ 𝐹 = (𝐴 − 𝑍)    ⇒   ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹)))
Theorem	intfracq 13871	Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 13870. (Contributed by NM, 16-Aug-2008.)
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁))    &   ⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹)))
Theorem	fldiv 13872	Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁)))
Theorem	fldiv2 13873	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 13874	Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ (𝑁 ∈ ℝ → (𝐾 ∈ (1...(⌊‘𝑁)) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
Theorem	uzsup 13875	An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞)
Theorem	ioopnfsup 13876	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴(,)+∞), ℝ*, < ) = +∞)
Theorem	icopnfsup 13877	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴[,)+∞), ℝ*, < ) = +∞)
Theorem	rpsup 13878	The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ+, ℝ*, < ) = +∞
Theorem	resup 13879	The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ, ℝ*, < ) = +∞
Theorem	xrsup 13880	The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
⊢ sup(ℝ*, ℝ*, < ) = +∞
5.6.2  The modulo (remainder) operation
Syntax	cmo 13881	Extend class notation with the modulo operation.
class mod
Definition	df-mod 13882*	Define the modulo (remainder) operation. See modval 13883 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 30377). (Contributed by NM, 10-Nov-2008.)
⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦)))))
Theorem	modval 13883	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 13884	The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵)))
Theorem	modcl 13885	Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ ℝ)
Theorem	flpmodeq 13886	Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴)
Theorem	modcld 13887	Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℝ)
Theorem	mod0 13888	𝐴 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 13889	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 13890	𝐴 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 13891	The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵))
Theorem	modlt 13892	The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵)
Theorem	modelico 13893	Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵))
Theorem	moddiffl 13894	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 13895	The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ)
Theorem	modfrac 13896	The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴)))
Theorem	flmod 13897	The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.)
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1)))
Theorem	intfrac 13898	Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.)
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1)))
Theorem	zmod10 13899	An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0)
Theorem	zmod1congr 13900	Two arbitrary integers are congruent modulo 1, see example 4 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 mod 1) = (𝐵 mod 1))