Home Metamath Proof ExplorerTheorem List (p. 130 of 330) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-22459) Hilbert Space Explorer (22460-23982) Users' Mathboxes (23983-32936)

Theorem List for Metamath Proof Explorer - 12901-13000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremiddvds 12901 An integer divides itself. (Contributed by Paul Chapman, 21-Mar-2011.)

Theorem1dvds 12902 1 divides any integer. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvds0 12903 Any integer divides 0. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremnegdvdsb 12904 An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsnegb 12905 An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremabsdvdsb 12906 An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsabsb 12907 An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)

Theorem0dvds 12908 Only 0 is divisible by 0 . (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsmul1 12909 An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsmul2 12910 An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremiddvdsexp 12911 An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.)

Theoremmuldvds1 12912 If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremmuldvds2 12913 If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdscmul 12914 Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsmulc 12915 Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdscmulr 12916 Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsmulcr 12917 Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvds2ln 12918 If an integer divides each of two other integers, it divides any linear combination of them. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvds2add 12919 If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvds2sub 12920 If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdstr 12921 The divides relation is transitive. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsmultr1 12922 If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)

Theoremdvdsmultr2 12923 If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)

Theoremordvdsmul 12924 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.)

Theoremdvdssub2 12925 If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014.)

Theoremdvdsadd 12926 An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 13-Jul-2014.)

Theoremdvdsaddr 12927 An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremdvdssub 12928 An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremdvdssubr 12929 An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremdvdsadd2b 12930 Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)

Theoremfsumdvds 12931* If every term in a sum is divisible by , then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.)

Theoremdvdslelem 12932 Lemma for dvdsle 12933. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsle 12933 The divisors of a positive integer are bounded by it. The proof does not use . (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsleabs 12934 The divisors of a nonzero integer are bounded by its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.)

Theoremdvdseq 12935 If two integers divide each other, they must be equal, up to a difference in sign. (Contributed by Mario Carneiro, 30-May-2014.)

Theoremdvds1 12936 The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.)

Theoremalzdvds 12937* Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdvdsext 12938* Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.)

Theoremfzm1ndvds 12939 No number between and divides . (Contributed by Mario Carneiro, 24-Jan-2015.)

Theoremfzo0dvdseq 12940 Zero is the only one of the first nonnegative integers that is divisible by . (Contributed by Stefan O'Rear, 6-Sep-2015.)
..^

Theoremfzocongeq 12941 Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.)
..^ ..^

Theoremdvdsfac 12942 A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.)

Theoremdvdsexp 12943 A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.)

Theoremdvdsmod 12944 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.)

Theoremodd2np1lem 12945* Lemma for odd2np1 12946. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

Theoremodd2np1 12946* 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.)

Theoremoddm1even 12947 An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)

Theoremoddp1even 12948 An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)

Theoremoexpneg 12949 The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.)

Theorem3dvds 12950* A rule for divisibility by 3 of a number written in base 10. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.)

6.1.4  The division algorithm

Theoremdivalglem0 12951 Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem1 12952 Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem2 12953* Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem4 12954* Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem5 12955* Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem6 12956 Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem7 12957 Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem8 12958* Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem9 12959* Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalglem10 12960* Lemma for divalg 12961. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalg 12961* The division algorithm (theorem). Dividing an integer by a nonzero integer produces a (unique) quotient and a unique remainder . The proof does not use , or . (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalgb 12962* Express the division algorithm as stated in divalg 12961 in terms of . (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremdivalg2 12963* The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.)

Theoremdivalgmod 12964* The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor (compare divalg2 12963 and divalgb 12962). This demonstration theorem justifies the use of to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremndvdssub 12965 Corollary of the division algorithm. If an integer greater than divides , then it does not divide any of , ... . (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremndvdsadd 12966 Corollary of the division algorithm. If an integer greater than divides , then it does not divide any of , ... . (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremndvdsp1 12967 Special case of ndvdsadd 12966. If an integer greater than divides , it does not divide . (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremndvdsi 12968 A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.)

6.1.5  Bit sequences

Syntaxcbits 12969 Define the binary bits of an integer.
bits

Syntaxcsmu 12971 Define the sequence multiplication on bit sequences.
smul

Definitiondf-bits 12972* Define the binary bits of an integer. The expression bits means that the -th bit of is 1 (and its negation means the bit is 0). (Contributed by Mario Carneiro, 4-Sep-2016.)
bits

Theorembitsfval 12973* Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsval 12974 Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsval2 12975 Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsss 12976 The set of bits of an integer is a subset of . (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsf 12977 The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembits0 12978 Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembits0e 12979 The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembits0o 12980 The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsp1 12981 The -th bit of is the -th bit of . (Contributed by Mario Carneiro, 5-Sep-2016.)
bits bits

Theorembitsp1e 12982 The -th bit of is the -th bit of . (Contributed by Mario Carneiro, 5-Sep-2016.)
bits bits

Theorembitsp1o 12983 The -th bit of is the -th bit of . (Contributed by Mario Carneiro, 5-Sep-2016.)
bits bits

Theorembitsfzolem 12984* Lemma for bitsfzo 12985. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits ..^              ..^

Theorembitsfzo 12985 The bits of a number are all less than iff the number is nonnegative and less than . (Contributed by Mario Carneiro, 5-Sep-2016.)
..^ bits ..^

Theorembitsmod 12986 Truncating the bit sequence after some is equivalent to reducing the argument . (Contributed by Mario Carneiro, 6-Sep-2016.)
bits bits ..^

Theorembitsfi 12987 Every number is associated to a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitscmp 12988 The bit complement of is . (Thus, by bitsfi 12987, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.)
bits bits

Theorem0bits 12989 The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.)
bits

Theoremm1bits 12990 The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsinv1lem 12991 Lemma for bitsinv1 12992. (Contributed by Mario Carneiro, 22-Sep-2016.)
bits

Theorembitsinv1 12992* There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 12988), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.)
bits

Theorembitsinv2 12993* There is an explicit inverse to the bits function for nonnegative integers, part 2. (Contributed by Mario Carneiro, 8-Sep-2016.)
bits

Theorembitsf1ocnv 12994* The bits function restricted to nonnegative integers is a bijection from the integers to the finite sets of integers. It is in fact the inverse of the Ackermann bijection ackbijnn 12645. (Contributed by Mario Carneiro, 8-Sep-2016.)
bits bits

Theorembitsf1o 12995 The bits function restricted to nonnegative integers is a bijection from the integers to the finite sets of integers. It is in fact the inverse of the Ackermann bijection ackbijnn 12645. (Contributed by Mario Carneiro, 8-Sep-2016.)
bits

Theorembitsf1 12996 The bits function is an injection from to . It is obviously not a bijection (by Cantor's theorem canth2 7296), and in fact its range is the set of finite and cofinite subsets of . (Contributed by Mario Carneiro, 22-Sep-2016.)
bits

Theorem2ebits 12997 The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016.)
bits

Theorembitsinv 12998* The inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.)
bits

Theorembitsinvp1 12999 Recursive definition of the inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016.)
bits        ..^ ..^

Theoremsadadd2lem2 13000 The core of the proof of sadadd2 13010. The intuitive justification for this is that cadd is true if at least two arguments are true, and hadd is true if an odd number of arguments are true, so altogether the result is where is the number of true arguments, which is equivalently obtained by adding together one for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016.)