Home | Intuitionistic Logic Explorer Theorem List (p. 116 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvdsdc 11501 | Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.) |
DECID | ||
Theorem | moddvds 11502 | Two ways to say (mod ), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | dvds0lem 11503 | A lemma to assist theorems of with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds1lem 11504* | A lemma to assist theorems of with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2lem 11505* | A lemma to assist theorems of with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | iddvds 11506 | 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 11507 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds0 11508 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | negdvdsb 11509 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsnegb 11510 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | absdvdsb 11511 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsabsb 11512 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | 0dvds 11513 | Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | zdvdsdc 11514 | Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.) |
DECID | ||
Theorem | dvdsmul1 11515 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsmul2 11516 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | iddvdsexp 11517 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | muldvds1 11518 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | muldvds2 11519 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdscmul 11520 | 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 11521 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdscmulr 11522 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsmulcr 11523 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | summodnegmod 11524 | 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.) |
Theorem | modmulconst 11525 | Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.) |
Theorem | dvds2ln 11526 | 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 11527 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2sub 11528 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2subd 11529 | Natural deduction form of dvds2sub 11528. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | dvdstr 11530 | 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 | dvdsmultr1 11531 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | dvdsmultr1d 11532 | Natural deduction form of dvdsmultr1 11531. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | dvdsmultr2 11533 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | ordvdsmul 11534 | 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 11535 | 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 11536 | 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 11537 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | dvdssub 11538 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | dvdssubr 11539 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | dvdsadd2b 11540 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
Theorem | dvdslelemd 11541 | Lemma for dvdsle 11542. (Contributed by Jim Kingdon, 8-Nov-2021.) |
Theorem | dvdsle 11542 | The divisors of a positive integer are bounded by it. The proof does not use . (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsleabs 11543 | 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.) |
Theorem | dvdsleabs2 11544 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
Theorem | dvdsabseq 11545 | 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.) |
Theorem | dvdseq 11546 | 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.) |
Theorem | divconjdvds 11547 | 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.) |
Theorem | dvdsdivcl 11548* | 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 11549* | An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.) |
Theorem | dvdsssfz1 11550* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
Theorem | dvds1 11551 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
Theorem | alzdvds 11552* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsext 11553* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Theorem | fzm1ndvds 11554 | No number between and divides . (Contributed by Mario Carneiro, 24-Jan-2015.) |
Theorem | fzo0dvdseq 11555 | Zero is the only one of the first nonnegative integers that is divisible by . (Contributed by Stefan O'Rear, 6-Sep-2015.) |
..^ | ||
Theorem | fzocongeq 11556 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
..^ ..^ | ||
Theorem | addmodlteqALT 11557 | 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 10171 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
..^ ..^ | ||
Theorem | dvdsfac 11558 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
Theorem | dvdsexp 11559 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | dvdsmod 11560 | 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 for any base. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Theorem | mulmoddvds 11561 | 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.) |
Theorem | 3dvdsdec 11562 | 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.) |
; | ||
Theorem | 3dvds2dec 11563 | 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.) |
;; | ||
The set of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 11567. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom to say that " is even" (which implies , see evenelz 11564) and to say that " is odd" (under the assumption that ). The previously proven theorems about even and odd numbers, like zneo 9152, zeo 9156, zeo2 9157, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 11586 and oddp1d2 11587. The corresponding theorems are zeneo 11568, zeo3 11565 and zeo4 11567. | ||
Theorem | evenelz 11564 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 11498. (Contributed by AV, 22-Jun-2021.) |
Theorem | zeo3 11565 | An integer is even or odd. (Contributed by AV, 17-Jun-2021.) |
Theorem | zeoxor 11566 | An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.) |
Theorem | zeo4 11567 | An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.) |
Theorem | zeneo 11568 | 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 9152 follows immediately from the fact that a contradiction implies anything, see pm2.21i 635. (Contributed by AV, 22-Jun-2021.) |
Theorem | odd2np1lem 11569* | Lemma for odd2np1 11570. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | odd2np1 11570* | 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.) |
Theorem | even2n 11571* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
Theorem | oddm1even 11572 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
Theorem | oddp1even 11573 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
Theorem | oexpneg 11574 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) |
Theorem | mod2eq0even 11575 | 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.) |
Theorem | mod2eq1n2dvds 11576 | 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.) |
Theorem | oddnn02np1 11577* | A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.) |
Theorem | oddge22np1 11578* | An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) |
Theorem | evennn02n 11579* | A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) |
Theorem | evennn2n 11580* | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
Theorem | 2tp1odd 11581 | A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.) |
Theorem | mulsucdiv2z 11582 | 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.) |
Theorem | sqoddm1div8z 11583 | A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.) |
Theorem | 2teven 11584 | A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.) |
Theorem | zeo5 11585 | An integer is either even or odd, version of zeo3 11565 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020.) |
Theorem | evend2 11586 | An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo 9156 and zeo2 9157. (Contributed by AV, 22-Jun-2021.) |
Theorem | oddp1d2 11587 | An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo 9156 and zeo2 9157. (Contributed by AV, 22-Jun-2021.) |
Theorem | zob 11588 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) |
Theorem | oddm1d2 11589 | An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.) |
Theorem | ltoddhalfle 11590 | An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.) |
Theorem | halfleoddlt 11591 | An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.) |
Theorem | opoe 11592 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | omoe 11593 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | opeo 11594 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | omeo 11595 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | m1expe 11596 | Exponentiation of -1 by an even power. Variant of m1expeven 10340. (Contributed by AV, 25-Jun-2021.) |
Theorem | m1expo 11597 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) |
Theorem | m1exp1 11598 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) |
Theorem | nn0enne 11599 | A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.) |
Theorem | nn0ehalf 11600 | The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |