Home | Metamath
Proof Explorer Theorem List (p. 133 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ceicl 13201 | The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ (𝐴 ∈ ℝ → -(⌊‘-𝐴) ∈ ℤ) | ||
Theorem | ceilcl 13202 | Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) |
⊢ (𝐴 ∈ ℝ → (⌈‘𝐴) ∈ ℤ) | ||
Theorem | ceige 13203 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ -(⌊‘-𝐴)) | ||
Theorem | ceilge 13204 | The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (⌈‘𝐴)) | ||
Theorem | ceim1l 13205 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ (𝐴 ∈ ℝ → (-(⌊‘-𝐴) − 1) < 𝐴) | ||
Theorem | ceilm1lt 13206 | One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → ((⌈‘𝐴) − 1) < 𝐴) | ||
Theorem | ceile 13207 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jeff Hankins, 10-Jun-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → -(⌊‘-𝐴) ≤ 𝐵) | ||
Theorem | ceille 13208 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵) → (⌈‘𝐴) ≤ 𝐵) | ||
Theorem | ceilid 13209 | An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℤ → (⌈‘𝐴) = 𝐴) | ||
Theorem | ceilidz 13210 | A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌈‘𝐴) = 𝐴)) | ||
Theorem | flleceil 13211 | The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ (⌈‘𝐴)) | ||
Theorem | fleqceilz 13212 | A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (⌊‘𝐴) = (⌈‘𝐴))) | ||
Theorem | quoremz 13213 | Quotient and remainder of an integer divided by a positive integer. TODO - is this really needed for anything? Should we use mod to simplify it? Remark (AV): This is a special case of divalg 15744. (Contributed by NM, 14-Aug-2008.) |
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) & ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) | ||
Theorem | quoremnn0 13214 | Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.) |
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) & ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) ⇒ ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) | ||
Theorem | quoremnn0ALT 13215 | Alternate proof of quoremnn0 13214 not using quoremz 13213. TODO - Keep either quoremnn0ALT 13215 (if we don't keep quoremz 13213) or quoremnn0 13214? (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) & ⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) ⇒ ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → ((𝑄 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) | ||
Theorem | intfrac2 13216 | Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 13244? (Contributed by NM, 16-Aug-2008.) |
⊢ 𝑍 = (⌊‘𝐴) & ⊢ 𝐹 = (𝐴 − 𝑍) ⇒ ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐹 ∧ 𝐹 < 1 ∧ 𝐴 = (𝑍 + 𝐹))) | ||
Theorem | intfracq 13217 | Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 13216. (Contributed by NM, 16-Aug-2008.) |
⊢ 𝑍 = (⌊‘(𝑀 / 𝑁)) & ⊢ 𝐹 = ((𝑀 / 𝑁) − 𝑍) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (0 ≤ 𝐹 ∧ 𝐹 ≤ ((𝑁 − 1) / 𝑁) ∧ (𝑀 / 𝑁) = (𝑍 + 𝐹))) | ||
Theorem | fldiv 13218 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘𝐴) / 𝑁)) = (⌊‘(𝐴 / 𝑁))) | ||
Theorem | fldiv2 13219 | Cancellation of an embedded floor of a ratio. Generalization of Equation 2.4 in [CormenLeisersonRivest] p. 33 (where 𝐴 must be an integer). (Contributed by NM, 9-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (⌊‘((⌊‘(𝐴 / 𝑀)) / 𝑁)) = (⌊‘(𝐴 / (𝑀 · 𝑁)))) | ||
Theorem | fznnfl 13220 | Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ (𝑁 ∈ ℝ → (𝐾 ∈ (1...(⌊‘𝑁)) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | uzsup 13221 | An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞) | ||
Theorem | ioopnfsup 13222 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴(,)+∞), ℝ*, < ) = +∞) | ||
Theorem | icopnfsup 13223 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴[,)+∞), ℝ*, < ) = +∞) | ||
Theorem | rpsup 13224 | The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ sup(ℝ+, ℝ*, < ) = +∞ | ||
Theorem | resup 13225 | The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ sup(ℝ, ℝ*, < ) = +∞ | ||
Theorem | xrsup 13226 | The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ sup(ℝ*, ℝ*, < ) = +∞ | ||
Syntax | cmo 13227 | Extend class notation with the modulo operation. |
class mod | ||
Definition | df-mod 13228* | Define the modulo (remainder) operation. See modval 13229 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 28156). (Contributed by NM, 10-Nov-2008.) |
⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) | ||
Theorem | modval 13229 | 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 reals to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) (Contributed by NM, 10-Nov-2008.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | ||
Theorem | modvalr 13230 | The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵))) | ||
Theorem | modcl 13231 | Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ ℝ) | ||
Theorem | flpmodeq 13232 | Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴) | ||
Theorem | modcld 13233 | Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℝ) | ||
Theorem | mod0 13234 | 𝐴 mod 𝐵 is zero iff 𝐴 is evenly divisible by 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ (𝐴 / 𝐵) ∈ ℤ)) | ||
Theorem | mulmod0 13235 | The product of an integer and a positive real number is 0 modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) (Revised by AV, 5-Jul-2020.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → ((𝐴 · 𝑀) mod 𝑀) = 0) | ||
Theorem | negmod0 13236 | 𝐴 is divisible by 𝐵 iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Fan Zheng, 7-Jun-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ (-𝐴 mod 𝐵) = 0)) | ||
Theorem | modge0 13237 | The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵)) | ||
Theorem | modlt 13238 | The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵) | ||
Theorem | modelico 13239 | Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵)) | ||
Theorem | moddiffl 13240 | Value of the modulo operation rewritten to give two ways of expressing the quotient when "𝐴 is divided by 𝐵 using Euclidean division." Multiplying both sides by 𝐵, this implies that 𝐴 mod 𝐵 differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Jeff Madsen, 17-Jun-2010.) (Revised by Mario Carneiro, 6-Sep-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) = (⌊‘(𝐴 / 𝐵))) | ||
Theorem | moddifz 13241 | The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ) | ||
Theorem | modfrac 13242 | The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴))) | ||
Theorem | flmod 13243 | The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1))) | ||
Theorem | intfrac 13244 | Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.) |
⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1))) | ||
Theorem | zmod10 13245 | An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0) | ||
Theorem | zmod1congr 13246 | 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 | modmulnn 13247 | Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by NM, 2-Jan-2009.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ) → ((𝑁 · (⌊‘𝐴)) mod (𝑁 · 𝑀)) ≤ ((⌊‘(𝑁 · 𝐴)) mod (𝑁 · 𝑀))) | ||
Theorem | modvalp1 13248 | The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 + 𝐵) − (((⌊‘(𝐴 / 𝐵)) + 1) · 𝐵)) = (𝐴 mod 𝐵)) | ||
Theorem | zmodcl 13249 | Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ ℕ0) | ||
Theorem | zmodcld 13250 | Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℕ0) | ||
Theorem | zmodfz 13251 | An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...(𝐵 − 1))) | ||
Theorem | zmodfzo 13252 | An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0..^𝐵)) | ||
Theorem | zmodfzp1 13253 | An integer mod 𝐵 lies in the first 𝐵 + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...𝐵)) | ||
Theorem | modid 13254 | Identity law for modulo. (Contributed by NM, 29-Dec-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴) | ||
Theorem | modid0 13255 | A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.) |
⊢ (𝑁 ∈ ℝ+ → (𝑁 mod 𝑁) = 0) | ||
Theorem | modid2 13256 | Identity law for modulo. (Contributed by NM, 29-Dec-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 𝐴 ↔ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | zmodid2 13257 | Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0...(𝑁 − 1)))) | ||
Theorem | zmodidfzo 13258 | Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0..^𝑁))) | ||
Theorem | zmodidfzoimp 13259 | Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.) |
⊢ (𝑀 ∈ (0..^𝑁) → (𝑀 mod 𝑁) = 𝑀) | ||
Theorem | 0mod 13260 | Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014.) |
⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0) | ||
Theorem | 1mod 13261 | Special case: 1 modulo a real number greater than 1 is 1. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1) | ||
Theorem | modabs 13262 | Absorption law for modulo. (Contributed by NM, 29-Dec-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) ∧ 𝐵 ≤ 𝐶) → ((𝐴 mod 𝐵) mod 𝐶) = (𝐴 mod 𝐵)) | ||
Theorem | modabs2 13263 | Absorption law for modulo. (Contributed by NM, 29-Dec-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) mod 𝐵) = (𝐴 mod 𝐵)) | ||
Theorem | modcyc 13264 | The modulo operation is periodic. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵)) | ||
Theorem | modcyc2 13265 | The modulo operation is periodic. (Contributed by NM, 12-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 − (𝐵 · 𝑁)) mod 𝐵) = (𝐴 mod 𝐵)) | ||
Theorem | modadd1 13266 | Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) | ||
Theorem | modaddabs 13267 | Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) | ||
Theorem | modaddmod 13268 | The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) + 𝐵) mod 𝑀) = ((𝐴 + 𝐵) mod 𝑀)) | ||
Theorem | muladdmodid 13269 | The sum of a positive real number less than an upper bound and the product of an integer and the upper bound is the positive real number modulo the upper bound. (Contributed by AV, 5-Jul-2020.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ∧ 𝐴 ∈ (0[,)𝑀)) → (((𝑁 · 𝑀) + 𝐴) mod 𝑀) = 𝐴) | ||
Theorem | mulp1mod1 13270 | 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 | modmuladd 13271* | Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) | ||
Theorem | modmuladdim 13272* | Implication of a decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) | ||
Theorem | modmuladdnn0 13273* | Implication of a decomposition of a nonnegative integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 → ∃𝑘 ∈ ℕ0 𝐴 = ((𝑘 · 𝑀) + 𝐵))) | ||
Theorem | negmod 13274 | 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 AV, 5-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (-𝐴 mod 𝑁) = ((𝑁 − 𝐴) mod 𝑁)) | ||
Theorem | m1modnnsub1 13275 | Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.) |
⊢ (𝑀 ∈ ℕ → (-1 mod 𝑀) = (𝑀 − 1)) | ||
Theorem | m1modge3gt1 13276 | Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.) |
⊢ (𝑀 ∈ (ℤ≥‘3) → 1 < (-1 mod 𝑀)) | ||
Theorem | addmodid 13277 | 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 13278 | 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 | modadd2mod 13279 | The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → ((𝐵 + (𝐴 mod 𝑀)) mod 𝑀) = ((𝐵 + 𝐴) mod 𝑀)) | ||
Theorem | modm1p1mod0 13280 | If a real number modulo a positive real number equals the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals 0. (Contributed by AV, 2-Nov-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = (𝑀 − 1) → ((𝐴 + 1) mod 𝑀) = 0)) | ||
Theorem | modltm1p1mod 13281 | If a real number modulo a positive real number is less than the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals the real number modulo the positive real number increased by 1. (Contributed by AV, 2-Nov-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ (𝐴 mod 𝑀) < (𝑀 − 1)) → ((𝐴 + 1) mod 𝑀) = ((𝐴 mod 𝑀) + 1)) | ||
Theorem | modmul1 13282 | Multiplication property of the modulo operation. Note that the multiplier 𝐶 must be an integer. (Contributed by NM, 12-Nov-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 · 𝐶) mod 𝐷) = ((𝐵 · 𝐶) mod 𝐷)) | ||
Theorem | modmul12d 13283 | Multiplication property of the modulo operation, see theorem 5.2(b) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 5-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) mod 𝐸) = ((𝐵 · 𝐷) mod 𝐸)) | ||
Theorem | modnegd 13284 | Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐶) = (𝐵 mod 𝐶)) ⇒ ⊢ (𝜑 → (-𝐴 mod 𝐶) = (-𝐵 mod 𝐶)) | ||
Theorem | modadd12d 13285 | Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐸) = ((𝐵 + 𝐷) mod 𝐸)) | ||
Theorem | modsub12d 13286 | Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐶) mod 𝐸) = ((𝐵 − 𝐷) mod 𝐸)) | ||
Theorem | modsubmod 13287 | The difference of a real number modulo a positive real number and another real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) − 𝐵) mod 𝑀) = ((𝐴 − 𝐵) mod 𝑀)) | ||
Theorem | modsubmodmod 13288 | The difference of a real number modulo a positive real number and another real number modulo this positive real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) − (𝐵 mod 𝑀)) mod 𝑀) = ((𝐴 − 𝐵) mod 𝑀)) | ||
Theorem | 2txmodxeq0 13289 | Two times a positive real number modulo the real number is zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ (𝑋 ∈ ℝ+ → ((2 · 𝑋) mod 𝑋) = 0) | ||
Theorem | 2submod 13290 | If a real number is between a positive real number and twice the positive real number, the real number modulo the positive real number equals the real number minus the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (𝐵 ≤ 𝐴 ∧ 𝐴 < (2 · 𝐵))) → (𝐴 mod 𝐵) = (𝐴 − 𝐵)) | ||
Theorem | modifeq2int 13291 | 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(𝐴 < 𝐵, 𝐴, (𝐴 − 𝐵))) | ||
Theorem | modaddmodup 13292 | 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.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ ((𝑀 − (𝐴 mod 𝑀))..^𝑀) → ((𝐵 + (𝐴 mod 𝑀)) − 𝑀) = ((𝐵 + 𝐴) mod 𝑀))) | ||
Theorem | modaddmodlo 13293 | 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.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝐵 ∈ (0..^(𝑀 − (𝐴 mod 𝑀))) → (𝐵 + (𝐴 mod 𝑀)) = ((𝐵 + 𝐴) mod 𝑀))) | ||
Theorem | modmulmod 13294 | The product of a real number modulo a positive real number and an integer equals the product of the real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℝ+) → (((𝐴 mod 𝑀) · 𝐵) mod 𝑀) = ((𝐴 · 𝐵) mod 𝑀)) | ||
Theorem | modmulmodr 13295 | The product of an integer and a real number modulo a positive real number equals the product of the integer and the real number modulo the positive real number. (Contributed by Alexander van der Vekens, 9-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → ((𝐴 · (𝐵 mod 𝑀)) mod 𝑀) = ((𝐴 · 𝐵) mod 𝑀)) | ||
Theorem | modaddmulmod 13296 | The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℤ) ∧ 𝑀 ∈ ℝ+) → ((𝐴 + ((𝐵 mod 𝑀) · 𝐶)) mod 𝑀) = ((𝐴 + (𝐵 · 𝐶)) mod 𝑀)) | ||
Theorem | moddi 13297 | Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (𝐴 · (𝐵 mod 𝐶)) = ((𝐴 · 𝐵) mod (𝐴 · 𝐶))) | ||
Theorem | modsubdir 13298 | Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → ((𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)))) | ||
Theorem | modeqmodmin 13299 | A real number equals the difference of the real number and a positive real number modulo the positive real number. (Contributed by AV, 3-Nov-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+) → (𝐴 mod 𝑀) = ((𝐴 − 𝑀) mod 𝑀)) | ||
Theorem | modirr 13300 | A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐴 / 𝐵) ∈ (ℝ ∖ ℚ)) → (𝐴 mod 𝐵) ≠ 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |