Theorem List for Intuitionistic Logic Explorer - 10101-10200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | flqaddz 10101 |
An integer can be moved in and out of the floor of a sum. (Contributed by
Jim Kingdon, 10-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flqzadd 10102 |
An integer can be moved in and out of the floor of a sum. (Contributed by
Jim Kingdon, 10-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flqmulnn0 10103 |
Move a nonnegative integer in and out of a floor. (Contributed by Jim
Kingdon, 10-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | btwnzge0 10104 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2tnp1ge0ge0 10105 |
Two times an integer plus one is not negative iff the integer is not
negative. (Contributed by AV, 19-Jun-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![N N](_cn.gif)
![1 1](1.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flhalf 10106 |
Ordering relation for the floor of half of an integer. (Contributed by
NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
|
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fldivnn0le 10107 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![L L](_cl.gif) ![) )](rp.gif) ![( (](lp.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flltdivnn0lt 10108 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![L L](_cl.gif) ![) )](rp.gif) ![(
(](lp.gif) ![L L](_cl.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | fldiv4p1lem1div2 10109 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![5 5](5.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | ceilqval 10110 |
The value of the ceiling function. (Contributed by Jim Kingdon,
10-Oct-2021.)
|
![( (](lp.gif) ⌈![`
`](backtick.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ceiqcl 10111 |
The ceiling function returns an integer (closure law). (Contributed by
Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | ceilqcl 10112 |
Closure of the ceiling function. (Contributed by Jim Kingdon,
11-Oct-2021.)
|
![( (](lp.gif) ⌈![`
`](backtick.gif) ![A A](_ca.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | ceiqge 10113 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ceilqge 10114 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif)
⌈![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ceiqm1l 10115 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![1 1](1.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ceilqm1lt 10116 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ⌈![` `](backtick.gif) ![A A](_ca.gif) ![1 1](1.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ceiqle 10117 |
The ceiling of a real number is the smallest integer greater than or equal
to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ceilqle 10118 |
The ceiling of a real number is the smallest integer greater than or equal
to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ⌈![`
`](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | ceilid 10119 |
An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
|
![( (](lp.gif) ⌈![`
`](backtick.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | ceilqidz 10120 |
A rational number equals its ceiling iff it is an integer. (Contributed
by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ⌈![` `](backtick.gif) ![A A](_ca.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flqleceil 10121 |
The floor of a rational number is less than or equal to its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ⌈![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) |
|
Theorem | flqeqceilz 10122 |
A rational number is an integer iff its floor equals its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ⌈![`
`](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | intqfrac2 10123 |
Decompose a real into integer and fractional parts. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![Z Z](_cz.gif) ![( (](lp.gif)
![( (](lp.gif)
![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | intfracq 10124 |
Decompose a rational number, expressed as a ratio, into integer and
fractional parts. The fractional part has a tighter bound than that of
intqfrac2 10123. (Contributed by NM, 16-Aug-2008.)
|
![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![Z Z](_cz.gif) ![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![N N](_cn.gif)
![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![F F](_cf.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flqdiv 10125 |
Cancellation of the embedded floor of a real divided by an integer.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
4.6.2 The modulo (remainder)
operation
|
|
Syntax | cmo 10126 |
Extend class notation with the modulo operation.
|
![mod mod](_mod.gif) |
|
Definition | df-mod 10127* |
Define the modulo (remainder) operation. See modqval 10128 for its value.
For example, ![( (](lp.gif) ![3 3](3.gif) and ![( (](lp.gif) ![-u -u](shortminus.gif) ![2 2](2.gif) . As with
df-fl 10074 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.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqval 10128 |
The value of the modulo operation. The modulo congruence notation of
number theory,
(modulo ), can be expressed in our
notation as ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N N](_cn.gif) . 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 10077 we
only prove this for rationals although other particular kinds of real
numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqvalr 10129 |
The value of the modulo operation (multiplication in reversed order).
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqcl 10130 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif)
![QQ QQ](bbq.gif) ![) )](rp.gif) |
|
Theorem | flqpmodeq 10131 |
Partition of a division into its integer part and the remainder.
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | modqcld 10132 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![QQ
QQ](bbq.gif) ![) )](rp.gif) |
|
Theorem | modq0 10133 |
is zero iff is evenly divisible by . (Contributed
by Jim Kingdon, 17-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif)
![ZZ ZZ](bbz.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulqmod0 10134 |
The product of an integer and a positive rational number is 0 modulo the
positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif)
![M M](_cm.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | negqmod0 10135 |
is divisible by iff its negative is.
(Contributed by Jim
Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqge0 10136 |
The modulo operation is nonnegative. (Contributed by Jim Kingdon,
18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqlt 10137 |
The modulo operation is less than its second argument. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | modqelico 10138 |
Modular reduction produces a half-open interval. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![0 0](0.gif) ![[,) [,)](_ico.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqdiffl 10139 |
The modulo operation differs from by an integer multiple of .
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqdifz 10140 |
The modulo operation differs from by an integer multiple of .
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | modqfrac 10141 |
The fractional part of a number is the number modulo 1. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | flqmod 10142 |
The floor function expressed in terms of the modulo operation.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | intqfrac 10143 |
Break a number into its integer part and its fractional part.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmod10 10144 |
An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | zmod1congr 10145 |
Two arbitrary integers are congruent modulo 1, see example 4 in
[ApostolNT] p. 107. (Contributed by AV,
21-Jul-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmulnn 10146 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqvalp1 10147 |
The value of the modulo operation (expressed with sum of denominator and
nominator). (Contributed by Jim Kingdon, 20-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![1 1](1.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmodcl 10148 |
Closure law for the modulo operation restricted to integers. (Contributed
by NM, 27-Nov-2008.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![B B](_cb.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
|
Theorem | zmodcld 10149 |
Closure law for the modulo operation restricted to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![NN0 NN0](_bbn0.gif) ![) )](rp.gif) |
|
Theorem | zmodfz 10150 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![0 0](0.gif) ![...
...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmodfzo 10151 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ..^![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmodfzp1 10152 |
An integer mod lies
in the first nonnegative integers.
(Contributed by AV, 27-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![0 0](0.gif) ![...
...](ldots.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqid 10153 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | modqid0 10154 |
A positive real number modulo itself is 0. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N N](_cn.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | modqid2 10155 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmodid2 10156 |
Identity law for modulo restricted to integers. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![0 0](0.gif) ![... ...](ldots.gif) ![( (](lp.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmodidfzo 10157 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | zmodidfzoimp 10158 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![( (](lp.gif)
![N N](_cn.gif) ![M M](_cm.gif) ![) )](rp.gif) |
|
Theorem | q0mod 10159 |
Special case: 0 modulo a positive real number is 0. (Contributed by Jim
Kingdon, 21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N
N](_cn.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | q1mod 10160 |
Special case: 1 modulo a real number greater than 1 is 1. (Contributed by
Jim Kingdon, 21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N
N](_cn.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | modqabs 10161 |
Absorption law for modulo. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqabs2 10162 |
Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqcyc 10163 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqcyc2 10164 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N N](_cn.gif) ![) )](rp.gif)
![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqadd1 10165 |
Addition property of the modulo operation. (Contributed by Jim Kingdon,
22-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqaddabs 10166 |
Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqaddmod 10167 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![B B](_cb.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulqaddmodid 10168 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![( (](lp.gif) ![0 0](0.gif) ![[,) [,)](_ico.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![A A](_ca.gif)
![M M](_cm.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mulp1mod1 10169 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![1 1](1.gif)
![N N](_cn.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | modqmuladd 10170* |
Decomposition of an integer into a multiple of a modulus and a
remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![( (](lp.gif) ![0
0](0.gif) ![[,) [,)](_ico.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif)
![QQ QQ](bbq.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif)
![E. E.](exists.gif)
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmuladdim 10171* |
Implication of a decomposition of an integer into a multiple of a
modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmuladdnn0 10172* |
Implication of a decomposition of a nonnegative integer into a multiple
of a modulus and a remainder. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | qnegmod 10173 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![N N](_cn.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | m1modnnsub1 10174 |
Minus one modulo a positive integer is equal to the integer minus one.
(Contributed by AV, 14-Jul-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif)
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | m1modge3gt1 10175 |
Minus one modulo an integer greater than two is greater than one.
(Contributed by AV, 14-Jul-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![3 3](3.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addmodid 10176 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![M M](_cm.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | addmodidr 10177 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif)
![M M](_cm.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | modqadd2mod 10178 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqm1p1mod0 10179 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![M M](_cm.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqltm1p1mod 10180 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![(
(](lp.gif) ![1 1](1.gif) ![)
)](rp.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmul1 10181 |
Multiplication property of the modulo operation. Note that the
multiplier
must be an integer. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmul12d 10182 |
Multiplication property of the modulo operation, see theorem 5.2(b) in
[ApostolNT] p. 107. (Contributed by
Jim Kingdon, 24-Oct-2021.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqnegd 10183 |
Negation property of the modulo operation. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![C C](_cc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqadd12d 10184 |
Additive property of the modulo operation. (Contributed by Jim Kingdon,
25-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqsub12d 10185 |
Subtraction property of the modulo operation. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![( (](lp.gif) ![E E](_ce.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![E E](_ce.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![E E](_ce.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqsubmod 10186 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![B B](_cb.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqsubmodmod 10187 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | q2txmodxeq0 10188 |
Two times a positive number modulo the number is zero. (Contributed by
Jim Kingdon, 25-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![( (](lp.gif) ![( (](lp.gif) ![X X](_cx.gif) ![X X](_cx.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | q2submod 10189 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modifeq2int 10190 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![if if](_if.gif) ![( (](lp.gif) ![B B](_cb.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modaddmodup 10191 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ..^![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modaddmodlo 10192 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ..^![( (](lp.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmulmod 10193 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![B B](_cb.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqmulmodr 10194 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![M M](_cm.gif) ![) )](rp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqaddmulmod 10195 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif)
![( (](lp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![C C](_cc.gif) ![) )](rp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqdi 10196 |
Distribute multiplication over a modulo operation. (Contributed by Jim
Kingdon, 26-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqsubdir 10197 |
Distribute the modulo operation over a subtraction. (Contributed by Jim
Kingdon, 26-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modqeqmodmin 10198 |
A rational number equals the difference of the rational number and a
modulus modulo the modulus. (Contributed by Jim Kingdon, 26-Oct-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![( (](lp.gif) ![M M](_cm.gif)
![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif) ![M M](_cm.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modfzo0difsn 10199* |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ..^![N N](_cn.gif)
![( (](lp.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![{ {](lbrace.gif) ![J J](_cj.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![J J](_cj.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | modsumfzodifsn 10200 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ..^![N N](_cn.gif)
![( (](lp.gif) ..^![N N](_cn.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![J J](_cj.gif)
![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ..^![N N](_cn.gif) ![{ {](lbrace.gif) ![J J](_cj.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |