![]() |
Metamath
Proof Explorer Theorem List (p. 139 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fldiv4lem1div2uz2 13801 | The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021.) (Proof shortened by AV, 9-Jul-2022.) |
โข (๐ โ (โคโฅโ2) โ (โโ(๐ / 4)) โค ((๐ โ 1) / 2)) | ||
Theorem | fldiv4lem1div2 13802 | The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021.) |
โข (๐ โ โ โ (โโ(๐ / 4)) โค ((๐ โ 1) / 2)) | ||
Theorem | ceilval 13803 | The value of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) |
โข (๐ด โ โ โ (โโ๐ด) = -(โโ-๐ด)) | ||
Theorem | dfceil2 13804* | Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.) |
โข โ = (๐ฅ โ โ โฆ (โฉ๐ฆ โ โค (๐ฅ โค ๐ฆ โง ๐ฆ < (๐ฅ + 1)))) | ||
Theorem | ceilval2 13805* | The value of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018.) |
โข (๐ด โ โ โ (โโ๐ด) = (โฉ๐ฆ โ โค (๐ด โค ๐ฆ โง ๐ฆ < (๐ด + 1)))) | ||
Theorem | ceicl 13806 | The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007.) |
โข (๐ด โ โ โ -(โโ-๐ด) โ โค) | ||
Theorem | ceilcl 13807 | Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015.) |
โข (๐ด โ โ โ (โโ๐ด) โ โค) | ||
Theorem | ceilcld 13808 | Closure of the ceiling function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (โโ๐ด) โ โค) | ||
Theorem | ceige 13809 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jeff Hankins, 10-Jun-2007.) |
โข (๐ด โ โ โ ๐ด โค -(โโ-๐ด)) | ||
Theorem | ceilge 13810 | The ceiling of a real number is greater than or equal to that number. (Contributed by AV, 30-Nov-2018.) |
โข (๐ด โ โ โ ๐ด โค (โโ๐ด)) | ||
Theorem | ceilged 13811 | The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โค (โโ๐ด)) | ||
Theorem | ceim1l 13812 | 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 13813 | One less than the ceiling of a real number is strictly less than that number. (Contributed by AV, 30-Nov-2018.) |
โข (๐ด โ โ โ ((โโ๐ด) โ 1) < ๐ด) | ||
Theorem | ceile 13814 | 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 13815 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by AV, 30-Nov-2018.) |
โข ((๐ด โ โ โง ๐ต โ โค โง ๐ด โค ๐ต) โ (โโ๐ด) โค ๐ต) | ||
Theorem | ceilid 13816 | An integer is its own ceiling. (Contributed by AV, 30-Nov-2018.) |
โข (๐ด โ โค โ (โโ๐ด) = ๐ด) | ||
Theorem | ceilidz 13817 | A real number equals its ceiling iff it is an integer. (Contributed by AV, 30-Nov-2018.) |
โข (๐ด โ โ โ (๐ด โ โค โ (โโ๐ด) = ๐ด)) | ||
Theorem | flleceil 13818 | The floor of a real number is less than or equal to its ceiling. (Contributed by AV, 30-Nov-2018.) |
โข (๐ด โ โ โ (โโ๐ด) โค (โโ๐ด)) | ||
Theorem | fleqceilz 13819 | A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018.) |
โข (๐ด โ โ โ (๐ด โ โค โ (โโ๐ด) = (โโ๐ด))) | ||
Theorem | quoremz 13820 | 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 16346. (Contributed by NM, 14-Aug-2008.) |
โข ๐ = (โโ(๐ด / ๐ต)) & โข ๐ = (๐ด โ (๐ต ยท ๐)) โ โข ((๐ด โ โค โง ๐ต โ โ) โ ((๐ โ โค โง ๐ โ โ0) โง (๐ < ๐ต โง ๐ด = ((๐ต ยท ๐) + ๐ )))) | ||
Theorem | quoremnn0 13821 | Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008.) |
โข ๐ = (โโ(๐ด / ๐ต)) & โข ๐ = (๐ด โ (๐ต ยท ๐)) โ โข ((๐ด โ โ0 โง ๐ต โ โ) โ ((๐ โ โ0 โง ๐ โ โ0) โง (๐ < ๐ต โง ๐ด = ((๐ต ยท ๐) + ๐ )))) | ||
Theorem | quoremnn0ALT 13822 | Alternate proof of quoremnn0 13821 not using quoremz 13820. TODO - Keep either quoremnn0ALT 13822 (if we don't keep quoremz 13820) or quoremnn0 13821? (Contributed by NM, 14-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (โโ(๐ด / ๐ต)) & โข ๐ = (๐ด โ (๐ต ยท ๐)) โ โข ((๐ด โ โ0 โง ๐ต โ โ) โ ((๐ โ โ0 โง ๐ โ โ0) โง (๐ < ๐ต โง ๐ด = ((๐ต ยท ๐) + ๐ )))) | ||
Theorem | intfrac2 13823 | Decompose a real into integer and fractional parts. TODO - should we replace this with intfrac 13851? (Contributed by NM, 16-Aug-2008.) |
โข ๐ = (โโ๐ด) & โข ๐น = (๐ด โ ๐) โ โข (๐ด โ โ โ (0 โค ๐น โง ๐น < 1 โง ๐ด = (๐ + ๐น))) | ||
Theorem | intfracq 13824 | Decompose a rational number, expressed as a ratio, into integer and fractional parts. The fractional part has a tighter bound than that of intfrac2 13823. (Contributed by NM, 16-Aug-2008.) |
โข ๐ = (โโ(๐ / ๐)) & โข ๐น = ((๐ / ๐) โ ๐) โ โข ((๐ โ โค โง ๐ โ โ) โ (0 โค ๐น โง ๐น โค ((๐ โ 1) / ๐) โง (๐ / ๐) = (๐ + ๐น))) | ||
Theorem | fldiv 13825 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by NM, 16-Aug-2008.) |
โข ((๐ด โ โ โง ๐ โ โ) โ (โโ((โโ๐ด) / ๐)) = (โโ(๐ด / ๐))) | ||
Theorem | fldiv2 13826 | 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 13827 | Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016.) |
โข (๐ โ โ โ (๐พ โ (1...(โโ๐)) โ (๐พ โ โ โง ๐พ โค ๐))) | ||
Theorem | uzsup 13828 | An upper set of integers is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ sup(๐, โ*, < ) = +โ) | ||
Theorem | ioopnfsup 13829 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
โข ((๐ด โ โ* โง ๐ด โ +โ) โ sup((๐ด(,)+โ), โ*, < ) = +โ) | ||
Theorem | icopnfsup 13830 | An upper set of reals is unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
โข ((๐ด โ โ* โง ๐ด โ +โ) โ sup((๐ด[,)+โ), โ*, < ) = +โ) | ||
Theorem | rpsup 13831 | The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
โข sup(โ+, โ*, < ) = +โ | ||
Theorem | resup 13832 | The real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
โข sup(โ, โ*, < ) = +โ | ||
Theorem | xrsup 13833 | The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016.) |
โข sup(โ*, โ*, < ) = +โ | ||
Syntax | cmo 13834 | Extend class notation with the modulo operation. |
class mod | ||
Definition | df-mod 13835* | Define the modulo (remainder) operation. See modval 13836 for its value. For example, (5 mod 3) = 2 and (-7 mod 2) = 1 (ex-mod 29702). (Contributed by NM, 10-Nov-2008.) |
โข mod = (๐ฅ โ โ, ๐ฆ โ โ+ โฆ (๐ฅ โ (๐ฆ ยท (โโ(๐ฅ / ๐ฆ))))) | ||
Theorem | modval 13836 | 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 13837 | The value of the modulo operation (multiplication in reversed order). (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด mod ๐ต) = (๐ด โ ((โโ(๐ด / ๐ต)) ยท ๐ต))) | ||
Theorem | modcl 13838 | Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด mod ๐ต) โ โ) | ||
Theorem | flpmodeq 13839 | Partition of a division into its integer part and the remainder. (Contributed by Alexander van der Vekens, 14-Apr-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (((โโ(๐ด / ๐ต)) ยท ๐ต) + (๐ด mod ๐ต)) = ๐ด) | ||
Theorem | modcld 13840 | Closure law for the modulo operation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) โ โข (๐ โ (๐ด mod ๐ต) โ โ) | ||
Theorem | mod0 13841 | ๐ด 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 13842 | 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 13843 | ๐ด 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 13844 | The modulo operation is nonnegative. (Contributed by NM, 10-Nov-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ 0 โค (๐ด mod ๐ต)) | ||
Theorem | modlt 13845 | The modulo operation is less than its second argument. (Contributed by NM, 10-Nov-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด mod ๐ต) < ๐ต) | ||
Theorem | modelico 13846 | Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (๐ด mod ๐ต) โ (0[,)๐ต)) | ||
Theorem | moddiffl 13847 | 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 13848 | The modulo operation differs from ๐ด by an integer multiple of ๐ต. (Contributed by Mario Carneiro, 15-Jul-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ ((๐ด โ (๐ด mod ๐ต)) / ๐ต) โ โค) | ||
Theorem | modfrac 13849 | The fractional part of a number is the number modulo 1. (Contributed by NM, 11-Nov-2008.) |
โข (๐ด โ โ โ (๐ด mod 1) = (๐ด โ (โโ๐ด))) | ||
Theorem | flmod 13850 | The floor function expressed in terms of the modulo operation. (Contributed by NM, 11-Nov-2008.) |
โข (๐ด โ โ โ (โโ๐ด) = (๐ด โ (๐ด mod 1))) | ||
Theorem | intfrac 13851 | Break a number into its integer part and its fractional part. (Contributed by NM, 31-Dec-2008.) |
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (๐ด mod 1))) | ||
Theorem | zmod10 13852 | An integer modulo 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข (๐ โ โค โ (๐ mod 1) = 0) | ||
Theorem | zmod1congr 13853 | 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 13854 | 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 13855 | 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 13856 | Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008.) |
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด mod ๐ต) โ โ0) | ||
Theorem | zmodcld 13857 | Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ด mod ๐ต) โ โ0) | ||
Theorem | zmodfz 13858 | An integer mod ๐ต lies in the first ๐ต nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010.) |
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด mod ๐ต) โ (0...(๐ต โ 1))) | ||
Theorem | zmodfzo 13859 | An integer mod ๐ต lies in the first ๐ต nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด mod ๐ต) โ (0..^๐ต)) | ||
Theorem | zmodfzp1 13860 | An integer mod ๐ต lies in the first ๐ต + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018.) |
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด mod ๐ต) โ (0...๐ต)) | ||
Theorem | modid 13861 | Identity law for modulo. (Contributed by NM, 29-Dec-2008.) |
โข (((๐ด โ โ โง ๐ต โ โ+) โง (0 โค ๐ด โง ๐ด < ๐ต)) โ (๐ด mod ๐ต) = ๐ด) | ||
Theorem | modid0 13862 | A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018.) |
โข (๐ โ โ+ โ (๐ mod ๐) = 0) | ||
Theorem | modid2 13863 | Identity law for modulo. (Contributed by NM, 29-Dec-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ ((๐ด mod ๐ต) = ๐ด โ (0 โค ๐ด โง ๐ด < ๐ต))) | ||
Theorem | zmodid2 13864 | Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ mod ๐) = ๐ โ ๐ โ (0...(๐ โ 1)))) | ||
Theorem | zmodidfzo 13865 | Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.) |
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ mod ๐) = ๐ โ ๐ โ (0..^๐))) | ||
Theorem | zmodidfzoimp 13866 | Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018.) |
โข (๐ โ (0..^๐) โ (๐ mod ๐) = ๐) | ||
Theorem | 0mod 13867 | Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014.) |
โข (๐ โ โ+ โ (0 mod ๐) = 0) | ||
Theorem | 1mod 13868 | 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 13869 | Absorption law for modulo. (Contributed by NM, 29-Dec-2008.) |
โข (((๐ด โ โ โง ๐ต โ โ+ โง ๐ถ โ โ+) โง ๐ต โค ๐ถ) โ ((๐ด mod ๐ต) mod ๐ถ) = (๐ด mod ๐ต)) | ||
Theorem | modabs2 13870 | Absorption law for modulo. (Contributed by NM, 29-Dec-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ ((๐ด mod ๐ต) mod ๐ต) = (๐ด mod ๐ต)) | ||
Theorem | modcyc 13871 | The modulo operation is periodic. (Contributed by NM, 10-Nov-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+ โง ๐ โ โค) โ ((๐ด + (๐ ยท ๐ต)) mod ๐ต) = (๐ด mod ๐ต)) | ||
Theorem | modcyc2 13872 | The modulo operation is periodic. (Contributed by NM, 12-Nov-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ+ โง ๐ โ โค) โ ((๐ด โ (๐ต ยท ๐)) mod ๐ต) = (๐ด mod ๐ต)) | ||
Theorem | modadd1 13873 | Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008.) |
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ+) โง (๐ด mod ๐ท) = (๐ต mod ๐ท)) โ ((๐ด + ๐ถ) mod ๐ท) = ((๐ต + ๐ถ) mod ๐ท)) | ||
Theorem | modaddabs 13874 | Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ+) โ (((๐ด mod ๐ถ) + (๐ต mod ๐ถ)) mod ๐ถ) = ((๐ด + ๐ต) mod ๐ถ)) | ||
Theorem | modaddmod 13875 | 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 13876 | 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 13877 | 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 13878* | Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต โ (0[,)๐) โง ๐ โ โ+) โ ((๐ด mod ๐) = ๐ต โ โ๐ โ โค ๐ด = ((๐ ยท ๐) + ๐ต))) | ||
Theorem | modmuladdim 13879* | 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 13880* | 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 13881 | 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 13882 | Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.) |
โข (๐ โ โ โ (-1 mod ๐) = (๐ โ 1)) | ||
Theorem | m1modge3gt1 13883 | Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.) |
โข (๐ โ (โคโฅโ3) โ 1 < (-1 mod ๐)) | ||
Theorem | addmodid 13884 | 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 13885 | 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 13886 | 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 13887 | 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 13888 | 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 13889 | 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 13890 | 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 13891 | Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด mod ๐ถ) = (๐ต mod ๐ถ)) โ โข (๐ โ (-๐ด mod ๐ถ) = (-๐ต mod ๐ถ)) | ||
Theorem | modadd12d 13892 | Additive property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ธ โ โ+) & โข (๐ โ (๐ด mod ๐ธ) = (๐ต mod ๐ธ)) & โข (๐ โ (๐ถ mod ๐ธ) = (๐ท mod ๐ธ)) โ โข (๐ โ ((๐ด + ๐ถ) mod ๐ธ) = ((๐ต + ๐ท) mod ๐ธ)) | ||
Theorem | modsub12d 13893 | Subtraction property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ) & โข (๐ โ ๐ธ โ โ+) & โข (๐ โ (๐ด mod ๐ธ) = (๐ต mod ๐ธ)) & โข (๐ โ (๐ถ mod ๐ธ) = (๐ท mod ๐ธ)) โ โข (๐ โ ((๐ด โ ๐ถ) mod ๐ธ) = ((๐ต โ ๐ท) mod ๐ธ)) | ||
Theorem | modsubmod 13894 | 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 13895 | 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 13896 | 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 13897 | 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 13898 | 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 13899 | 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 13900 | 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 ๐))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |