Theorem List for Intuitionistic Logic Explorer - 9901-10000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | flqltnz 9901 |
If A is not an integer, then the floor of A is less than A. (Contributed
by Jim Kingdon, 9-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ ¬ 𝐴 ∈ ℤ) →
(⌊‘𝐴) <
𝐴) |
|
Theorem | flqwordi 9902 |
Ordering relationship for the greatest integer function. (Contributed by
Jim Kingdon, 9-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐴) ≤ (⌊‘𝐵)) |
|
Theorem | flqword2 9903 |
Ordering relationship for the greatest integer function. (Contributed by
Jim Kingdon, 9-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐴 ≤ 𝐵) → (⌊‘𝐵) ∈
(ℤ≥‘(⌊‘𝐴))) |
|
Theorem | flqbi 9904 |
A condition equivalent to floor. (Contributed by Jim Kingdon,
9-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ) →
((⌊‘𝐴) = 𝐵 ↔ (𝐵 ≤ 𝐴 ∧ 𝐴 < (𝐵 + 1)))) |
|
Theorem | flqbi2 9905 |
A condition equivalent to floor. (Contributed by Jim Kingdon,
9-Oct-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐹 ∈ ℚ) →
((⌊‘(𝑁 + 𝐹)) = 𝑁 ↔ (0 ≤ 𝐹 ∧ 𝐹 < 1))) |
|
Theorem | adddivflid 9906 |
The floor of a sum of an integer and a fraction is equal to the integer
iff the denominator of the fraction is less than the numerator.
(Contributed by AV, 14-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ) → (𝐵 < 𝐶 ↔ (⌊‘(𝐴 + (𝐵 / 𝐶))) = 𝐴)) |
|
Theorem | flqge0nn0 9907 |
The floor of a number greater than or equal to 0 is a nonnegative integer.
(Contributed by Jim Kingdon, 10-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈
ℕ0) |
|
Theorem | flqge1nn 9908 |
The floor of a number greater than or equal to 1 is a positive integer.
(Contributed by Jim Kingdon, 10-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 1 ≤ 𝐴) → (⌊‘𝐴) ∈
ℕ) |
|
Theorem | fldivnn0 9909 |
The floor function of a division of a nonnegative integer by a positive
integer is a nonnegative integer. (Contributed by Alexander van der
Vekens, 14-Apr-2018.)
|
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) →
(⌊‘(𝐾 / 𝐿)) ∈
ℕ0) |
|
Theorem | divfl0 9910 |
The floor of a fraction is 0 iff the denominator is less than the
numerator. (Contributed by AV, 8-Jul-2021.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (⌊‘(𝐴 / 𝐵)) = 0)) |
|
Theorem | flqaddz 9911 |
An integer can be moved in and out of the floor of a sum. (Contributed by
Jim Kingdon, 10-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℤ) →
(⌊‘(𝐴 + 𝑁)) = ((⌊‘𝐴) + 𝑁)) |
|
Theorem | flqzadd 9912 |
An integer can be moved in and out of the floor of a sum. (Contributed by
Jim Kingdon, 10-Oct-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℚ) →
(⌊‘(𝑁 + 𝐴)) = (𝑁 + (⌊‘𝐴))) |
|
Theorem | flqmulnn0 9913 |
Move a nonnegative integer in and out of a floor. (Contributed by Jim
Kingdon, 10-Oct-2021.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℚ) → (𝑁 · (⌊‘𝐴)) ≤ (⌊‘(𝑁 · 𝐴))) |
|
Theorem | btwnzge0 9914 |
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.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ≤ 𝐴 ∧ 𝐴 < (𝑁 + 1))) → (0 ≤ 𝐴 ↔ 0 ≤ 𝑁)) |
|
Theorem | 2tnp1ge0ge0 9915 |
Two times an integer plus one is not negative iff the integer is not
negative. (Contributed by AV, 19-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (0 ≤ ((2 ·
𝑁) + 1) ↔ 0 ≤
𝑁)) |
|
Theorem | flhalf 9916 |
Ordering relation for the floor of half of an integer. (Contributed by
NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
|
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (2 · (⌊‘((𝑁 + 1) / 2)))) |
|
Theorem | fldivnn0le 9917 |
The floor function of a division of a nonnegative integer by a positive
integer is less than or equal to the division. (Contributed by Alexander
van der Vekens, 14-Apr-2018.)
|
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) →
(⌊‘(𝐾 / 𝐿)) ≤ (𝐾 / 𝐿)) |
|
Theorem | flltdivnn0lt 9918 |
The floor function of a division of a nonnegative integer by a positive
integer is less than the division of a greater dividend by the same
positive integer. (Contributed by Alexander van der Vekens,
14-Apr-2018.)
|
⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐿 ∈ ℕ)
→ (𝐾 < 𝑁 → (⌊‘(𝐾 / 𝐿)) < (𝑁 / 𝐿))) |
|
Theorem | fldiv4p1lem1div2 9919 |
The floor of an integer equal to 3 or greater than 4, increased by 1, is
less than or equal to the half of the integer minus 1. (Contributed by
AV, 8-Jul-2021.)
|
⊢ ((𝑁 = 3 ∨ 𝑁 ∈ (ℤ≥‘5))
→ ((⌊‘(𝑁
/ 4)) + 1) ≤ ((𝑁
− 1) / 2)) |
|
Theorem | ceilqval 9920 |
The value of the ceiling function. (Contributed by Jim Kingdon,
10-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (⌈‘𝐴) = -(⌊‘-𝐴)) |
|
Theorem | ceiqcl 9921 |
The ceiling function returns an integer (closure law). (Contributed by
Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ →
-(⌊‘-𝐴) ∈
ℤ) |
|
Theorem | ceilqcl 9922 |
Closure of the ceiling function. (Contributed by Jim Kingdon,
11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (⌈‘𝐴) ∈
ℤ) |
|
Theorem | ceiqge 9923 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ≤ -(⌊‘-𝐴)) |
|
Theorem | ceilqge 9924 |
The ceiling of a real number is greater than or equal to that number.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 ≤ (⌈‘𝐴)) |
|
Theorem | ceiqm1l 9925 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ →
(-(⌊‘-𝐴)
− 1) < 𝐴) |
|
Theorem | ceilqm1lt 9926 |
One less than the ceiling of a real number is strictly less than that
number. (Contributed by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ →
((⌈‘𝐴) −
1) < 𝐴) |
|
Theorem | ceiqle 9927 |
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 9928 |
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 9929 |
An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.)
|
⊢ (𝐴 ∈ ℤ → (⌈‘𝐴) = 𝐴) |
|
Theorem | ceilqidz 9930 |
A rational number equals its ceiling iff it is an integer. (Contributed
by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴)) |
|
Theorem | flqleceil 9931 |
The floor of a rational number is less than or equal to its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (⌊‘𝐴) ≤ (⌈‘𝐴)) |
|
Theorem | flqeqceilz 9932 |
A rational number is an integer iff its floor equals its ceiling.
(Contributed by Jim Kingdon, 11-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴))) |
|
Theorem | intqfrac2 9933 |
Decompose a real into integer and fractional parts. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
⊢ 𝑍 = (⌊‘𝐴)
& ⊢ 𝐹 = (𝐴 − 𝑍) ⇒ ⊢ (𝐴 ∈ ℚ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹))) |
|
Theorem | intfracq 9934 |
Decompose a rational number, expressed as a ratio, into integer and
fractional parts. The fractional part has a tighter bound than that of
intqfrac2 9933. (Contributed by NM, 16-Aug-2008.)
|
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁)) & ⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) |
|
Theorem | flqdiv 9935 |
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 9936 |
Extend class notation with the modulo operation.
|
class mod |
|
Definition | df-mod 9937* |
Define the modulo (remainder) operation. See modqval 9938 for its value.
For example, (5 mod 3) = 2 and (-7 mod 2) = 1. As with
df-fl 9884 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.)
|
⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) |
|
Theorem | modqval 9938 |
The value of the modulo operation. The modulo congruence notation of
number theory, 𝐽≡𝐾 (modulo 𝑁), can be expressed in
our
notation as (𝐽 mod 𝑁) = (𝐾 mod 𝑁). Definition 1 in Knuth, The
Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses
"mod"
for the operation and "modulo" for the congruence. Unlike
Knuth, we
restrict the second argument to positive 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 9887 we
only prove this for rationals although other particular kinds of real
numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
|
Theorem | modqvalr 9939 |
The value of the modulo operation (multiplication in reversed order).
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵))) |
|
Theorem | modqcl 9940 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) ∈ ℚ) |
|
Theorem | flqpmodeq 9941 |
Partition of a division into its integer part and the remainder.
(Contributed by Jim Kingdon, 16-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) →
(((⌊‘(𝐴 /
𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴) |
|
Theorem | modqcld 9942 |
Closure law for the modulo operation. (Contributed by Jim Kingdon,
16-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℚ) |
|
Theorem | modq0 9943 |
𝐴 mod
𝐵 is zero iff 𝐴 is
evenly divisible by 𝐵. (Contributed
by Jim Kingdon, 17-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 mod 𝐵) = 0 ↔ (𝐴 / 𝐵) ∈ ℤ)) |
|
Theorem | mulqmod0 9944 |
The product of an integer and a positive rational number is 0 modulo the
positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℚ ∧ 0 < 𝑀) → ((𝐴 · 𝑀) mod 𝑀) = 0) |
|
Theorem | negqmod0 9945 |
𝐴
is divisible by 𝐵 iff its negative is. (Contributed
by Jim
Kingdon, 18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 mod 𝐵) = 0 ↔ (-𝐴 mod 𝐵) = 0)) |
|
Theorem | modqge0 9946 |
The modulo operation is nonnegative. (Contributed by Jim Kingdon,
18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → 0 ≤ (𝐴 mod 𝐵)) |
|
Theorem | modqlt 9947 |
The modulo operation is less than its second argument. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) < 𝐵) |
|
Theorem | modqelico 9948 |
Modular reduction produces a half-open interval. (Contributed by Jim
Kingdon, 18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → (𝐴 mod 𝐵) ∈ (0[,)𝐵)) |
|
Theorem | modqdiffl 9949 |
The modulo operation differs from 𝐴 by an integer multiple of 𝐵.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) = (⌊‘(𝐴 / 𝐵))) |
|
Theorem | modqdifz 9950 |
The modulo operation differs from 𝐴 by an integer multiple of 𝐵.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ) |
|
Theorem | modqfrac 9951 |
The fractional part of a number is the number modulo 1. (Contributed by
Jim Kingdon, 18-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴))) |
|
Theorem | flqmod 9952 |
The floor function expressed in terms of the modulo operation.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1))) |
|
Theorem | intqfrac 9953 |
Break a number into its integer part and its fractional part.
(Contributed by Jim Kingdon, 18-Oct-2021.)
|
⊢ (𝐴 ∈ ℚ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1))) |
|
Theorem | zmod10 9954 |
An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0) |
|
Theorem | zmod1congr 9955 |
Two arbitrary integers are congruent modulo 1, see example 4 in
[ApostolNT] p. 107. (Contributed by AV,
21-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 mod 1) = (𝐵 mod 1)) |
|
Theorem | modqmulnn 9956 |
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.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℚ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀))) |
|
Theorem | modqvalp1 9957 |
The value of the modulo operation (expressed with sum of denominator and
nominator). (Contributed by Jim Kingdon, 20-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 + 𝐵) − (((⌊‘(𝐴 / 𝐵)) + 1) · 𝐵)) = (𝐴 mod 𝐵)) |
|
Theorem | zmodcl 9958 |
Closure law for the modulo operation restricted to integers. (Contributed
by NM, 27-Nov-2008.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈
ℕ0) |
|
Theorem | zmodcld 9959 |
Closure law for the modulo operation restricted to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℕ)
⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈
ℕ0) |
|
Theorem | zmodfz 9960 |
An integer mod 𝐵 lies in the first 𝐵
nonnegative integers.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...(𝐵 − 1))) |
|
Theorem | zmodfzo 9961 |
An integer mod 𝐵 lies in the first 𝐵
nonnegative integers.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0..^𝐵)) |
|
Theorem | zmodfzp1 9962 |
An integer mod 𝐵 lies in the first 𝐵 + 1
nonnegative integers.
(Contributed by AV, 27-Oct-2018.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...𝐵)) |
|
Theorem | modqid 9963 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴) |
|
Theorem | modqid0 9964 |
A positive real number modulo itself is 0. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
⊢ ((𝑁 ∈ ℚ ∧ 0 < 𝑁) → (𝑁 mod 𝑁) = 0) |
|
Theorem | modqid2 9965 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 mod 𝐵) = 𝐴 ↔ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵))) |
|
Theorem | zmodid2 9966 |
Identity law for modulo restricted to integers. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0...(𝑁 − 1)))) |
|
Theorem | zmodidfzo 9967 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0..^𝑁))) |
|
Theorem | zmodidfzoimp 9968 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
⊢ (𝑀 ∈ (0..^𝑁) → (𝑀 mod 𝑁) = 𝑀) |
|
Theorem | q0mod 9969 |
Special case: 0 modulo a positive real number is 0. (Contributed by Jim
Kingdon, 21-Oct-2021.)
|
⊢ ((𝑁 ∈ ℚ ∧ 0 < 𝑁) → (0 mod 𝑁) = 0) |
|
Theorem | q1mod 9970 |
Special case: 1 modulo a real number greater than 1 is 1. (Contributed by
Jim Kingdon, 21-Oct-2021.)
|
⊢ ((𝑁 ∈ ℚ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1) |
|
Theorem | modqabs 9971 |
Absorption law for modulo. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐵)
& ⊢ (𝜑 → 𝐶 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 mod 𝐵) mod 𝐶) = (𝐴 mod 𝐵)) |
|
Theorem | modqabs2 9972 |
Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) → ((𝐴 mod 𝐵) mod 𝐵) = (𝐴 mod 𝐵)) |
|
Theorem | modqcyc 9973 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℤ) ∧ (𝐵 ∈ ℚ ∧ 0 < 𝐵)) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵)) |
|
Theorem | modqcyc2 9974 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℤ) ∧ (𝐵 ∈ ℚ ∧ 0 < 𝐵)) → ((𝐴 − (𝐵 · 𝑁)) mod 𝐵) = (𝐴 mod 𝐵)) |
|
Theorem | modqadd1 9975 |
Addition property of the modulo operation. (Contributed by Jim Kingdon,
22-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 𝐶 ∈ ℚ) & ⊢ (𝜑 → 𝐷 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐷)
& ⊢ (𝜑 → (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) |
|
Theorem | modqaddabs 9976 |
Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ (𝐶 ∈ ℚ ∧ 0 < 𝐶)) → (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) |
|
Theorem | modqaddmod 9977 |
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.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ (𝑀 ∈ ℚ ∧ 0 < 𝑀)) → (((𝐴 mod 𝑀) + 𝐵) mod 𝑀) = ((𝐴 + 𝐵) mod 𝑀)) |
|
Theorem | mulqaddmodid 9978 |
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.)
|
⊢ (((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℚ) ∧ (𝐴 ∈ ℚ ∧ 𝐴 ∈ (0[,)𝑀))) → (((𝑁 · 𝑀) + 𝐴) mod 𝑀) = 𝐴) |
|
Theorem | mulp1mod1 9979 |
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.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘2))
→ (((𝑁 · 𝐴) + 1) mod 𝑁) = 1) |
|
Theorem | modqmuladd 9980* |
Decomposition of an integer into a multiple of a modulus and a
remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ (0[,)𝑀)) & ⊢ (𝜑 → 𝑀 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝑀) ⇒ ⊢ (𝜑 → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |
|
Theorem | modqmuladdim 9981* |
Implication of a decomposition of an integer into a multiple of a
modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℚ ∧ 0 < 𝑀) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |
|
Theorem | modqmuladdnn0 9982* |
Implication of a decomposition of a nonnegative integer into a multiple
of a modulus and a remainder. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℚ ∧ 0 <
𝑀) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) |
|
Theorem | qnegmod 9983 |
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.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → (-𝐴 mod 𝑁) = ((𝑁 − 𝐴) mod 𝑁)) |
|
Theorem | m1modnnsub1 9984 |
Minus one modulo a positive integer is equal to the integer minus one.
(Contributed by AV, 14-Jul-2021.)
|
⊢ (𝑀 ∈ ℕ → (-1 mod 𝑀) = (𝑀 − 1)) |
|
Theorem | m1modge3gt1 9985 |
Minus one modulo an integer greater than two is greater than one.
(Contributed by AV, 14-Jul-2021.)
|
⊢ (𝑀 ∈ (ℤ≥‘3)
→ 1 < (-1 mod 𝑀)) |
|
Theorem | addmodid 9986 |
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.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀) → ((𝑀 + 𝐴) mod 𝑀) = 𝐴) |
|
Theorem | addmodidr 9987 |
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.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀) → ((𝐴 + 𝑀) mod 𝑀) = 𝐴) |
|
Theorem | modqadd2mod 9988 |
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.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ (𝑀 ∈ ℚ ∧ 0 < 𝑀)) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀)) |
|
Theorem | modqm1p1mod0 9989 |
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.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 0 < 𝑀) → ((𝐴 mod 𝑀) = (𝑀 − 1) → ((𝐴 + 1) mod 𝑀) = 0)) |
|
Theorem | modqltm1p1mod 9990 |
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.)
|
⊢ (((𝐴 ∈ ℚ ∧ (𝐴 mod 𝑀) < (𝑀 − 1)) ∧ (𝑀 ∈ ℚ ∧ 0 < 𝑀)) → ((𝐴 + 1) mod 𝑀) = ((𝐴 mod 𝑀) + 1)) |
|
Theorem | modqmul1 9991 |
Multiplication property of the modulo operation. Note that the
multiplier 𝐶 must be an integer. (Contributed by
Jim Kingdon,
24-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐷)
& ⊢ (𝜑 → (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) mod 𝐷) = ((𝐵 · 𝐶) mod 𝐷)) |
|
Theorem | modqmul12d 9992 |
Multiplication property of the modulo operation, see theorem 5.2(b) in
[ApostolNT] p. 107. (Contributed by
Jim Kingdon, 24-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝐸 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐸)
& ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) mod 𝐸) = ((𝐵 · 𝐷) mod 𝐸)) |
|
Theorem | modqnegd 9993 |
Negation property of the modulo operation. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 𝐶 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐶)
& ⊢ (𝜑 → (𝐴 mod 𝐶) = (𝐵 mod 𝐶)) ⇒ ⊢ (𝜑 → (-𝐴 mod 𝐶) = (-𝐵 mod 𝐶)) |
|
Theorem | modqadd12d 9994 |
Additive property of the modulo operation. (Contributed by Jim Kingdon,
25-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 𝐶 ∈ ℚ) & ⊢ (𝜑 → 𝐷 ∈ ℚ) & ⊢ (𝜑 → 𝐸 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐸)
& ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐸) = ((𝐵 + 𝐷) mod 𝐸)) |
|
Theorem | modqsub12d 9995 |
Subtraction property of the modulo operation. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → 𝐶 ∈ ℚ) & ⊢ (𝜑 → 𝐷 ∈ ℚ) & ⊢ (𝜑 → 𝐸 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐸)
& ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐶) mod 𝐸) = ((𝐵 − 𝐷) mod 𝐸)) |
|
Theorem | modqsubmod 9996 |
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.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ (𝑀 ∈ ℚ ∧ 0 < 𝑀)) → (((𝐴 mod 𝑀) − 𝐵) mod 𝑀) = ((𝐴 − 𝐵) mod 𝑀)) |
|
Theorem | modqsubmodmod 9997 |
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.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) ∧ (𝑀 ∈ ℚ ∧ 0 < 𝑀)) → (((𝐴 mod 𝑀) − (𝐵 mod 𝑀)) mod 𝑀) = ((𝐴 − 𝐵) mod 𝑀)) |
|
Theorem | q2txmodxeq0 9998 |
Two times a positive number modulo the number is zero. (Contributed by
Jim Kingdon, 25-Oct-2021.)
|
⊢ ((𝑋 ∈ ℚ ∧ 0 < 𝑋) → ((2 · 𝑋) mod 𝑋) = 0) |
|
Theorem | q2submod 9999 |
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.)
|
⊢ (((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 0 < 𝐵) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < (2 · 𝐵))) → (𝐴 mod 𝐵) = (𝐴 − 𝐵)) |
|
Theorem | modifeq2int 10000 |
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.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < (2 · 𝐵)) → (𝐴 mod 𝐵) = if(𝐴 < 𝐵, 𝐴, (𝐴 − 𝐵))) |