Theorem List for Intuitionistic Logic Explorer - 9301-9400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | flqmulnn0 9301 |
Move a nonnegative integer in and out of a floor. (Contributed by Jim
Kingdon, 10-Oct-2021.)
|
|
|
Theorem | btwnzge0 9302 |
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.)
|
|
|
Theorem | 2tnp1ge0ge0 9303 |
Two times an integer plus one is not negative iff the integer is not
negative. (Contributed by AV, 19-Jun-2021.)
|
|
|
Theorem | flhalf 9304 |
Ordering relation for the floor of half of an integer. (Contributed by
NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
|
|
|
Theorem | fldivnn0le 9305 |
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.)
|
|
|
Theorem | flltdivnn0lt 9306 |
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.)
|
|
|
Theorem | fldiv4p1lem1div2 9307 |
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.)
|
|
|
Theorem | ceilqval 9308 |
The value of the ceiling function. (Contributed by Jim Kingdon,
10-Oct-2021.)
|
⌈ |
|
Theorem | ceiqcl 9309 |
The ceiling function returns an integer (closure law). (Contributed by
Jim Kingdon, 11-Oct-2021.)
|
|
|
Theorem | ceilqcl 9310 |
Closure of the ceiling function. (Contributed by Jim Kingdon,
11-Oct-2021.)
|
⌈ |
|
Theorem | ceiqge 9311 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
|
|
Theorem | ceilqge 9312 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⌈ |
|
Theorem | ceiqm1l 9313 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
|
|
Theorem | ceilqm1lt 9314 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
⌈ |
|
Theorem | ceiqle 9315 |
The ceiling of a real number is the smallest integer greater than or equal
to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
|
|
Theorem | ceilqle 9316 |
The ceiling of a real number is the smallest integer greater than or equal
to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
⌈ |
|
Theorem | ceilid 9317 |
An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
|
⌈ |
|
Theorem | ceilqidz 9318 |
A rational number equals its ceiling iff it is an integer. (Contributed
by Jim Kingdon, 11-Oct-2021.)
|
⌈ |
|
Theorem | flqleceil 9319 |
The floor of a rational number is less than or equal to its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⌈ |
|
Theorem | flqeqceilz 9320 |
A rational number is an integer iff its floor equals its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⌈ |
|
Theorem | intqfrac2 9321 |
Decompose a real into integer and fractional parts. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
|
|
Theorem | intfracq 9322 |
Decompose a rational number, expressed as a ratio, into integer and
fractional parts. The fractional part has a tighter bound than that of
intqfrac2 9321. (Contributed by NM, 16-Aug-2008.)
|
|
|
Theorem | flqdiv 9323 |
Cancellation of the embedded floor of a real divided by an integer.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
3.6.2 The modulo (remainder)
operation
|
|
Syntax | cmo 9324 |
Extend class notation with the modulo operation.
|
|
|
Definition | df-mod 9325* |
Define the modulo (remainder) operation. See modqval 9326 for its value.
For example, and . As with
df-fl 9274 we define this for first and second arguments
which are real and
positive real, respectively, even though many theorems will need to be
more restricted (for example, specify rational arguments). (Contributed
by NM, 10-Nov-2008.)
|
|
|
Theorem | modqval 9326 |
The value of the modulo operation. The modulo congruence notation of
number theory,
(modulo ), can be expressed in our
notation as . 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 numbers 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.) As with flqcl 9277 we
only prove this for rationals although other particular kinds of real
numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.)
|
|
|
Theorem | modqvalr 9327 |
The value of the modulo operation (multiplication in reversed order).
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
|
|
Theorem | modqcl 9328 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
|
|
Theorem | flqpmodeq 9329 |
Partition of a division into its integer part and the remainder.
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
|
|
Theorem | modqcld 9330 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
|
|
Theorem | modq0 9331 |
is zero iff is evenly divisible by . (Contributed
by Jim Kingdon, 17-Oct-2021.)
|
|
|
Theorem | mulqmod0 9332 |
The product of an integer and a positive rational number is 0 modulo the
positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | negqmod0 9333 |
is divisible by iff its negative is.
(Contributed by Jim
Kingdon, 18-Oct-2021.)
|
|
|
Theorem | modqge0 9334 |
The modulo operation is nonnegative. (Contributed by Jim Kingdon,
18-Oct-2021.)
|
|
|
Theorem | modqlt 9335 |
The modulo operation is less than its second argument. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | modqelico 9336 |
Modular reduction produces a half-open interval. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
|
|
Theorem | modqdiffl 9337 |
The modulo operation differs from by an integer multiple of .
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | modqdifz 9338 |
The modulo operation differs from by an integer multiple of .
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | modqfrac 9339 |
The fractional part of a number is the number modulo 1. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | flqmod 9340 |
The floor function expressed in terms of the modulo operation.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | intqfrac 9341 |
Break a number into its integer part and its fractional part.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | zmod10 9342 |
An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | zmod1congr 9343 |
Two arbitrary integers are congruent modulo 1, see example 4 in
[ApostolNT] p. 107. (Contributed by AV,
21-Jul-2021.)
|
|
|
Theorem | modqmulnn 9344 |
Move a positive integer in and out of a floor in the first argument of a
modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.)
|
|
|
Theorem | modqvalp1 9345 |
The value of the modulo operation (expressed with sum of denominator and
nominator). (Contributed by Jim Kingdon, 20-Oct-2021.)
|
|
|
Theorem | zmodcl 9346 |
Closure law for the modulo operation restricted to integers. (Contributed
by NM, 27-Nov-2008.)
|
|
|
Theorem | zmodcld 9347 |
Closure law for the modulo operation restricted to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | zmodfz 9348 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
|
|
Theorem | zmodfzo 9349 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^ |
|
Theorem | zmodfzp1 9350 |
An integer mod lies
in the first nonnegative integers.
(Contributed by AV, 27-Oct-2018.)
|
|
|
Theorem | modqid 9351 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | modqid0 9352 |
A positive real number modulo itself is 0. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqid2 9353 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | zmodid2 9354 |
Identity law for modulo restricted to integers. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
|
|
Theorem | zmodidfzo 9355 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
..^ |
|
Theorem | zmodidfzoimp 9356 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
..^
|
|
Theorem | q0mod 9357 |
Special case: 0 modulo a positive real number is 0. (Contributed by Jim
Kingdon, 21-Oct-2021.)
|
|
|
Theorem | q1mod 9358 |
Special case: 1 modulo a real number greater than 1 is 1. (Contributed by
Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | modqabs 9359 |
Absorption law for modulo. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqabs2 9360 |
Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | modqcyc 9361 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqcyc2 9362 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqadd1 9363 |
Addition property of the modulo operation. (Contributed by Jim Kingdon,
22-Oct-2021.)
|
|
|
Theorem | modqaddabs 9364 |
Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.)
|
|
|
Theorem | modqaddmod 9365 |
The sum of a number modulo a modulus and another number equals the sum of
the two numbers modulo the same modulus. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
|
|
Theorem | mulqaddmodid 9366 |
The sum of a positive rational number less than an upper bound and the
product of an integer and the upper bound is the positive rational number
modulo the upper bound. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
|
|
Theorem | mulp1mod1 9367 |
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.)
|
|
|
Theorem | modqmuladd 9368* |
Decomposition of an integer into a multiple of a modulus and a
remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
|
|
Theorem | modqmuladdim 9369* |
Implication of a decomposition of an integer into a multiple of a
modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
|
|
Theorem | modqmuladdnn0 9370* |
Implication of a decomposition of a nonnegative integer into a multiple
of a modulus and a remainder. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
|
|
Theorem | qnegmod 9371 |
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 Jim Kingdon, 24-Oct-2021.)
|
|
|
Theorem | m1modnnsub1 9372 |
Minus one modulo a positive integer is equal to the integer minus one.
(Contributed by AV, 14-Jul-2021.)
|
|
|
Theorem | m1modge3gt1 9373 |
Minus one modulo an integer greater than two is greater than one.
(Contributed by AV, 14-Jul-2021.)
|
|
|
Theorem | addmodid 9374 |
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.)
|
|
|
Theorem | addmodidr 9375 |
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.)
|
|
|
Theorem | modqadd2mod 9376 |
The sum of a number modulo a modulus and another number equals the sum of
the two numbers modulo the modulus. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqm1p1mod0 9377 |
If a number modulo a modulus equals the modulus decreased by 1, the first
number increased by 1 modulo the modulus equals 0. (Contributed by Jim
Kingdon, 24-Oct-2021.)
|
|
|
Theorem | modqltm1p1mod 9378 |
If a number modulo a modulus is less than the modulus decreased by 1, the
first number increased by 1 modulo the modulus equals the first number
modulo the modulus, increased by 1. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqmul1 9379 |
Multiplication property of the modulo operation. Note that the
multiplier
must be an integer. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqmul12d 9380 |
Multiplication property of the modulo operation, see theorem 5.2(b) in
[ApostolNT] p. 107. (Contributed by
Jim Kingdon, 24-Oct-2021.)
|
|
|
Theorem | modqnegd 9381 |
Negation property of the modulo operation. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqadd12d 9382 |
Additive property of the modulo operation. (Contributed by Jim Kingdon,
25-Oct-2021.)
|
|
|
Theorem | modqsub12d 9383 |
Subtraction property of the modulo operation. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modqsubmod 9384 |
The difference of a number modulo a modulus and another number equals the
difference of the two numbers modulo the modulus. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modqsubmodmod 9385 |
The difference of a number modulo a modulus and another number modulo the
same modulus equals the difference of the two numbers modulo the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | q2txmodxeq0 9386 |
Two times a positive number modulo the number is zero. (Contributed by
Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | q2submod 9387 |
If a number is between a modulus and twice the modulus, the first number
modulo the modulus equals the first number minus the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modifeq2int 9388 |
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.)
|
|
|
Theorem | modaddmodup 9389 |
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.)
|
..^
|
|
Theorem | modaddmodlo 9390 |
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.)
|
..^
|
|
Theorem | modqmulmod 9391 |
The product of a rational number modulo a modulus and an integer equals
the product of the rational number and the integer modulo the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modqmulmodr 9392 |
The product of an integer and a rational number modulo a modulus equals
the product of the integer and the rational number modulo the modulus.
(Contributed by Jim Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqaddmulmod 9393 |
The sum of a rational number and the product of a second rational number
modulo a modulus and an integer equals the sum of the rational number and
the product of the other rational number and the integer modulo the
modulus. (Contributed by Jim Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqdi 9394 |
Distribute multiplication over a modulo operation. (Contributed by Jim
Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqsubdir 9395 |
Distribute the modulo operation over a subtraction. (Contributed by Jim
Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqeqmodmin 9396 |
A rational number equals the difference of the rational number and a
modulus modulo the modulus. (Contributed by Jim Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modfzo0difsn 9397* |
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.)
|
..^
..^ ..^ |
|
Theorem | modsumfzodifsn 9398 |
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.)
|
..^
..^
..^ |
|
Theorem | modlteq 9399 |
Two nonnegative integers less than the modulus are equal iff they are
equal modulo the modulus. (Contributed by AV, 14-Mar-2021.)
|
..^ ..^
|
|
Theorem | addmodlteq 9400 |
Two nonnegative integers less than the modulus are equal iff the sums of
these integer with another integer are equal modulo the modulus.
(Contributed by AV, 20-Mar-2021.)
|
..^ ..^
|