Home | Intuitionistic Logic Explorer Theorem List (p. 121 of 139) | < 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 | neglcm 12001 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm lcm | ||
Theorem | lcmabs 12002 | The lcm of two integers is the same as that of their absolute values. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm lcm | ||
Theorem | lcmgcdlem 12003 | Lemma for lcmgcd 12004 and lcmdvds 12005. Prove them for positive , , and . (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
lcm lcm | ||
Theorem | lcmgcd 12004 |
The product of two numbers' least common multiple and greatest common
divisor is the absolute value of the product of the two numbers. In
particular, that absolute value is the least common multiple of two
coprime numbers, for which .
Multiple methods exist for proving this, and it is often proven either as a consequence of the fundamental theorem of arithmetic or of Bézout's identity bezout 11938; see, e.g., https://proofwiki.org/wiki/Product_of_GCD_and_LCM 11938 and https://math.stackexchange.com/a/470827 11938. This proof uses the latter to first confirm it for positive integers and (the "Second Proof" in the above Stack Exchange page), then shows that implies it for all nonzero integer inputs, then finally uses lcm0val 11991 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcmdvds 12005 | The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcmid 12006 | The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcm1 12007 | The lcm of an integer and 1 is the absolute value of the integer. (Contributed by AV, 23-Aug-2020.) |
lcm | ||
Theorem | lcmgcdnn 12008 | The product of two positive integers' least common multiple and greatest common divisor is the product of the two integers. (Contributed by AV, 27-Aug-2020.) |
lcm | ||
Theorem | lcmgcdeq 12009 | Two integers' absolute values are equal iff their least common multiple and greatest common divisor are equal. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcmdvdsb 12010 | Biconditional form of lcmdvds 12005. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcmass 12011 | Associative law for lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
lcm lcm lcm lcm | ||
Theorem | 3lcm2e6woprm 12012 | The least common multiple of three and two is six. This proof does not use the property of 2 and 3 being prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 27-Aug-2020.) |
lcm | ||
Theorem | 6lcm4e12 12013 | The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020.) |
lcm ; | ||
According to Wikipedia "Coprime integers", see https://en.wikipedia.org/wiki/Coprime_integers (16-Aug-2020) "[...] two integers a and b are said to be relatively prime, mutually prime, or coprime [...] if the only positive integer (factor) that divides both of them is 1. Consequently, any prime number that divides one does not divide the other. This is equivalent to their greatest common divisor (gcd) being 1.". In the following, we use this equivalent characterization to say that and are coprime (or relatively prime) if . The equivalence of the definitions is shown by coprmgcdb 12014. The negation, i.e. two integers are not coprime, can be expressed either by , see ncoprmgcdne1b 12015, or equivalently by , see ncoprmgcdgt1b 12016. A proof of Euclid's lemma based on coprimality is provided in coprmdvds 12018 (as opposed to Euclid's lemma for primes). | ||
Theorem | coprmgcdb 12014* | Two positive integers are coprime, i.e. the only positive integer that divides both of them is 1, iff their greatest common divisor is 1. (Contributed by AV, 9-Aug-2020.) |
Theorem | ncoprmgcdne1b 12015* | Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is not 1. (Contributed by AV, 9-Aug-2020.) |
Theorem | ncoprmgcdgt1b 12016* | Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is greater than 1. (Contributed by AV, 9-Aug-2020.) |
Theorem | coprmdvds1 12017 | If two positive integers are coprime, i.e. their greatest common divisor is 1, the only positive integer that divides both of them is 1. (Contributed by AV, 4-Aug-2021.) |
Theorem | coprmdvds 12018 | Euclid's Lemma (see ProofWiki "Euclid's Lemma", 10-Jul-2021, https://proofwiki.org/wiki/Euclid's_Lemma): If an integer divides the product of two integers and is coprime to one of them, then it divides the other. See also theorem 1.5 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by AV, 10-Jul-2021.) |
Theorem | coprmdvds2 12019 | If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | mulgcddvds 12020 | One half of rpmulgcd2 12021, which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015.) |
Theorem | rpmulgcd2 12021 | If is relatively prime to , then the GCD of with is the product of the GCDs with and respectively. (Contributed by Mario Carneiro, 2-Jul-2015.) |
Theorem | qredeq 12022 | Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.) |
Theorem | qredeu 12023* | Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013.) |
Theorem | rpmul 12024 | If is relatively prime to and to , it is also relatively prime to their product. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-Jul-2015.) |
Theorem | rpdvds 12025 | If is relatively prime to then it is also relatively prime to any divisor of . (Contributed by Mario Carneiro, 19-Jun-2015.) |
Theorem | congr 12026* | Definition of congruence by integer multiple (see ProofWiki "Congruence (Number Theory)", 11-Jul-2021, https://proofwiki.org/wiki/Definition:Congruence_(Number_Theory)): An integer is congruent to an integer modulo if their difference is a multiple of . See also the definition in [ApostolNT] p. 104: "... is congruent to modulo , and we write (mod ) if divides the difference ", or Wikipedia "Modular arithmetic - Congruence", https://en.wikipedia.org/wiki/Modular_arithmetic#Congruence, 11-Jul-2021,: "Given an integer n > 1, called a modulus, two integers are said to be congruent modulo n, if n is a divisor of their difference (i.e., if there is an integer k such that a-b = kn)". (Contributed by AV, 11-Jul-2021.) |
Theorem | divgcdcoprm0 12027 | Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.) |
Theorem | divgcdcoprmex 12028* | Integers divided by gcd are coprime (see ProofWiki "Integers Divided by GCD are Coprime", 11-Jul-2021, https://proofwiki.org/wiki/Integers_Divided_by_GCD_are_Coprime): Any pair of integers, not both zero, can be reduced to a pair of coprime ones by dividing them by their gcd. (Contributed by AV, 12-Jul-2021.) |
Theorem | cncongr1 12029 | One direction of the bicondition in cncongr 12031. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.) |
Theorem | cncongr2 12030 | The other direction of the bicondition in cncongr 12031. (Contributed by AV, 11-Jul-2021.) |
Theorem | cncongr 12031 | Cancellability of Congruences (see ProofWiki "Cancellability of Congruences, https://proofwiki.org/wiki/Cancellability_of_Congruences, 10-Jul-2021): Two products with a common factor are congruent modulo a positive integer iff the other factors are congruent modulo the integer divided by the greates common divisor of the integer and the common factor. See also Theorem 5.4 "Cancellation law" in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.) |
Theorem | cncongrcoprm 12032 | Corollary 1 of Cancellability of Congruences: Two products with a common factor are congruent modulo an integer being coprime to the common factor iff the other factors are congruent modulo the integer. (Contributed by AV, 13-Jul-2021.) |
Remark: to represent odd prime numbers, i.e., all prime numbers except , the idiom is used. It is a little bit shorter than . Both representations can be converted into each other by eldifsn 3700. | ||
Syntax | cprime 12033 | Extend the definition of a class to include the set of prime numbers. |
Definition | df-prm 12034* | Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | isprm 12035* | The predicate "is a prime number". A prime number is a positive integer with exactly two positive divisors. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | prmnn 12036 | A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | prmz 12037 | A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.) |
Theorem | prmssnn 12038 | The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.) |
Theorem | prmex 12039 | The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.) |
Theorem | 1nprm 12040 | 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
Theorem | 1idssfct 12041* | The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | isprm2lem 12042* | Lemma for isprm2 12043. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | isprm2 12043* | The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only positive divisors are 1 and itself. Definition in [ApostolNT] p. 16. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | isprm3 12044* | The predicate "is a prime number". A prime number is an integer greater than or equal to 2 with no divisors strictly between 1 and itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | isprm4 12045* | The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only divisor greater than or equal to 2 is itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | prmind2 12046* | A variation on prmind 12047 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | prmind 12047* | Perform induction over the multiplicative structure of . If a property holds for the primes and and is preserved under multiplication, then it holds for every positive integer. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | dvdsprime 12048 | If divides a prime, then is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.) |
Theorem | nprm 12049 | A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | nprmi 12050 | An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
Theorem | dvdsnprmd 12051 | If a number is divisible by an integer greater than 1 and less then the number, the number is not prime. (Contributed by AV, 24-Jul-2021.) |
Theorem | prm2orodd 12052 | A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.) |
Theorem | 2prm 12053 | 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
Theorem | 3prm 12054 | 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | 4nprm 12055 | 4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.) |
Theorem | prmdc 12056 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) |
DECID | ||
Theorem | prmuz2 12057 | A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | prmgt1 12058 | A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
Theorem | prmm2nn0 12059 | Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
Theorem | oddprmgt2 12060 | An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.) |
Theorem | oddprmge3 12061 | An odd prime is greater than or equal to 3. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 20-Aug-2021.) |
Theorem | sqnprm 12062 | A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | dvdsprm 12063 | An integer greater than or equal to 2 divides a prime number iff it is equal to it. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | exprmfct 12064* | Every integer greater than or equal to 2 has a prime factor. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 20-Jun-2015.) |
Theorem | prmdvdsfz 12065* | Each integer greater than 1 and less then or equal to a fixed number is divisible by a prime less then or equal to this fixed number. (Contributed by AV, 15-Aug-2020.) |
Theorem | nprmdvds1 12066 | No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.) |
Theorem | isprm5lem 12067* | Lemma for isprm5 12068. The interesting direction (showing that one only needs to check prime divisors up to the square root of ). (Contributed by Jim Kingdon, 20-Oct-2024.) |
Theorem | isprm5 12068* | One need only check prime divisors of up to in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | divgcdodd 12069 | Either is odd or is odd. (Contributed by Scott Fenton, 19-Apr-2014.) |
This section is about coprimality with respect to primes, and a special version of Euclid's lemma for primes is provided, see euclemma 12072. | ||
Theorem | coprm 12070 | A prime number either divides an integer or is coprime to it, but not both. Theorem 1.8 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | prmrp 12071 | Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | euclemma 12072 | Euclid's lemma. A prime number divides the product of two integers iff it divides at least one of them. Theorem 1.9 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | isprm6 12073* | A number is prime iff it satisfies Euclid's lemma euclemma 12072. (Contributed by Mario Carneiro, 6-Sep-2015.) |
Theorem | prmdvdsexp 12074 | A prime divides a positive power of an integer iff it divides the integer. (Contributed by Mario Carneiro, 24-Feb-2014.) (Revised by Mario Carneiro, 17-Jul-2014.) |
Theorem | prmdvdsexpb 12075 | A prime divides a positive power of another iff they are equal. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 24-Feb-2014.) |
Theorem | prmdvdsexpr 12076 | If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Theorem | prmexpb 12077 | Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.) |
Theorem | prmfac1 12078 | The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.) |
Theorem | rpexp 12079 | If two numbers and are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | rpexp1i 12080 | Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
Theorem | rpexp12i 12081 | Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
Theorem | prmndvdsfaclt 12082 | A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021.) |
Theorem | cncongrprm 12083 | Corollary 2 of Cancellability of Congruences: Two products with a common factor are congruent modulo a prime number not dividing the common factor iff the other factors are congruent modulo the prime number. (Contributed by AV, 13-Jul-2021.) |
Theorem | isevengcd2 12084 | The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.) |
Theorem | isoddgcd1 12085 | The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.) |
Theorem | 3lcm2e6 12086 | The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 27-Aug-2020.) |
lcm | ||
Theorem | sqrt2irrlem 12087 | Lemma for sqrt2irr 12088. This is the core of the proof: - if , then and are even, so and are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) |
Theorem | sqrt2irr 12088 |
The square root of 2 is not rational. That is, for any rational number,
does not equal it. However, if we were to say "the
square root of 2 is irrational" that would mean something stronger:
"for any rational number, is apart from it" (the two
statements are equivalent given excluded middle). See sqrt2irrap 12106 for
the proof that the square root of two is irrational.
The proof's core is proven in sqrt2irrlem 12087, which shows that if , then and are even, so and are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
Theorem | sqrt2re 12089 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
Theorem | sqrt2irr0 12090 | The square root of 2 is not rational. (Contributed by AV, 23-Dec-2022.) |
Theorem | pw2dvdslemn 12091* | Lemma for pw2dvds 12092. If a natural number has some power of two which does not divide it, there is a highest power of two which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.) |
Theorem | pw2dvds 12092* | A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.) |
Theorem | pw2dvdseulemle 12093 | Lemma for pw2dvdseu 12094. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | pw2dvdseu 12094* | A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdclemxy 12095* | Lemma for oddpwdc 12100. Another way of stating that decomposing a natural number into a power of two and an odd number is unique. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdclemdvds 12096* | Lemma for oddpwdc 12100. A natural number is divisible by the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | oddpwdclemndvds 12097* | Lemma for oddpwdc 12100. A natural number is not divisible by one more than the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | oddpwdclemodd 12098* | Lemma for oddpwdc 12100. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdclemdc 12099* | Lemma for oddpwdc 12100. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdc 12100* | The function that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |