![]() |
Metamath
Proof Explorer Theorem List (p. 163 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | divides 16201* | Define the divides relation. ๐ โฅ ๐ means ๐ divides into ๐ with no remainder. For example, 3 โฅ 6 (ex-dvds 29747). As proven in dvdsval3 16203, ๐ โฅ ๐ โ (๐ mod ๐) = 0. See divides 16201 and dvdsval2 16202 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ โ๐ โ โค (๐ ยท ๐) = ๐)) | ||
Theorem | dvdsval2 16202 | One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.) |
โข ((๐ โ โค โง ๐ โ 0 โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ / ๐) โ โค)) | ||
Theorem | dvdsval3 16203 | One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.) |
โข ((๐ โ โ โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐ mod ๐) = 0)) | ||
Theorem | dvdszrcl 16204 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข (๐ โฅ ๐ โ (๐ โ โค โง ๐ โ โค)) | ||
Theorem | dvdsmod0 16205 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
โข ((๐ โ โ โง ๐ โฅ ๐) โ (๐ mod ๐) = 0) | ||
Theorem | p1modz1 16206 | If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022.) |
โข ((๐ โฅ ๐ด โง 1 < ๐) โ ((๐ด + 1) mod ๐) = 1) | ||
Theorem | dvdsmodexp 16207 | If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl 16719). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.) |
โข ((๐ โ โ โง ๐ต โ โ โง ๐ โฅ ๐ด) โ ((๐ดโ๐ต) mod ๐) = (๐ด mod ๐)) | ||
Theorem | nndivdvds 16208 | Strong form of dvdsval2 16202 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ต โฅ ๐ด โ (๐ด / ๐ต) โ โ)) | ||
Theorem | nndivides 16209* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ โ๐ โ โ (๐ ยท ๐) = ๐)) | ||
Theorem | moddvds 16210 | Two ways to say ๐ดโก๐ต (mod ๐), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ๐ โฅ (๐ด โ ๐ต))) | ||
Theorem | modm1div 16211 | An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.) |
โข ((๐ โ (โคโฅโ2) โง ๐ด โ โค) โ ((๐ด mod ๐) = 1 โ ๐ โฅ (๐ด โ 1))) | ||
Theorem | dvds0lem 16212 | A lemma to assist theorems of โฅ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ ยท ๐) = ๐) โ ๐ โฅ ๐) | ||
Theorem | dvds1lem 16213* | A lemma to assist theorems of โฅ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ (๐ฝ โ โค โง ๐พ โ โค)) & โข (๐ โ (๐ โ โค โง ๐ โ โค)) & โข ((๐ โง ๐ฅ โ โค) โ ๐ โ โค) & โข ((๐ โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐ฝ) = ๐พ โ (๐ ยท ๐) = ๐)) โ โข (๐ โ (๐ฝ โฅ ๐พ โ ๐ โฅ ๐)) | ||
Theorem | dvds2lem 16214* | A lemma to assist theorems of โฅ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ (๐ผ โ โค โง ๐ฝ โ โค)) & โข (๐ โ (๐พ โ โค โง ๐ฟ โ โค)) & โข (๐ โ (๐ โ โค โง ๐ โ โค)) & โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) & โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ) โ (๐ ยท ๐) = ๐)) โ โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ ๐ โฅ ๐)) | ||
Theorem | iddvds 16215 | An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ ๐ โฅ ๐) | ||
Theorem | 1dvds 16216 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ 1 โฅ ๐) | ||
Theorem | dvds0 16217 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ ๐ โฅ 0) | ||
Theorem | negdvdsb 16218 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ -๐ โฅ ๐)) | ||
Theorem | dvdsnegb 16219 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ -๐)) | ||
Theorem | absdvdsb 16220 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (absโ๐) โฅ ๐)) | ||
Theorem | dvdsabsb 16221 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (absโ๐))) | ||
Theorem | 0dvds 16222 | Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ (0 โฅ ๐ โ ๐ = 0)) | ||
Theorem | dvdsmul1 16223 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) | ||
Theorem | dvdsmul2 16224 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) | ||
Theorem | iddvdsexp 16225 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โฅ (๐โ๐)) | ||
Theorem | muldvds1 16226 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โฅ ๐ โ ๐พ โฅ ๐)) | ||
Theorem | muldvds2 16227 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โฅ ๐ โ ๐ โฅ ๐)) | ||
Theorem | dvdscmul 16228 | Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in [ApostolNT] p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐พ ยท ๐) โฅ (๐พ ยท ๐))) | ||
Theorem | dvdsmulc 16229 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) | ||
Theorem | dvdscmulr 16230 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐พ ยท ๐) โฅ (๐พ ยท ๐) โ ๐ โฅ ๐)) | ||
Theorem | dvdsmulcr 16231 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ ยท ๐พ) โฅ (๐ ยท ๐พ) โ ๐ โฅ ๐)) | ||
Theorem | summodnegmod 16232 | The sum of two integers modulo a positive integer equals zero iff the first of the two integers equals the negative of the other integer modulo the positive integer. (Contributed by AV, 25-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ) โ (((๐ด + ๐ต) mod ๐) = 0 โ (๐ด mod ๐) = (-๐ต mod ๐))) | ||
Theorem | modmulconst 16233 | Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ((๐ถ ยท ๐ด) mod (๐ถ ยท ๐)) = ((๐ถ ยท ๐ต) mod (๐ถ ยท ๐)))) | ||
Theorem | dvds2ln 16234 | If an integer divides each of two other integers, it divides any linear combination of them. Theorem 1.1(c) in [ApostolNT] p. 14 (linearity property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (((๐ผ โ โค โง ๐ฝ โ โค) โง (๐พ โ โค โง ๐ โ โค โง ๐ โ โค)) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ ((๐ผ ยท ๐) + (๐ฝ ยท ๐)))) | ||
Theorem | dvds2add 16235 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ + ๐))) | ||
Theorem | dvds2sub 16236 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ โ ๐))) | ||
Theorem | dvds2addd 16237 | Deduction form of dvds2add 16235. (Contributed by SN, 21-Aug-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ + ๐)) | ||
Theorem | dvds2subd 16238 | Deduction form of dvds2sub 16236. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ โ ๐)) | ||
Theorem | dvdstr 16239 | The divides relation is transitive. Theorem 1.1(b) in [ApostolNT] p. 14 (transitive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐ โฅ ๐) โ ๐พ โฅ ๐)) | ||
Theorem | dvdstrd 16240 | The divides relation is transitive, a deduction version of dvdstr 16239. (Contributed by metakunt, 12-May-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) & โข (๐ โ ๐ โฅ ๐) โ โข (๐ โ ๐พ โฅ ๐) | ||
Theorem | dvdsmultr1 16241 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | dvdsmultr1d 16242 | Deduction form of dvdsmultr1 16241. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ ยท ๐)) | ||
Theorem | dvdsmultr2 16243 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | dvdsmultr2d 16244 | Deduction form of dvdsmultr2 16243. (Contributed by SN, 23-Aug-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ ยท ๐)) | ||
Theorem | ordvdsmul 16245 | If an integer divides either of two others, it divides their product. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 17-Jul-2014.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โจ ๐พ โฅ ๐) โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | dvdssub2 16246 | If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014.) |
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง ๐พ โฅ (๐ โ ๐)) โ (๐พ โฅ ๐ โ ๐พ โฅ ๐)) | ||
Theorem | dvdsadd 16247 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 13-Jul-2014.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ + ๐))) | ||
Theorem | dvdsaddr 16248 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ + ๐))) | ||
Theorem | dvdssub 16249 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ โ ๐))) | ||
Theorem | dvdssubr 16250 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ โ ๐))) | ||
Theorem | dvdsadd2b 16251 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค โง (๐ถ โ โค โง ๐ด โฅ ๐ถ)) โ (๐ด โฅ ๐ต โ ๐ด โฅ (๐ถ + ๐ต))) | ||
Theorem | dvdsaddre2b 16252 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 16251 only requiring ๐ต to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต โ โ โง (๐ถ โ โค โง ๐ด โฅ ๐ถ)) โ (๐ด โฅ ๐ต โ ๐ด โฅ (๐ถ + ๐ต))) | ||
Theorem | fsumdvds 16253* | If every term in a sum is divisible by ๐, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โฅ ๐ต) โ โข (๐ โ ๐ โฅ ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | dvdslelem 16254 | Lemma for dvdsle 16255. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ๐ โ โค & โข ๐ โ โ & โข ๐พ โ โค โ โข (๐ < ๐ โ (๐พ ยท ๐) โ ๐) | ||
Theorem | dvdsle 16255 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ โค ๐)) | ||
Theorem | dvdsleabs 16256 | The divisors of a nonzero integer are bounded by its absolute value. Theorem 1.1(i) in [ApostolNT] p. 14 (comparison property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โฅ ๐ โ ๐ โค (absโ๐))) | ||
Theorem | dvdsleabs2 16257 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โฅ ๐ โ (absโ๐) โค (absโ๐))) | ||
Theorem | dvdsabseq 16258 | If two integers divide each other, they must be equal, up to a difference in sign. Theorem 1.1(j) in [ApostolNT] p. 14. (Contributed by Mario Carneiro, 30-May-2014.) (Revised by AV, 7-Aug-2021.) |
โข ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (absโ๐) = (absโ๐)) | ||
Theorem | dvdseq 16259 | If two nonnegative integers divide each other, they must be equal. (Contributed by Mario Carneiro, 30-May-2014.) (Proof shortened by AV, 7-Aug-2021.) |
โข (((๐ โ โ0 โง ๐ โ โ0) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ = ๐) | ||
Theorem | divconjdvds 16260 | If a nonzero integer ๐ divides another integer ๐, the other integer ๐ divided by the nonzero integer ๐ (i.e. the divisor conjugate of ๐ to ๐) divides the other integer ๐. Theorem 1.1(k) in [ApostolNT] p. 14. (Contributed by AV, 7-Aug-2021.) |
โข ((๐ โฅ ๐ โง ๐ โ 0) โ (๐ / ๐) โฅ ๐) | ||
Theorem | dvdsdivcl 16261* | The complement of a divisor of ๐ is also a divisor of ๐. (Contributed by Mario Carneiro, 2-Jul-2015.) (Proof shortened by AV, 9-Aug-2021.) |
โข ((๐ โ โ โง ๐ด โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ / ๐ด) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) | ||
Theorem | dvdsflip 16262* | An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.) |
โข ๐ด = {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} & โข ๐น = (๐ฆ โ ๐ด โฆ (๐ / ๐ฆ)) โ โข (๐ โ โ โ ๐น:๐ดโ1-1-ontoโ๐ด) | ||
Theorem | dvdsssfz1 16263* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ด โ โ โ {๐ โ โ โฃ ๐ โฅ ๐ด} โ (1...๐ด)) | ||
Theorem | dvds1 16264 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
โข (๐ โ โ0 โ (๐ โฅ 1 โ ๐ = 1)) | ||
Theorem | alzdvds 16265* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ (โ๐ฅ โ โค ๐ฅ โฅ ๐ โ ๐ = 0)) | ||
Theorem | dvdsext 16266* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0) โ (๐ด = ๐ต โ โ๐ฅ โ โ0 (๐ด โฅ ๐ฅ โ ๐ต โฅ ๐ฅ))) | ||
Theorem | fzm1ndvds 16267 | No number between 1 and ๐ โ 1 divides ๐. (Contributed by Mario Carneiro, 24-Jan-2015.) |
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐) | ||
Theorem | fzo0dvdseq 16268 | Zero is the only one of the first ๐ด nonnegative integers that is divisible by ๐ด. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข (๐ต โ (0..^๐ด) โ (๐ด โฅ ๐ต โ ๐ต = 0)) | ||
Theorem | fzocongeq 16269 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ด โ (๐ถ..^๐ท) โง ๐ต โ (๐ถ..^๐ท)) โ ((๐ท โ ๐ถ) โฅ (๐ด โ ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | addmodlteqALT 16270 | Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq 13913 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ ๐ผ = ๐ฝ)) | ||
Theorem | dvdsfac 16271 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
โข ((๐พ โ โ โง ๐ โ (โคโฅโ๐พ)) โ ๐พ โฅ (!โ๐)) | ||
Theorem | dvdsexp2im 16272 | If an integer divides another integer, then it also divides any of its powers. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โ) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐โ๐))) | ||
Theorem | dvdsexp 16273 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
โข ((๐ด โ โค โง ๐ โ โ0 โง ๐ โ (โคโฅโ๐)) โ (๐ดโ๐) โฅ (๐ดโ๐)) | ||
Theorem | dvdsmod 16274 | Any number ๐พ whose mod base ๐ is divisible by a divisor ๐ of the base is also divisible by ๐. This means that primes will also be relatively prime to the base when reduced mod ๐ for any base. (Contributed by Mario Carneiro, 13-Mar-2014.) |
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ mod ๐) โ ๐ โฅ ๐พ)) | ||
Theorem | mulmoddvds 16275 | If an integer is divisible by a positive integer, the product of this integer with another integer modulo the positive integer is 0. (Contributed by Alexander van der Vekens, 30-Aug-2018.) (Proof shortened by AV, 18-Mar-2022.) |
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ (๐ โฅ ๐ด โ ((๐ด ยท ๐ต) mod ๐) = 0)) | ||
Theorem | 3dvds 16276* | A rule for divisibility by 3 of a number written in base 10. This is Metamath 100 proof #85. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.) (Revised by AV, 8-Sep-2021.) |
โข ((๐ โ โ0 โง ๐น:(0...๐)โถโค) โ (3 โฅ ฮฃ๐ โ (0...๐)((๐นโ๐) ยท (;10โ๐)) โ 3 โฅ ฮฃ๐ โ (0...๐)(๐นโ๐))) | ||
Theorem | 3dvdsdec 16277 | A decimal number is divisible by three iff the sum of its two "digits" is divisible by three. The term "digits" in its narrow sense is only correct if ๐ด and ๐ต actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers ๐ด and ๐ต, especially if ๐ด is itself a decimal number, e.g., ๐ด = ;๐ถ๐ท. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข (3 โฅ ;๐ด๐ต โ 3 โฅ (๐ด + ๐ต)) | ||
Theorem | 3dvds2dec 16278 | A decimal number is divisible by three iff the sum of its three "digits" is divisible by three. The term "digits" in its narrow sense is only correct if ๐ด, ๐ต and ๐ถ actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers ๐ด, ๐ต and ๐ถ. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 โ โข (3 โฅ ;;๐ด๐ต๐ถ โ 3 โฅ ((๐ด + ๐ต) + ๐ถ)) | ||
Theorem | fprodfvdvdsd 16279* | A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐น:๐ตโถโค) โ โข (๐ โ โ๐ฅ โ ๐ด (๐นโ๐ฅ) โฅ โ๐ โ ๐ด (๐นโ๐)) | ||
Theorem | fproddvdsd 16280* | A finite product of integers is divisible by any of its factors. (Contributed by AV, 14-Aug-2020.) (Proof shortened by AV, 2-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ด โ โค) โ โข (๐ โ โ๐ฅ โ ๐ด ๐ฅ โฅ โ๐ โ ๐ด ๐) | ||
The set โค of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 16283. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom 2 โฅ ๐ to say that "๐ is even" (which implies ๐ โ โค, see evenelz 16281) and ยฌ 2 โฅ ๐ to say that "๐ is odd" (under the assumption that ๐ โ โค). The previously proven theorems about even and odd numbers, like zneo 12647, zeo 12650, zeo2 12651, etc. use different representations, which are equivalent to the representations using the divides relation, see evend2 16302 and oddp1d2 16303. The corresponding theorems are zeneo 16284, zeo3 16282 and zeo4 16283. | ||
Theorem | evenelz 16281 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 16204. (Contributed by AV, 22-Jun-2021.) |
โข (2 โฅ ๐ โ ๐ โ โค) | ||
Theorem | zeo3 16282 | An integer is even or odd. With this representation of even and odd integers, this variant of zeo 12650 follows immediately from the law of excluded middle, see exmidd 894. (Contributed by AV, 17-Jun-2021.) |
โข (๐ โ โค โ (2 โฅ ๐ โจ ยฌ 2 โฅ ๐)) | ||
Theorem | zeo4 16283 | An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12651 follows immediately from the principle of double negation, see notnotb 314. (Contributed by AV, 17-Jun-2021.) |
โข (๐ โ โค โ (2 โฅ ๐ โ ยฌ ยฌ 2 โฅ ๐)) | ||
Theorem | zeneo 16284 | No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. This variant of zneo 12647 follows immediately from the fact that a contradiction implies anything, see pm2.21i 119. (Contributed by AV, 22-Jun-2021.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ ((2 โฅ ๐ด โง ยฌ 2 โฅ ๐ต) โ ๐ด โ ๐ต)) | ||
Theorem | odd2np1lem 16285* | Lemma for odd2np1 16286. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (๐ โ โ0 โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) | ||
Theorem | odd2np1 16286* | An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) | ||
Theorem | even2n 16287* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
โข (2 โฅ ๐ โ โ๐ โ โค (2 ยท ๐) = ๐) | ||
Theorem | oddm1even 16288 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ โ 1))) | ||
Theorem | oddp1even 16289 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ + 1))) | ||
Theorem | oexpneg 16290 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.) |
โข ((๐ด โ โ โง ๐ โ โ โง ยฌ 2 โฅ ๐) โ (-๐ดโ๐) = -(๐ดโ๐)) | ||
Theorem | mod2eq0even 16291 | An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.) |
โข (๐ โ โค โ ((๐ mod 2) = 0 โ 2 โฅ ๐)) | ||
Theorem | mod2eq1n2dvds 16292 | An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see example 3 in [ApostolNT] p. 107. (Contributed by AV, 24-May-2020.) (Proof shortened by AV, 5-Jul-2020.) |
โข (๐ โ โค โ ((๐ mod 2) = 1 โ ยฌ 2 โฅ ๐)) | ||
Theorem | oddnn02np1 16293* | A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.) |
โข (๐ โ โ0 โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ0 ((2 ยท ๐) + 1) = ๐)) | ||
Theorem | oddge22np1 16294* | An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 9-Jul-2022.) |
โข (๐ โ (โคโฅโ2) โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ ((2 ยท ๐) + 1) = ๐)) | ||
Theorem | evennn02n 16295* | A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) (Proof shortened by AV, 10-Jul-2022.) |
โข (๐ โ โ0 โ (2 โฅ ๐ โ โ๐ โ โ0 (2 ยท ๐) = ๐)) | ||
Theorem | evennn2n 16296* | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
โข (๐ โ โ โ (2 โฅ ๐ โ โ๐ โ โ (2 ยท ๐) = ๐)) | ||
Theorem | 2tp1odd 16297 | A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต = ((2 ยท ๐ด) + 1)) โ ยฌ 2 โฅ ๐ต) | ||
Theorem | mulsucdiv2z 16298 | An integer multiplied with its successor divided by 2 yields an integer, i.e. an integer multiplied with its successor is even. (Contributed by AV, 19-Jul-2021.) |
โข (๐ โ โค โ ((๐ ยท (๐ + 1)) / 2) โ โค) | ||
Theorem | sqoddm1div8z 16299 | A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ (((๐โ2) โ 1) / 8) โ โค) | ||
Theorem | 2teven 16300 | A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต = (2 ยท ๐ด)) โ 2 โฅ ๐ต) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |