P. 103 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10201-10300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzo0ssnn0 10201	Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018.)
|- ( 0..^ N ) C_ NN0
Theorem	fzo01 10202	Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( 0..^ 1 ) = { 0 }
Theorem	fzo12sn 10203	A 1-based half-open integer interval up to, but not including, 2 is a singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018.)
|- ( 1..^ 2 ) = { 1 }
Theorem	fzo0to2pr 10204	A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
|- ( 0..^ 2 ) = { 0 , 1 }
Theorem	fzo0to3tp 10205	A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
|- ( 0..^ 3 ) = { 0 , 1 , 2 }
Theorem	fzo0to42pr 10206	A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017.)
|- ( 0..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
Theorem	fzo0sn0fzo1 10207	A half-open range of nonnegative integers is the union of the singleton set containing 0 and a half-open range of positive integers. (Contributed by Alexander van der Vekens, 18-May-2018.)
|- ( N e. NN -> ( 0..^ N ) = ( { 0 } u. ( 1..^ N ) ) )
Theorem	fzoend 10208	The endpoint of a half-open integer range. (Contributed by Mario Carneiro, 29-Sep-2015.)
|- ( A e. ( A..^ B ) -> ( B - 1 ) e. ( A..^ B ) )
Theorem	fzo0end 10209	The endpoint of a zero-based half-open range. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Revised by Mario Carneiro, 29-Sep-2015.)
|- ( B e. NN -> ( B - 1 ) e. ( 0..^ B ) )
Theorem	ssfzo12 10210	Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
|- ( ( K e. ZZ /\ L e. ZZ /\ K < L ) -> ( ( K..^ L ) C_ ( M..^ N ) -> ( M <_ K /\ L <_ N ) ) )
Theorem	ssfzo12bi 10211	Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018.)
|- ( ( ( K e. ZZ /\ L e. ZZ ) /\ ( M e. ZZ /\ N e. ZZ ) /\ K < L ) -> ( ( K..^ L ) C_ ( M..^ N ) <-> ( M <_ K /\ L <_ N ) ) )
Theorem	ubmelm1fzo 10212	The result of subtracting 1 and an integer of a half-open range of nonnegative integers from the upper bound of this range is contained in this range. (Contributed by AV, 23-Mar-2018.) (Revised by AV, 30-Oct-2018.)
|- ( K e. ( 0..^ N ) -> ( ( N - K ) - 1 ) e. ( 0..^ N ) )
Theorem	fzofzp1 10213	If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( C e. ( A..^ B ) -> ( C + 1 ) e. ( A ... B ) )
Theorem	fzofzp1b 10214	If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( C e. ( ZZ>= ` A ) -> ( C e. ( A..^ B ) <-> ( C + 1 ) e. ( A ... B ) ) )
Theorem	elfzom1b 10215	An integer is a member of a 1-based finite set of sequential integers iff its predecessor is a member of the corresponding 0-based set. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 1..^ N ) <-> ( K - 1 ) e. ( 0..^ ( N - 1 ) ) ) )
Theorem	elfzonelfzo 10216	If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
|- ( N e. ZZ -> ( ( K e. ( M..^ R ) /\ -. K e. ( M..^ N ) ) -> K e. ( N..^ R ) ) )
Theorem	elfzomelpfzo 10217	An integer increased by another integer is an element of a half-open integer range if and only if the integer is contained in the half-open integer range with bounds decreased by the other integer. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( K e. ( ( M - L )..^ ( N - L ) ) <-> ( K + L ) e. ( M..^ N ) ) )
Theorem	peano2fzor 10218	A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M..^ N ) ) -> K e. ( M..^ N ) )
Theorem	fzosplitsn 10219	Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( B e. ( ZZ>= ` A ) -> ( A..^ ( B + 1 ) ) = ( ( A..^ B ) u. { B } ) )
Theorem	fzosplitprm1 10220	Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> ( A..^ ( B + 1 ) ) = ( ( A..^ ( B - 1 ) ) u. { ( B - 1 ) , B } ) )
Theorem	fzosplitsni 10221	Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( B e. ( ZZ>= ` A ) -> ( C e. ( A..^ ( B + 1 ) ) <-> ( C e. ( A..^ B ) \/ C = B ) ) )
Theorem	fzisfzounsn 10222	A finite interval of integers as union of a half-open integer range and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
|- ( B e. ( ZZ>= ` A ) -> ( A ... B ) = ( ( A..^ B ) u. { B } ) )
Theorem	fzostep1 10223	Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015.)
|- ( A e. ( B..^ C ) -> ( ( A + 1 ) e. ( B..^ C ) \/ ( A + 1 ) = C ) )
Theorem	fzoshftral 10224*	Shift the scanning order inside of a quantification over a half-open integer range, analogous to fzshftral 10094. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M..^ N ) ph <-> A. k e. ( ( M + K )..^ ( N + K ) ) [. ( k - K ) / j ]. ph ) )
Theorem	fzind2 10225*	Induction on the integers from M to N inclusive. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Version of fzind 9357 using integer range definitions. (Contributed by Mario Carneiro, 6-Feb-2016.)
|- ( x = M -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> th ) )   &    |- ( x = K -> ( ph <-> ta ) )   &    |- ( N e. ( ZZ>= ` M ) -> ps )   &    |- ( y e. ( M..^ N ) -> ( ch -> th ) )   =>    |- ( K e. ( M ... N ) -> ta )
Theorem	exfzdc 10226*	Decidability of the existence of an integer defined by a decidable proposition. (Contributed by Jim Kingdon, 28-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ n e. ( M ... N ) ) -> DECID ps )   =>    |- ( ph -> DECID E. n e. ( M ... N ) ps )
Theorem	fvinim0ffz 10227	The function values for the borders of a finite interval of integers, which is the domain of the function, are not in the image of the interior of the interval iff the intersection of the images of the interior and the borders is empty. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.)
|- ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1..^ K ) ) ) = (/) <-> ( ( F ` 0 ) e/ ( F " ( 1..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1..^ K ) ) ) ) )
Theorem	subfzo0 10228	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.)
|- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) ) -> ( -u N < ( I - J ) /\ ( I - J ) < N ) )
4.5.7  Rational numbers (cont.)
Theorem	qtri3or 10229	Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.)
|- ( ( M e. QQ /\ N e. QQ ) -> ( M < N \/ M = N \/ N < M ) )
Theorem	qletric 10230	Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A <_ B \/ B <_ A ) )
Theorem	qlelttric 10231	Rational trichotomy. (Contributed by Jim Kingdon, 7-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A <_ B \/ B < A ) )
Theorem	qltnle 10232	'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( A < B <-> -. B <_ A ) )
Theorem	qdceq 10233	Equality of rationals is decidable. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> DECID A = B )
Theorem	exbtwnzlemstep 10234*	Lemma for exbtwnzlemex 10236. Induction step. (Contributed by Jim Kingdon, 10-May-2022.)
|- ( ph -> K e. NN )   &    |- ( ph -> A e. RR )   &    |- ( ( ph /\ n e. ZZ ) -> ( n <_ A \/ A < n ) )   =>    |- ( ( ph /\ E. m e. ZZ ( m <_ A /\ A < ( m + ( K + 1 ) ) ) ) -> E. m e. ZZ ( m <_ A /\ A < ( m + K ) ) )
Theorem	exbtwnzlemshrink 10235*	Lemma for exbtwnzlemex 10236. Shrinking the range around A. (Contributed by Jim Kingdon, 10-May-2022.)
|- ( ph -> J e. NN )   &    |- ( ph -> A e. RR )   &    |- ( ( ph /\ n e. ZZ ) -> ( n <_ A \/ A < n ) )   =>    |- ( ( ph /\ E. m e. ZZ ( m <_ A /\ A < ( m + J ) ) ) -> E. x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
Theorem	exbtwnzlemex 10236*	Existence of an integer so that a given real number is between the integer and its successor. The real number must satisfy the n <_ A \/ A < n hypothesis. For example either a rational number or a number which is irrational (in the sense of being apart from any rational number) will meet this condition. The proof starts by finding two integers which are less than and greater than A. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on the n <_ A \/ A < n hypothesis, and iterating until the range consists of two consecutive integers. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( ph -> A e. RR )   &    |- ( ( ph /\ n e. ZZ ) -> ( n <_ A \/ A < n ) )   =>    |- ( ph -> E. x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
Theorem	exbtwnz 10237*	If a real number is between an integer and its successor, there is a unique greatest integer less than or equal to the real number. (Contributed by Jim Kingdon, 10-May-2022.)
|- ( ph -> E. x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
Theorem	qbtwnz 10238*	There is a unique greatest integer less than or equal to a rational number. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
Theorem	rebtwn2zlemstep 10239*	Lemma for rebtwn2z 10241. Induction step. (Contributed by Jim Kingdon, 13-Oct-2021.)
|- ( ( K e. ( ZZ>= ` 2 ) /\ A e. RR /\ E. m e. ZZ ( m < A /\ A < ( m + ( K + 1 ) ) ) ) -> E. m e. ZZ ( m < A /\ A < ( m + K ) ) )
Theorem	rebtwn2zlemshrink 10240*	Lemma for rebtwn2z 10241. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.)
|- ( ( A e. RR /\ J e. ( ZZ>= ` 2 ) /\ E. m e. ZZ ( m < A /\ A < ( m + J ) ) ) -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) )
Theorem	rebtwn2z 10241*	A real number can be bounded by integers above and below which are two apart. The proof starts by finding two integers which are less than and greater than the given real number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on weak linearity, and iterating until the range consists of integers which are two apart. (Contributed by Jim Kingdon, 13-Oct-2021.)
|- ( A e. RR -> E. x e. ZZ ( x < A /\ A < ( x + 2 ) ) )
Theorem	qbtwnrelemcalc 10242	Lemma for qbtwnre 10243. Calculations involved in showing the constructed rational number is less than B. (Contributed by Jim Kingdon, 14-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> M < ( A x. ( 2 x. N ) ) )   &    |- ( ph -> ( 1 / N ) < ( B - A ) )   =>    |- ( ph -> ( ( M + 2 ) / ( 2 x. N ) ) < B )
Theorem	qbtwnre 10243*	The rational numbers are dense in RR: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )
Theorem	qbtwnxr 10244*	The rational numbers are dense in RR*: any two extended real numbers have a rational between them. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )
Theorem	qavgle 10245	The average of two rational numbers is less than or equal to at least one of them. (Contributed by Jim Kingdon, 3-Nov-2021.)
|- ( ( A e. QQ /\ B e. QQ ) -> ( ( ( A + B ) / 2 ) <_ A \/ ( ( A + B ) / 2 ) <_ B ) )
Theorem	ioo0 10246	An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
Theorem	ioom 10247*	An open interval of extended reals is inhabited iff the lower argument is less than the upper argument. (Contributed by Jim Kingdon, 27-Nov-2021.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( E. x x e. ( A (,) B ) <-> A < B ) )
Theorem	ico0 10248	An empty open interval of extended reals. (Contributed by FL, 30-May-2014.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )
Theorem	ioc0 10249	An empty open interval of extended reals. (Contributed by FL, 30-May-2014.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,] B ) = (/) <-> B <_ A ) )
Theorem	dfrp2 10250	Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.)
|- RR+ = ( 0 (,) +oo )
Theorem	elicod 10251	Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ C )   &    |- ( ph -> C < B )   =>    |- ( ph -> C e. ( A [,) B ) )
Theorem	icogelb 10252	An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,) B ) ) -> A <_ C )
Theorem	elicore 10253	A member of a left-closed right-open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ C e. ( A [,) B ) ) -> C e. RR )
4.6  Elementary integer functions
4.6.1  The floor and ceiling functions
Syntax	cfl 10254	Extend class notation with floor (greatest integer) function.
class |_
Syntax	cceil 10255	Extend class notation to include the ceiling function.
class ⌈
Definition	df-fl 10256*	Define the floor (greatest integer less than or equal to) function. See flval 10258 for its value, flqlelt 10262 for its basic property, and flqcl 10259 for its closure. For example, ( |_ ` ( 3 / 2 ) ) = 1 while ( |_ ` -u ( 3 / 2 ) ) = -u 2 (ex-fl 14133). Although we define this on real numbers so that notations are similar to the Metamath Proof Explorer, in the absence of excluded middle few theorems will be possible for all real numbers. Imagine a real number which is around 2.99995 or 3.00001 . In order to determine whether its floor is 2 or 3, it would be necessary to compute the number to arbitrary precision. 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.)
|- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) )
Definition	df-ceil 10257	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 ceilqval 10292 for its value, ceilqge 10296 and ceilqm1lt 10298 for its basic properties, and ceilqcl 10294 for its closure. For example, (⌈ ` ( 3 / 2 ) ) = 2 while (⌈ ` -u ( 3 / 2 ) ) = -u 1 (ex-ceil 14134). As described in df-fl 10256 most theorems are only for rationals, not reals. The symbol ⌈ is inspired by the gamma shaped left bracket of the usual notation. (Contributed by David A. Wheeler, 19-May-2015.)
|- ⌈ = ( x e. RR |-> -u ( |_ ` -u x ) )
Theorem	flval 10258*	Value of the floor (greatest integer) function. The floor of A is the (unique) integer less than or equal to A whose successor is strictly greater than A. (Contributed by NM, 14-Nov-2004.) (Revised by Mario Carneiro, 2-Nov-2013.)
|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
Theorem	flqcl 10259	The floor (greatest integer) function yields an integer when applied to a rational (closure law). For a similar closure law for real numbers apart from any integer, see flapcl 10261. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> ( |_ ` A ) e. ZZ )
Theorem	apbtwnz 10260*	There is a unique greatest integer less than or equal to a real number which is apart from all integers. (Contributed by Jim Kingdon, 11-May-2022.)
|- ( ( A e. RR /\ A. n e. ZZ A # n ) -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) )
Theorem	flapcl 10261*	The floor (greatest integer) function yields an integer when applied to a real number apart from any integer. For example, an irrational number (see for example sqrt2irrap 12163) would satisfy this condition. (Contributed by Jim Kingdon, 11-May-2022.)
|- ( ( A e. RR /\ A. n e. ZZ A # n ) -> ( |_ ` A ) e. ZZ )
Theorem	flqlelt 10262	A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) )
Theorem	flqcld 10263	The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( ph -> A e. QQ )   =>    |- ( ph -> ( |_ ` A ) e. ZZ )
Theorem	flqle 10264	A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> ( |_ ` A ) <_ A )
Theorem	flqltp1 10265	A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> A < ( ( |_ ` A ) + 1 ) )
Theorem	qfraclt1 10266	The fractional part of a rational number is less than one. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> ( A - ( |_ ` A ) ) < 1 )
Theorem	qfracge0 10267	The fractional part of a rational number is nonnegative. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> 0 <_ ( A - ( |_ ` A ) ) )
Theorem	flqge 10268	The floor function value is the greatest integer less than or equal to its argument. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( ( A e. QQ /\ B e. ZZ ) -> ( B <_ A <-> B <_ ( |_ ` A ) ) )
Theorem	flqlt 10269	The floor function value is less than the next integer. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( ( A e. QQ /\ B e. ZZ ) -> ( A < B <-> ( |_ ` A ) < B ) )
Theorem	flid 10270	An integer is its own floor. (Contributed by NM, 15-Nov-2004.)
|- ( A e. ZZ -> ( |_ ` A ) = A )
Theorem	flqidm 10271	The floor function is idempotent. (Contributed by Jim Kingdon, 8-Oct-2021.)
|- ( A e. QQ -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )
Theorem	flqidz 10272	A rational number equals its floor iff it is an integer. (Contributed by Jim Kingdon, 9-Oct-2021.)
|- ( A e. QQ -> ( ( |_ ` A ) = A <-> A e. ZZ ) )
Theorem	flqltnz 10273	If A is not an integer, then the floor of A is less than A. (Contributed by Jim Kingdon, 9-Oct-2021.)
|- ( ( A e. QQ /\ -. A e. ZZ ) -> ( |_ ` A ) < A )
Theorem	flqwordi 10274	Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ /\ A <_ B ) -> ( |_ ` A ) <_ ( |_ ` B ) )
Theorem	flqword2 10275	Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.)
|- ( ( A e. QQ /\ B e. QQ /\ A <_ B ) -> ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) )
Theorem	flqbi 10276	A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.)
|- ( ( A e. QQ /\ B e. ZZ ) -> ( ( |_ ` A ) = B <-> ( B <_ A /\ A < ( B + 1 ) ) ) )
Theorem	flqbi2 10277	A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.)
|- ( ( N e. ZZ /\ F e. QQ ) -> ( ( |_ ` ( N + F ) ) = N <-> ( 0 <_ F /\ F < 1 ) ) )
Theorem	adddivflid 10278	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	flqge0nn0 10279	The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- ( ( A e. QQ /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
Theorem	flqge1nn 10280	The floor of a number greater than or equal to 1 is a positive integer. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- ( ( A e. QQ /\ 1 <_ A ) -> ( |_ ` A ) e. NN )
Theorem	fldivnn0 10281	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	divfl0 10282	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	flqaddz 10283	An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- ( ( A e. QQ /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) )
Theorem	flqzadd 10284	An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- ( ( N e. ZZ /\ A e. QQ ) -> ( |_ ` ( N + A ) ) = ( N + ( |_ ` A ) ) )
Theorem	flqmulnn0 10285	Move a nonnegative integer in and out of a floor. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- ( ( N e. NN0 /\ A e. QQ ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) )
Theorem	btwnzge0 10286	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. (Contributed by NM, 12-Mar-2005.)
|- ( ( ( A e. RR /\ N e. ZZ ) /\ ( N <_ A /\ A < ( N + 1 ) ) ) -> ( 0 <_ A <-> 0 <_ N ) )
Theorem	2tnp1ge0ge0 10287	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 10288	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	fldivnn0le 10289	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 10290	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	fldiv4p1lem1div2 10291	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	ceilqval 10292	The value of the ceiling function. (Contributed by Jim Kingdon, 10-Oct-2021.)
|- ( A e. QQ -> (⌈ ` A ) = -u ( |_ ` -u A ) )
Theorem	ceiqcl 10293	The ceiling function returns an integer (closure law). (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( A e. QQ -> -u ( |_ ` -u A ) e. ZZ )
Theorem	ceilqcl 10294	Closure of the ceiling function. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( A e. QQ -> (⌈ ` A ) e. ZZ )
Theorem	ceiqge 10295	The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( A e. QQ -> A <_ -u ( |_ ` -u A ) )
Theorem	ceilqge 10296	The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( A e. QQ -> A <_ (⌈ ` A ) )
Theorem	ceiqm1l 10297	One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( A e. QQ -> ( -u ( |_ ` -u A ) - 1 ) < A )
Theorem	ceilqm1lt 10298	One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( A e. QQ -> ( (⌈ ` A ) - 1 ) < A )
Theorem	ceiqle 10299	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( ( A e. QQ /\ B e. ZZ /\ A <_ B ) -> -u ( |_ ` -u A ) <_ B )
Theorem	ceilqle 10300	The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|- ( ( A e. QQ /\ B e. ZZ /\ A <_ B ) -> (⌈ ` A ) <_ B )