| Metamath
Proof Explorer Theorem List (p. 140 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fldiv2 13901 | 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 13902 | Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.) |
| ⊢ (𝑁 ∈ ℝ → (𝐾 ∈ (1...(⌊‘𝑁)) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁))) | ||
| Theorem | uzsup 13903 | An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → sup(𝑍, ℝ*, < ) = +∞) | ||
| Theorem | ioopnfsup 13904 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴(,)+∞), ℝ*, < ) = +∞) | ||
| Theorem | icopnfsup 13905 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) → sup((𝐴[,)+∞), ℝ*, < ) = +∞) | ||
| Theorem | rpsup 13906 | The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
| ⊢ sup(ℝ+, ℝ*, < ) = +∞ | ||
| Theorem | resup 13907 | The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
| ⊢ sup(ℝ, ℝ*, < ) = +∞ | ||
| Theorem | xrsup 13908 | The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
| ⊢ sup(ℝ*, ℝ*, < ) = +∞ | ||
| Syntax | cmo 13909 | Extend class notation with the modulo operation. |
| class mod | ||
| Definition | df-mod 13910* | Define the modulo (remainder) operation. See modval 13911 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 30468). (Contributed by NM, 10-Nov-2008.) |
| ⊢ mod = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ+ ↦ (𝑥 − (𝑦 · (⌊‘(𝑥 / 𝑦))))) | ||
| Theorem | modval 13911 | 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 13912 | The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) = (𝐴 − ((⌊‘(𝐴 / 𝐵)) · 𝐵))) | ||
| Theorem | modcl 13913 | Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ ℝ) | ||
| Theorem | flpmodeq 13914 | Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((⌊‘(𝐴 / 𝐵)) · 𝐵) + (𝐴 mod 𝐵)) = 𝐴) | ||
| Theorem | modcld 13915 | Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℝ) | ||
| Theorem | mod0 13916 | 𝐴 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 13917 | 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 13918 | 𝐴 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 13919 | The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝐵)) | ||
| Theorem | modlt 13920 | The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) < 𝐵) | ||
| Theorem | modelico 13921 | Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 mod 𝐵) ∈ (0[,)𝐵)) | ||
| Theorem | moddiffl 13922 | 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 13923 | The modulo operation differs from 𝐴 by an integer multiple of 𝐵. (Contributed by Mario Carneiro, 15-Jul-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 − (𝐴 mod 𝐵)) / 𝐵) ∈ ℤ) | ||
| Theorem | modfrac 13924 | The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 mod 1) = (𝐴 − (⌊‘𝐴))) | ||
| Theorem | flmod 13925 | The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.) |
| ⊢ (𝐴 ∈ ℝ → (⌊‘𝐴) = (𝐴 − (𝐴 mod 1))) | ||
| Theorem | intfrac 13926 | Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 = ((⌊‘𝐴) + (𝐴 mod 1))) | ||
| Theorem | zmod10 13927 | An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ (𝑁 ∈ ℤ → (𝑁 mod 1) = 0) | ||
| Theorem | zmod1congr 13928 | 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 13929 | 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 13930 | 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 13931 | Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ ℕ0) | ||
| Theorem | zmodcld 13932 | Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 mod 𝐵) ∈ ℕ0) | ||
| Theorem | zmodfz 13933 | An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...(𝐵 − 1))) | ||
| Theorem | zmodfzo 13934 | An integer mod 𝐵 lies in the first 𝐵 nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0..^𝐵)) | ||
| Theorem | zmodfzp1 13935 | An integer mod 𝐵 lies in the first 𝐵 + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 mod 𝐵) ∈ (0...𝐵)) | ||
| Theorem | modid 13936 | Identity law for modulo. (Contributed by NM, 29-Dec-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴) | ||
| Theorem | modid0 13937 | A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.) |
| ⊢ (𝑁 ∈ ℝ+ → (𝑁 mod 𝑁) = 0) | ||
| Theorem | modid2 13938 | Identity law for modulo. (Contributed by NM, 29-Dec-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 𝐴 ↔ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵))) | ||
| Theorem | zmodid2 13939 | Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0...(𝑁 − 1)))) | ||
| Theorem | zmodidfzo 13940 | Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) = 𝑀 ↔ 𝑀 ∈ (0..^𝑁))) | ||
| Theorem | zmodidfzoimp 13941 | Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.) |
| ⊢ (𝑀 ∈ (0..^𝑁) → (𝑀 mod 𝑁) = 𝑀) | ||
| Theorem | 0mod 13942 | Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014.) |
| ⊢ (𝑁 ∈ ℝ+ → (0 mod 𝑁) = 0) | ||
| Theorem | 1mod 13943 | 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 13944 | Absorption law for modulo. (Contributed by NM, 29-Dec-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) ∧ 𝐵 ≤ 𝐶) → ((𝐴 mod 𝐵) mod 𝐶) = (𝐴 mod 𝐵)) | ||
| Theorem | modabs2 13945 | Absorption law for modulo. (Contributed by NM, 29-Dec-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) mod 𝐵) = (𝐴 mod 𝐵)) | ||
| Theorem | modcyc 13946 | The modulo operation is periodic. (Contributed by NM, 10-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵)) | ||
| Theorem | modcyc2 13947 | The modulo operation is periodic. (Contributed by NM, 12-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → ((𝐴 − (𝐵 · 𝑁)) mod 𝐵) = (𝐴 mod 𝐵)) | ||
| Theorem | modadd1 13948 | Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴 + 𝐶) mod 𝐷) = ((𝐵 + 𝐶) mod 𝐷)) | ||
| Theorem | modaddabs 13949 | Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (((𝐴 mod 𝐶) + (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 + 𝐵) mod 𝐶)) | ||
| Theorem | modaddmod 13950 | 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 13951 | 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 13952 | 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 | muladdmod 13953 | A real number is the sum of the number and a multiple of a positive real number modulo the positive real number. (Contributed by AV, 7-Sep-2025.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (((𝑁 · 𝑀) + 𝐴) mod 𝑀) = (𝐴 mod 𝑀)) | ||
| Theorem | modmuladd 13954* | Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (0[,)𝑀) ∧ 𝑀 ∈ ℝ+) → ((𝐴 mod 𝑀) = 𝐵 ↔ ∃𝑘 ∈ ℤ 𝐴 = ((𝑘 · 𝑀) + 𝐵))) | ||
| Theorem | modmuladdim 13955* | 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 13956* | 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 13957 | 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 13958 | Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.) |
| ⊢ (𝑀 ∈ ℕ → (-1 mod 𝑀) = (𝑀 − 1)) | ||
| Theorem | m1modge3gt1 13959 | Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.) |
| ⊢ (𝑀 ∈ (ℤ≥‘3) → 1 < (-1 mod 𝑀)) | ||
| Theorem | addmodid 13960 | 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 13961 | 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 13962 | 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 13963 | 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 13964 | 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 13965 | 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 13966 | 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 13967 | Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐶) = (𝐵 mod 𝐶)) ⇒ ⊢ (𝜑 → (-𝐴 mod 𝐶) = (-𝐵 mod 𝐶)) | ||
| Theorem | modadd12d 13968 | Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) mod 𝐸) = ((𝐵 + 𝐷) mod 𝐸)) | ||
| Theorem | modsub12d 13969 | Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 mod 𝐸) = (𝐵 mod 𝐸)) & ⊢ (𝜑 → (𝐶 mod 𝐸) = (𝐷 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐶) mod 𝐸) = ((𝐵 − 𝐷) mod 𝐸)) | ||
| Theorem | modsubmod 13970 | 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 13971 | 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 13972 | 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 13973 | 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 13974 | 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 13975 | 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 13976 | 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 13977 | 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 13978 | 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 13979 | 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 13980 | Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → (𝐴 · (𝐵 mod 𝐶)) = ((𝐴 · 𝐵) mod (𝐴 · 𝐶))) | ||
| Theorem | modsubdir 13981 | Distribute the modulo operation over a subtraction. (Contributed by NM, 30-Dec-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+) → ((𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)))) | ||
| Theorem | modeqmodmin 13982 | 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 13983 | A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐴 / 𝐵) ∈ (ℝ ∖ ℚ)) → (𝐴 mod 𝐵) ≠ 0) | ||
| Theorem | modfzo0difsn 13984* | 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.) |
| ⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ ((0..^𝑁) ∖ {𝐽})) → ∃𝑖 ∈ (1..^𝑁)𝐾 = ((𝑖 + 𝐽) mod 𝑁)) | ||
| Theorem | modsumfzodifsn 13985 | 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.) |
| ⊢ ((𝐽 ∈ (0..^𝑁) ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐾 + 𝐽) mod 𝑁) ∈ ((0..^𝑁) ∖ {𝐽})) | ||
| Theorem | modlteq 13986 | Two nonnegative integers less than the modulus are equal iff they are equal modulo the modulus. (Contributed by AV, 14-Mar-2021.) |
| ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐼 mod 𝑁) = (𝐽 mod 𝑁) ↔ 𝐼 = 𝐽)) | ||
| Theorem | addmodlteq 13987 | Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. A much shorter proof exists if the "divides" relation ∥ can be used, see addmodlteqALT 16362. (Contributed by AV, 20-Mar-2021.) |
| ⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽)) | ||
| Theorem | om2uz0i 13988* | The mapping 𝐺 is a one-to-one mapping from ω onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number 𝐶 (normally 0 for the upper integers ℕ0 or 1 for the upper integers ℕ), 1 maps to 𝐶 + 1, etc. This theorem shows the value of 𝐺 at ordinal natural number zero. (This series of theorems generalizes an earlier series for ℕ0 contributed by Raph Levien, 10-Apr-2004.) (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ (𝐺‘∅) = 𝐶 | ||
| Theorem | om2uzsuci 13989* | The value of 𝐺 (see om2uz0i 13988) at a successor. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) + 1)) | ||
| Theorem | om2uzuzi 13990* | The value 𝐺 (see om2uz0i 13988) at an ordinal natural number is in the upper integers. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ (𝐴 ∈ ω → (𝐺‘𝐴) ∈ (ℤ≥‘𝐶)) | ||
| Theorem | om2uzlti 13991* | Less-than relation for 𝐺 (see om2uz0i 13988). (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) < (𝐺‘𝐵))) | ||
| Theorem | om2uzlt2i 13992* | The mapping 𝐺 (see om2uz0i 13988) preserves order. (Contributed by NM, 4-May-2005.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) < (𝐺‘𝐵))) | ||
| Theorem | om2uzrani 13993* | Range of 𝐺 (see om2uz0i 13988). (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ ran 𝐺 = (ℤ≥‘𝐶) | ||
| Theorem | om2uzf1oi 13994* | 𝐺 (see om2uz0i 13988) is a one-to-one onto mapping. (Contributed by NM, 3-Oct-2004.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ 𝐺:ω–1-1-onto→(ℤ≥‘𝐶) | ||
| Theorem | om2uzisoi 13995* | 𝐺 (see om2uz0i 13988) is an isomorphism from natural ordinals to upper integers. (Contributed by NM, 9-Oct-2008.) (Revised by Mario Carneiro, 13-Sep-2013.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ 𝐺 Isom E , < (ω, (ℤ≥‘𝐶)) | ||
| Theorem | om2uzoi 13996* | An alternative definition of 𝐺 in terms of df-oi 9550. (Contributed by Mario Carneiro, 2-Jun-2015.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) ⇒ ⊢ 𝐺 = OrdIso( < , (ℤ≥‘𝐶)) | ||
| Theorem | om2uzrdg 13997* | A helper lemma for the value of a recursive definition generator on upper integers (typically either ℕ or ℕ0) with characteristic function 𝐹(𝑥, 𝑦) and initial value 𝐴. Normally 𝐹 is a function on the partition, and 𝐴 is a member of the partition. See also comment in om2uz0i 13988. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) ⇒ ⊢ (𝐵 ∈ ω → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) | ||
| Theorem | uzrdglem 13998* | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) ⇒ ⊢ (𝐵 ∈ (ℤ≥‘𝐶) → 〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ ran 𝑅) | ||
| Theorem | uzrdgfni 13999* | The recursive definition generator on upper integers is a function. See comment in om2uzrdg 13997. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 4-May-2015.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) & ⊢ 𝑆 = ran 𝑅 ⇒ ⊢ 𝑆 Fn (ℤ≥‘𝐶) | ||
| Theorem | uzrdg0i 14000* | Initial value of a recursive definition generator on upper integers. See comment in om2uzrdg 13997. (Contributed by Mario Carneiro, 26-Jun-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
| ⊢ 𝐶 ∈ ℤ & ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 𝐶) ↾ ω) & ⊢ 𝐴 ∈ V & ⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω) & ⊢ 𝑆 = ran 𝑅 ⇒ ⊢ (𝑆‘𝐶) = 𝐴 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |