P. 127 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12601-12700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	flltp1 12601	A basic property of the floor (greatest integer) function. (Contributed by NM, 24-Feb-2005.)
|- ( A e. RR -> A < ( ( |_ ` A ) + 1 ) )
Theorem	fllep1 12602	A basic property of the floor (greatest integer) function. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( A e. RR -> A <_ ( ( |_ ` A ) + 1 ) )
Theorem	fraclt1 12603	The fractional part of a real number is less than one. (Contributed by NM, 15-Jul-2008.)
|- ( A e. RR -> ( A - ( |_ ` A ) ) < 1 )
Theorem	fracle1 12604	The fractional part of a real number is less than or equal to one. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( A e. RR -> ( A - ( |_ ` A ) ) <_ 1 )
Theorem	fracge0 12605	The fractional part of a real number is nonnegative. (Contributed by NM, 17-Jul-2008.)
|- ( A e. RR -> 0 <_ ( A - ( |_ ` A ) ) )
Theorem	flge 12606	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.)
|- ( ( A e. RR /\ B e. ZZ ) -> ( B <_ A <-> B <_ ( |_ ` A ) ) )
Theorem	fllt 12607	The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005.)
|- ( ( A e. RR /\ B e. ZZ ) -> ( A < B <-> ( |_ ` A ) < B ) )
Theorem	flflp1 12608	Move floor function between strict and non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) <_ B <-> A < ( ( |_ ` B ) + 1 ) ) )
Theorem	flid 12609	An integer is its own floor. (Contributed by NM, 15-Nov-2004.)
|- ( A e. ZZ -> ( |_ ` A ) = A )
Theorem	flidm 12610	The floor function is idempotent. (Contributed by NM, 17-Aug-2008.)
|- ( A e. RR -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )
Theorem	flidz 12611	A real number equals its floor iff it is an integer. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR -> ( ( |_ ` A ) = A <-> A e. ZZ ) )
Theorem	flltnz 12612	If A is not an integer, then the floor of A is less than A. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) < A )
Theorem	flwordi 12613	Ordering relationship for the greatest integer function. (Contributed by NM, 31-Dec-2005.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` A ) <_ ( |_ ` B ) )
Theorem	flword2 12614	Ordering relationship for the greatest integer function. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) )
Theorem	flval2 12615*	An alternate way to define the floor (greatest integer) function. (Contributed by NM, 16-Nov-2004.)
|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) )
Theorem	flval3 12616*	An alternate way to define the floor (greatest integer) 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.)
|- ( A e. RR -> ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) )
Theorem	flbi 12617	A condition equivalent to floor. (Contributed by NM, 11-Mar-2005.) (Revised by Mario Carneiro, 2-Nov-2013.)
|- ( ( A e. RR /\ B e. ZZ ) -> ( ( |_ ` A ) = B <-> ( B <_ A /\ A < ( B + 1 ) ) ) )
Theorem	flbi2 12618	A condition equivalent to floor. (Contributed by NM, 15-Aug-2008.)
|- ( ( N e. ZZ /\ F e. RR ) -> ( ( |_ ` ( N + F ) ) = N <-> ( 0 <_ F /\ F < 1 ) ) )
Theorem	adddivflid 12619	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.)
|- ( ( A e. ZZ /\ B e. NN0 /\ C e. NN ) -> ( B < C <-> ( |_ ` ( A + ( B / C ) ) ) = A ) )
Theorem	ico01fl0 12620	The floor of a real number in [ 0 , 1 ) is 0. Remark: may shorten the proof of modid 12695 or a version of it where the antecedent is membership in an interval. (Contributed by BJ, 29-Jun-2019.)
|- ( A e. ( 0 [,) 1 ) -> ( |_ ` A ) = 0 )
Theorem	flge0nn0 12621	The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
Theorem	flge1nn 12622	The floor of a number greater than or equal to 1 is a positive integer. (Contributed by NM, 26-Apr-2005.)
|- ( ( A e. RR /\ 1 <_ A ) -> ( |_ ` A ) e. NN )
Theorem	fldivnn0 12623	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.)
|- ( ( K e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) e. NN0 )
Theorem	refldivcl 12624	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.)
|- ( ( K e. RR /\ L e. RR+ ) -> ( |_ ` ( K / L ) ) e. RR )
Theorem	divfl0 12625	The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021.)
|- ( ( A e. NN0 /\ B e. NN ) -> ( A < B <-> ( |_ ` ( A / B ) ) = 0 ) )
Theorem	fladdz 12626	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.)
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) )
Theorem	flzadd 12627	An integer can be moved in and out of the floor of a sum. (Contributed by NM, 2-Jan-2009.)
|- ( ( N e. ZZ /\ A e. RR ) -> ( |_ ` ( N + A ) ) = ( N + ( |_ ` A ) ) )
Theorem	flmulnn0 12628	Move a nonnegative integer in and out of a floor. (Contributed by NM, 2-Jan-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.)
|- ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )
Theorem	btwnzge0 12629	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 11787.) (Contributed by NM, 12-Mar-2005.)
|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( 0 <_ A <-> 0 <_ N ) )
Theorem	2tnp1ge0ge0 12630	Two times an integer plus one is not negative iff the integer is not negative. (Contributed by AV, 19-Jun-2021.)
|- ( N e. ZZ -> ( 0 <_ ( ( 2 x. N ) + 1 ) <-> 0 <_ N ) )
Theorem	flhalf 12631	Ordering relation for the floor of half of an integer. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
|- ( N e. ZZ -> N <_ ( 2 x. ( |_ ` ( ( N + 1 ) / 2 ) ) ) )
Theorem	fldivle 12632	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.)
|- ( ( K e. RR /\ L e. RR+ ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) )
Theorem	fldivnn0le 12633	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.)
|- ( ( K e. NN0 /\ L e. NN ) -> ( |_ ` ( K / L ) ) <_ ( K / L ) )
Theorem	flltdivnn0lt 12634	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.)
|- ( ( K e. NN0 /\ N e. NN0 /\ L e. NN ) -> ( K < N -> ( |_ ` ( K / L ) ) < ( N / L ) ) )
Theorem	ltdifltdiv 12635	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.)
|- ( ( A e. RR /\ B e. RR+ /\ C e. RR ) -> ( A < ( C - B ) -> ( ( |_ ` ( A / B ) ) + 1 ) < ( C / B ) ) )
Theorem	fldiv4p1lem1div2 12636	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.)
|- ( ( N = 3 \/ N e. ( ZZ>= ` 5 ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
Theorem	fldiv4lem1div2uz2 12637	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.)
|- ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )
Theorem	fldiv4lem1div2 12638	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.)
|- ( N e. NN -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )
Theorem	ceilval 12639	The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.)
|- ( A e. RR -> (⌈ ` A ) = -u ( |_ ` -u A ) )
Theorem	dfceil2 12640*	Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.)
|- ⌈ = ( x e. RR |-> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )
Theorem	ceilval2 12641*	The value of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.)
|- ( A e. RR -> (⌈ ` A ) = ( iota_ y e. ZZ ( A <_ y /\ y < ( A + 1 ) ) ) )
Theorem	ceicl 12642	The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007.)
|- ( A e. RR -> -u ( |_ ` -u A ) e. ZZ )
Theorem	ceilcl 12643	Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.)
|- ( A e. RR -> (⌈ ` A ) e. ZZ )
Theorem	ceige 12644	The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007.)
|- ( A e. RR -> A <_ -u ( |_ ` -u A ) )
Theorem	ceilge 12645	The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018.)
|- ( A e. RR -> A <_ (⌈ ` A ) )
Theorem	ceim1l 12646	One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007.)
|- ( A e. RR -> ( -u ( |_ ` -u A ) - 1 ) < A )
Theorem	ceilm1lt 12647	One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018.)
|- ( A e. RR -> ( (⌈ ` A ) - 1 ) < A )
Theorem	ceile 12648	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jeff Hankins, 10-Jun-2007.)
|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> -u ( |_ ` -u A ) <_ B )
Theorem	ceille 12649	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.)
|- ( ( A e. RR /\ B e. ZZ /\ A <_ B ) -> (⌈ ` A ) <_ B )
Theorem	ceilid 12650	An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
|- ( A e. ZZ -> (⌈ ` A ) = A )
Theorem	ceilidz 12651	A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.)
|- ( A e. RR -> ( A e. ZZ <-> (⌈ ` A ) = A ) )
Theorem	flleceil 12652	The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.)
|- ( A e. RR -> ( |_ ` A ) <_ (⌈ ` A ) )
Theorem	fleqceilz 12653	A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.)
|- ( A e. RR -> ( A e. ZZ <-> ( |_ ` A ) = (⌈ ` A ) ) )
Theorem	quoremz 12654	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 15126. (Contributed by NM, 14-Aug-2008.)
|- Q = ( |_ ` ( A / B ) )   &    |- R = ( A - ( B x. Q ) )   =>    |- ( ( A e. ZZ /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
Theorem	quoremnn0 12655	Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.)
|- Q = ( |_ ` ( A / B ) )   &    |- R = ( A - ( B x. Q ) )   =>    |- ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
Theorem	quoremnn0ALT 12656	Alternate proof of quoremnn0 12655 not using quoremz 12654. TODO - Keep either quoremnn0ALT 12656 (if we don't keep quoremz 12654) or quoremnn0 12655. (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- Q = ( |_ ` ( A / B ) )   &    |- R = ( A - ( B x. Q ) )   =>    |- ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )
Theorem	intfrac2 12657	Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 12685? (Contributed by NM, 16-Aug-2008.)
|- Z = ( |_ ` A )   &    |- F = ( A - Z )   =>    |- ( A e. RR -> ( 0 <_ F /\ F < 1 /\ A = ( Z + F ) ) )
Theorem	intfracq 12658	Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 12657. (Contributed by NM, 16-Aug-2008.)
|- Z = ( |_ ` ( M / N ) )   &    |- F = ( ( M / N ) - Z )   =>    |- ( ( M e. ZZ /\ N e. NN ) -> ( 0 <_ F /\ F <_ ( ( N - 1 ) / N ) /\ ( M / N ) = ( Z + F ) ) )
Theorem	fldiv 12659	Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.)
|- ( ( A e. RR /\ N e. NN ) -> ( |_ ` ( ( |_ ` A ) / N ) ) = ( |_ ` ( A / N ) ) )
Theorem	fldiv2 12660	Cancellation of an embedded floor of a ratio. Generalization of Equation 2.4 in [CormenLeisersonRivest] p. 33 (where A must be an integer). (Contributed by NM, 9-Nov-2008.)
|- ( ( A e. RR /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( |_ ` ( A / M ) ) / N ) ) = ( |_ ` ( A / ( M x. N ) ) ) )
Theorem	fznnfl 12661	Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.)
|- ( N e. RR -> ( K e. ( 1 ... ( |_ ` N ) ) <-> ( K e. NN /\ K <_ N ) ) )
Theorem	uzsup 12662	An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
Theorem	ioopnfsup 12663	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
|- ( ( A e. RR* /\ A =/= +oo ) -> sup ( ( A (,) +oo ) , RR* , < ) = +oo )
Theorem	icopnfsup 12664	An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
|- ( ( A e. RR* /\ A =/= +oo ) -> sup ( ( A [,) +oo ) , RR* , < ) = +oo )
Theorem	rpsup 12665	The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
|- sup ( RR+ , RR* , < ) = +oo
Theorem	resup 12666	The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
|- sup ( RR , RR* , < ) = +oo
Theorem	xrsup 12667	The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.)
|- sup ( RR* , RR* , < ) = +oo
5.6.2  The modulo (remainder) operation
Syntax	cmo 12668	Extend class notation with the modulo operation.
class mod
Definition	df-mod 12669*	Define the modulo (remainder) operation. See modval 12670 for its value. For example, ( 5 mod 3 ) = 2 and ( -u 7 mod 2 ) = 1 (ex-mod 27306). (Contributed by NM, 10-Nov-2008.)
|- mod = ( x e. RR , y e. RR+ |-> ( x - ( y x. ( |_ ` ( x / y ) ) ) ) )
Theorem	modval 12670	The value of the modulo operation. The modulo congruence notation of number theory, J == K (modulo N), can be expressed in our notation as ( J mod N ) = ( K mod N ). 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.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
Theorem	modvalr 12671	The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( ( |_ ` ( A / B ) ) x. B ) ) )
Theorem	modcl 12672	Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )
Theorem	flpmodeq 12673	Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( ( |_ ` ( A / B ) ) x. B ) + ( A mod B ) ) = A )
Theorem	modcld 12674	Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A mod B ) e. RR )
Theorem	mod0 12675	A mod B is zero iff A is evenly divisible by B. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A / B ) e. ZZ ) )
Theorem	mulmod0 12676	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.)
|- ( ( A e. ZZ /\ M e. RR+ ) -> ( ( A x. M ) mod M ) = 0 )
Theorem	negmod0 12677	A is divisible by B iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( -u A mod B ) = 0 ) )
Theorem	modge0 12678	The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.)
|- ( ( A e. RR /\ B e. RR+ ) -> 0 <_ ( A mod B ) )
Theorem	modlt 12679	The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )
Theorem	modelico 12680	Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. ( 0 [,) B ) )
Theorem	moddiffl 12681	The modulo operation differs from A by an integer multiple of B. (Contributed by Mario Carneiro, 6-Sep-2016.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) = ( |_ ` ( A / B ) ) )
Theorem	moddifz 12682	The modulo operation differs from A by an integer multiple of B. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( A mod B ) ) / B ) e. ZZ )
Theorem	modfrac 12683	The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR -> ( A mod 1 ) = ( A - ( |_ ` A ) ) )
Theorem	flmod 12684	The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR -> ( |_ ` A ) = ( A - ( A mod 1 ) ) )
Theorem	intfrac 12685	Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.)
|- ( A e. RR -> A = ( ( |_ ` A ) + ( A mod 1 ) ) )
Theorem	zmod10 12686	An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( N e. ZZ -> ( N mod 1 ) = 0 )
Theorem	zmod1congr 12687	Two arbitrary integers are congruent modulo 1, see example 4 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A mod 1 ) = ( B mod 1 ) )
Theorem	modmulnn 12688	Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by NM, 2-Jan-2009.)
|- ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) ) mod ( N x. M ) ) <_ ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) )
Theorem	modvalp1 12689	The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Alexander van der Vekens, 14-Apr-2018.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A + B ) - ( ( ( |_ ` ( A / B ) ) + 1 ) x. B ) ) = ( A mod B ) )
Theorem	zmodcl 12690	Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. NN0 )
Theorem	zmodcld 12691	Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. NN )   =>    |- ( ph -> ( A mod B ) e. NN0 )
Theorem	zmodfz 12692	An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ... ( B - 1 ) ) )
Theorem	zmodfzo 12693	An integer mod B lies in the first B nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0..^ B ) )
Theorem	zmodfzp1 12694	An integer mod B lies in the first B + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ... B ) )
Theorem	modid 12695	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = A )
Theorem	modid0 12696	A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.)
|- ( N e. RR+ -> ( N mod N ) = 0 )
Theorem	modid2 12697	Identity law for modulo. (Contributed by NM, 29-Dec-2008.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = A <-> ( 0 <_ A /\ A < B ) ) )
Theorem	zmodid2 12698	Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <-> M e. ( 0 ... ( N - 1 ) ) ) )
Theorem	zmodidfzo 12699	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <-> M e. ( 0..^ N ) ) )
Theorem	zmodidfzoimp 12700	Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.)
|- ( M e. ( 0..^ N ) -> ( M mod N ) = M )