Home | Intuitionistic Logic Explorer Theorem List (p. 118 of 132) | < 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 | coprmdvds2 11701 | 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 11702 | One half of rpmulgcd2 11703, which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015.) |
Theorem | rpmulgcd2 11703 | 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 11704 | Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.) |
Theorem | qredeu 11705* | Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013.) |
Theorem | rpmul 11706 | 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 11707 | If is relatively prime to then it is also relatively prime to any divisor of . (Contributed by Mario Carneiro, 19-Jun-2015.) |
Theorem | congr 11708* | 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 11709 | Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.) |
Theorem | divgcdcoprmex 11710* | 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 11711 | One direction of the bicondition in cncongr 11713. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.) |
Theorem | cncongr2 11712 | The other direction of the bicondition in cncongr 11713. (Contributed by AV, 11-Jul-2021.) |
Theorem | cncongr 11713 | 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 11714 | 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 3620. | ||
Syntax | cprime 11715 | Extend the definition of a class to include the set of prime numbers. |
Definition | df-prm 11716* | Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | isprm 11717* | 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 11718 | A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | prmz 11719 | A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.) |
Theorem | prmssnn 11720 | The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.) |
Theorem | prmex 11721 | The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.) |
Theorem | 1nprm 11722 | 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
Theorem | 1idssfct 11723* | The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | isprm2lem 11724* | Lemma for isprm2 11725. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | isprm2 11725* | 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 11726* | 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 11727* | 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 11728* | A variation on prmind 11729 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | prmind 11729* | 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 11730 | If divides a prime, then is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.) |
Theorem | nprm 11731 | A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | nprmi 11732 | An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
Theorem | dvdsnprmd 11733 | 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 11734 | A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.) |
Theorem | 2prm 11735 | 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
Theorem | 3prm 11736 | 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | 4nprm 11737 | 4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.) |
Theorem | prmuz2 11738 | A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | prmgt1 11739 | A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
Theorem | prmm2nn0 11740 | Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
Theorem | oddprmgt2 11741 | An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.) |
Theorem | oddprmge3 11742 | 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 11743 | A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.) |
Theorem | dvdsprm 11744 | 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 11745* | 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 11746* | 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 11747 | No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.) |
Theorem | divgcdodd 11748 | 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 11751. | ||
Theorem | coprm 11749 | 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 11750 | Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | euclemma 11751 | 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 11752* | A number is prime iff it satisfies Euclid's lemma euclemma 11751. (Contributed by Mario Carneiro, 6-Sep-2015.) |
Theorem | prmdvdsexp 11753 | 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 11754 | 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 11755 | If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Theorem | prmexpb 11756 | Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.) |
Theorem | prmfac1 11757 | The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.) |
Theorem | rpexp 11758 | 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 11759 | Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
Theorem | rpexp12i 11760 | Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
Theorem | prmndvdsfaclt 11761 | 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 11762 | 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 11763 | 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 11764 | 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 11765 | 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 11766 | Lemma for sqrt2irr 11767. 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 11767 |
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 11785 for
the proof that the square root of two is irrational.
The proof's core is proven in sqrt2irrlem 11766, 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 11768 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
Theorem | sqrt2irr0 11769 | The square root of 2 is not rational. (Contributed by AV, 23-Dec-2022.) |
Theorem | pw2dvdslemn 11770* | Lemma for pw2dvds 11771. 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 11771* | A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.) |
Theorem | pw2dvdseulemle 11772 | Lemma for pw2dvdseu 11773. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | pw2dvdseu 11773* | A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdclemxy 11774* | Lemma for oddpwdc 11779. 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 11775* | Lemma for oddpwdc 11779. A natural number is divisible by the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | oddpwdclemndvds 11776* | Lemma for oddpwdc 11779. 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 11777* | Lemma for oddpwdc 11779. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdclemdc 11778* | Lemma for oddpwdc 11779. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.) |
Theorem | oddpwdc 11779* | 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.) |
Theorem | sqpweven 11780* | The greatest power of two dividing the square of an integer is an even power of two. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | 2sqpwodd 11781* | The greatest power of two dividing twice the square of an integer is an odd power of two. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | sqne2sq 11782 | The square of a natural number can never be equal to two times the square of a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) |
Theorem | znege1 11783 | The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.) |
Theorem | sqrt2irraplemnn 11784 | Lemma for sqrt2irrap 11785. The square root of 2 is apart from a positive rational expressed as a numerator and denominator. (Contributed by Jim Kingdon, 2-Oct-2021.) |
# | ||
Theorem | sqrt2irrap 11785 | The square root of 2 is irrational. That is, for any rational number, is apart from it. In the absence of excluded middle, we can distinguish between this and "the square root of 2 is not rational" which is sqrt2irr 11767. (Contributed by Jim Kingdon, 2-Oct-2021.) |
# | ||
Syntax | cnumer 11786 | Extend class notation to include canonical numerator function. |
numer | ||
Syntax | cdenom 11787 | Extend class notation to include canonical denominator function. |
denom | ||
Definition | df-numer 11788* | The canonical numerator of a rational is the numerator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer | ||
Definition | df-denom 11789* | The canonical denominator of a rational is the denominator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom | ||
Theorem | qnumval 11790* | Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer | ||
Theorem | qdenval 11791* | Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom | ||
Theorem | qnumdencl 11792 | Lemma for qnumcl 11793 and qdencl 11794. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer denom | ||
Theorem | qnumcl 11793 | The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer | ||
Theorem | qdencl 11794 | The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom | ||
Theorem | fnum 11795 | Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer | ||
Theorem | fden 11796 | Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom | ||
Theorem | qnumdenbi 11797 | Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer denom | ||
Theorem | qnumdencoprm 11798 | The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer denom | ||
Theorem | qeqnumdivden 11799 | Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
numer denom | ||
Theorem | qmuldeneqnum 11800 | Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom numer |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |