![]() |
Metamath
Proof Explorer Theorem List (p. 167 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rpdvds 16601 | If πΎ is relatively prime to π then it is also relatively prime to any divisor π of π. (Contributed by Mario Carneiro, 19-Jun-2015.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ ((πΎ gcd π) = 1 β§ π β₯ π)) β (πΎ gcd π) = 1) | ||
Theorem | coprmprod 16602* | The product of the elements of a sequence of pairwise coprime positive integers is coprime to a positive integer which is coprime to all integers of the sequence. (Contributed by AV, 18-Aug-2020.) |
β’ (((π β Fin β§ π β β β§ π β β) β§ πΉ:ββΆβ β§ βπ β π ((πΉβπ) gcd π) = 1) β (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β (βπ β π (πΉβπ) gcd π) = 1)) | ||
Theorem | coprmproddvdslem 16603* | Lemma for coprmproddvds 16604: Induction step. (Contributed by AV, 19-Aug-2020.) |
β’ ((π¦ β Fin β§ Β¬ π§ β π¦) β ((((π¦ β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§ (βπ β π¦ βπ β (π¦ β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π¦ (πΉβπ) β₯ πΎ)) β βπ β π¦ (πΉβπ) β₯ πΎ) β ((((π¦ βͺ {π§}) β β β§ (πΎ β β β§ πΉ:ββΆβ)) β§ (βπ β (π¦ βͺ {π§})βπ β ((π¦ βͺ {π§}) β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ)) β βπ β (π¦ βͺ {π§})(πΉβπ) β₯ πΎ))) | ||
Theorem | coprmproddvds 16604* | If a positive integer is divisible by each element of a set of pairwise coprime positive integers, then it is divisible by their product. (Contributed by AV, 19-Aug-2020.) |
β’ (((π β β β§ π β Fin) β§ (πΎ β β β§ πΉ:ββΆβ) β§ (βπ β π βπ β (π β {π})((πΉβπ) gcd (πΉβπ)) = 1 β§ βπ β π (πΉβπ) β₯ πΎ)) β βπ β π (πΉβπ) β₯ πΎ) | ||
Theorem | congr 16605* | 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.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β ((π΄ mod π) = (π΅ mod π) β βπ β β€ (π Β· π) = (π΄ β π΅))) | ||
Theorem | divgcdcoprm0 16606 | Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π΅ β 0) β ((π΄ / (π΄ gcd π΅)) gcd (π΅ / (π΄ gcd π΅))) = 1) | ||
Theorem | divgcdcoprmex 16607* | 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.) |
β’ ((π΄ β β€ β§ (π΅ β β€ β§ π΅ β 0) β§ π = (π΄ gcd π΅)) β βπ β β€ βπ β β€ (π΄ = (π Β· π) β§ π΅ = (π Β· π) β§ (π gcd π) = 1)) | ||
Theorem | cncongr1 16608 | One direction of the bicondition in cncongr 16610. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π β β β§ π = (π / (πΆ gcd π)))) β (((π΄ Β· πΆ) mod π) = ((π΅ Β· πΆ) mod π) β (π΄ mod π) = (π΅ mod π))) | ||
Theorem | cncongr2 16609 | The other direction of the bicondition in cncongr 16610. (Contributed by AV, 11-Jul-2021.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π β β β§ π = (π / (πΆ gcd π)))) β ((π΄ mod π) = (π΅ mod π) β ((π΄ Β· πΆ) mod π) = ((π΅ Β· πΆ) mod π))) | ||
Theorem | cncongr 16610 | 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.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π β β β§ π = (π / (πΆ gcd π)))) β (((π΄ Β· πΆ) mod π) = ((π΅ Β· πΆ) mod π) β (π΄ mod π) = (π΅ mod π))) | ||
Theorem | cncongrcoprm 16611 | 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.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π β β β§ (πΆ gcd π) = 1)) β (((π΄ Β· πΆ) mod π) = ((π΅ Β· πΆ) mod π) β (π΄ mod π) = (π΅ mod π))) | ||
Remark: to represent odd prime numbers, i.e., all prime numbers except 2, the idiom π β (β β {2}) is used. It is a little bit shorter than (π β β β§ π β 2). Both representations can be converted into each other by eldifsn 4789. | ||
Syntax | cprime 16612 | Extend the definition of a class to include the set of prime numbers. |
class β | ||
Definition | df-prm 16613* | Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ β = {π β β β£ {π β β β£ π β₯ π} β 2o} | ||
Theorem | isprm 16614* | 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.) |
β’ (π β β β (π β β β§ {π β β β£ π β₯ π} β 2o)) | ||
Theorem | prmnn 16615 | A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β β β π β β) | ||
Theorem | prmz 16616 | A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.) |
β’ (π β β β π β β€) | ||
Theorem | prmssnn 16617 | The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.) |
β’ β β β | ||
Theorem | prmex 16618 | The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.) |
β’ β β V | ||
Theorem | 0nprm 16619 | 0 is not a prime number. Already Definition df-prm 16613 excludes 0 from being prime (β = {π β β β£ ...), but even if π β β0 was allowed, the condition {π β β β£ π β₯ π} β 2o would not hold for π = 0, because {π β β β£ π β₯ 0} = β, see dvds0 16219, and Β¬ β β 2o (there are more than 2 positive integers). (Contributed by AV, 29-May-2023.) |
β’ Β¬ 0 β β | ||
Theorem | 1nprm 16620 | 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
β’ Β¬ 1 β β | ||
Theorem | 1idssfct 16621* | The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β β β {1, π} β {π β β β£ π β₯ π}) | ||
Theorem | isprm2lem 16622* | Lemma for isprm2 16623. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ ((π β β β§ π β 1) β ({π β β β£ π β₯ π} β 2o β {π β β β£ π β₯ π} = {1, π})) | ||
Theorem | isprm2 16623* | 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.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β β (π§ β₯ π β (π§ = 1 β¨ π§ = π)))) | ||
Theorem | isprm3 16624* | 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.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β (2...(π β 1)) Β¬ π§ β₯ π)) | ||
Theorem | isprm4 16625* | 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.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β (β€β₯β2)(π§ β₯ π β π§ = π))) | ||
Theorem | prmind2 16626* | A variation on prmind 16627 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (π₯ = 1 β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π§ β (π β π)) & β’ (π₯ = (π¦ Β· π§) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ ((π₯ β β β§ βπ¦ β (1...(π₯ β 1))π) β π) & β’ ((π¦ β (β€β₯β2) β§ π§ β (β€β₯β2)) β ((π β§ π) β π)) β β’ (π΄ β β β π) | ||
Theorem | prmind 16627* | Perform induction over the multiplicative structure of β. If a property π(π₯) holds for the primes and 1 and is preserved under multiplication, then it holds for every positive integer. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (π₯ = 1 β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π§ β (π β π)) & β’ (π₯ = (π¦ Β· π§) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π₯ β β β π) & β’ ((π¦ β (β€β₯β2) β§ π§ β (β€β₯β2)) β ((π β§ π) β π)) β β’ (π΄ β β β π) | ||
Theorem | dvdsprime 16628 | If π divides a prime, then π is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.) |
β’ ((π β β β§ π β β) β (π β₯ π β (π = π β¨ π = 1))) | ||
Theorem | nprm 16629 | A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ ((π΄ β (β€β₯β2) β§ π΅ β (β€β₯β2)) β Β¬ (π΄ Β· π΅) β β) | ||
Theorem | nprmi 16630 | An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
β’ π΄ β β & β’ π΅ β β & β’ 1 < π΄ & β’ 1 < π΅ & β’ (π΄ Β· π΅) = π β β’ Β¬ π β β | ||
Theorem | dvdsnprmd 16631 | If a number is divisible by an integer greater than 1 and less than the number, the number is not prime. (Contributed by AV, 24-Jul-2021.) |
β’ (π β 1 < π΄) & β’ (π β π΄ < π) & β’ (π β π΄ β₯ π) β β’ (π β Β¬ π β β) | ||
Theorem | prm2orodd 16632 | A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.) |
β’ (π β β β (π = 2 β¨ Β¬ 2 β₯ π)) | ||
Theorem | 2prm 16633 | 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
β’ 2 β β | ||
Theorem | 2mulprm 16634 | A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023.) |
β’ (π΄ β β€ β ((2 Β· π΄) β β β π΄ = 1)) | ||
Theorem | 3prm 16635 | 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ 3 β β | ||
Theorem | 4nprm 16636 | 4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.) |
β’ Β¬ 4 β β | ||
Theorem | prmuz2 16637 | A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ (π β β β π β (β€β₯β2)) | ||
Theorem | prmgt1 16638 | A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
β’ (π β β β 1 < π) | ||
Theorem | prmm2nn0 16639 | Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
β’ (π β β β (π β 2) β β0) | ||
Theorem | oddprmgt2 16640 | An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.) |
β’ (π β (β β {2}) β 2 < π) | ||
Theorem | oddprmge3 16641 | 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.) |
β’ (π β (β β {2}) β π β (β€β₯β3)) | ||
Theorem | ge2nprmge4 16642 | A composite integer greater than or equal to 2 is greater than or equal to 4. (Contributed by AV, 5-Jun-2023.) |
β’ ((π β (β€β₯β2) β§ π β β) β π β (β€β₯β4)) | ||
Theorem | sqnprm 16643 | A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (π΄ β β€ β Β¬ (π΄β2) β β) | ||
Theorem | dvdsprm 16644 | 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.) |
β’ ((π β (β€β₯β2) β§ π β β) β (π β₯ π β π = π)) | ||
Theorem | exprmfct 16645* | 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.) |
β’ (π β (β€β₯β2) β βπ β β π β₯ π) | ||
Theorem | prmdvdsfz 16646* | 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.) |
β’ ((π β β β§ πΌ β (2...π)) β βπ β β (π β€ π β§ π β₯ πΌ)) | ||
Theorem | nprmdvds1 16647 | No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.) |
β’ (π β β β Β¬ π β₯ 1) | ||
Theorem | isprm5 16648* | One need only check prime divisors of π up to βπ in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β β ((π§β2) β€ π β Β¬ π§ β₯ π))) | ||
Theorem | isprm7 16649* | One need only check prime divisors of π up to βπ in order to ensure primality. This version of isprm5 16648 combines the primality and bound on π§ into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β ((2...(ββ(ββπ))) β© β) Β¬ π§ β₯ π)) | ||
Theorem | maxprmfct 16650* | The set of prime factors of an integer greater than or equal to 2 satisfies the conditions to have a supremum, and that supremum is a member of the set. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ π = {π§ β β β£ π§ β₯ π} β β’ (π β (β€β₯β2) β ((π β β€ β§ π β β β§ βπ₯ β β€ βπ¦ β π π¦ β€ π₯) β§ sup(π, β, < ) β π)) | ||
Theorem | divgcdodd 16651 | Either π΄ / (π΄ gcd π΅) is odd or π΅ / (π΄ gcd π΅) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (Β¬ 2 β₯ (π΄ / (π΄ gcd π΅)) β¨ Β¬ 2 β₯ (π΅ / (π΄ gcd π΅)))) | ||
This section is about coprimality with respect to primes, and a special version of Euclid's lemma for primes is provided, see euclemma 16654. | ||
Theorem | coprm 16652 | 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.) |
β’ ((π β β β§ π β β€) β (Β¬ π β₯ π β (π gcd π) = 1)) | ||
Theorem | prmrp 16653 | Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β ((π gcd π) = 1 β π β π)) | ||
Theorem | euclemma 16654 | 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 16655* | A number is prime iff it satisfies Euclid's lemma euclemma 16654. (Contributed by Mario Carneiro, 6-Sep-2015.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ₯ β β€ βπ¦ β β€ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) | ||
Theorem | prmdvdsexp 16656 | 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 16657 | 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 16658 | If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ ((π β β β§ π β β β§ π β β0) β (π β₯ (πβπ) β π = π)) | ||
Theorem | prmdvdssq 16659 | Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by SN, 21-Aug-2024.) |
β’ ((π β β β§ π β β€) β (π β₯ π β π β₯ (πβ2))) | ||
Theorem | prmdvdssqOLD 16660 | Obsolete version of prmdvdssq 16659 as of 21-Aug-2024. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β β β§ π β β€) β (π β₯ π β π β₯ (πβ2))) | ||
Theorem | prmexpb 16661 | Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.) |
β’ (((π β β β§ π β β) β§ (π β β β§ π β β)) β ((πβπ) = (πβπ) β (π = π β§ π = π))) | ||
Theorem | prmfac1 16662 | The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.) |
β’ ((π β β0 β§ π β β β§ π β₯ (!βπ)) β π β€ π) | ||
Theorem | rpexp 16663 | 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.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β (((π΄βπ) gcd π΅) = 1 β (π΄ gcd π΅) = 1)) | ||
Theorem | rpexp1i 16664 | Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd π΅) = 1)) | ||
Theorem | rpexp12i 16665 | Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ (π β β0 β§ π β β0)) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd (π΅βπ)) = 1)) | ||
Theorem | prmndvdsfaclt 16666 | A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021.) |
β’ ((π β β β§ π β β0) β (π < π β Β¬ π β₯ (!βπ))) | ||
Theorem | prmdvdsncoprmbd 16667* | Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b 16591 with the existential quantifier over the primes instead of integers greater than or equal to 2. (Contributed by SN, 24-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (βπ β β (π β₯ π΄ β§ π β₯ π΅) β (π΄ gcd π΅) β 1)) | ||
Theorem | ncoprmlnprm 16668 | If two positive integers are not coprime, the larger of them is not a prime number. (Contributed by AV, 9-Aug-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β (1 < (π΄ gcd π΅) β π΅ β β)) | ||
Theorem | cncongrprm 16669 | 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.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π β β β§ Β¬ π β₯ πΆ)) β (((π΄ Β· πΆ) mod π) = ((π΅ Β· πΆ) mod π) β (π΄ mod π) = (π΅ mod π))) | ||
Theorem | isevengcd2 16670 | 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.) |
β’ (π β β€ β (2 β₯ π β (2 gcd π) = 2)) | ||
Theorem | isoddgcd1 16671 | 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.) |
β’ (π β β€ β (Β¬ 2 β₯ π β (2 gcd π) = 1)) | ||
Theorem | 3lcm2e6 16672 | 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.) |
β’ (3 lcm 2) = 6 | ||
Syntax | cnumer 16673 | Extend class notation to include canonical numerator function. |
class numer | ||
Syntax | cdenom 16674 | Extend class notation to include canonical denominator function. |
class denom | ||
Definition | df-numer 16675* | 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 = (π¦ β β β¦ (1st β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π¦ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Definition | df-denom 16676* | 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 = (π¦ β β β¦ (2nd β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π¦ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qnumval 16677* | Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (numerβπ΄) = (1st β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π΄ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qdenval 16678* | Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (denomβπ΄) = (2nd β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π΄ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qnumdencl 16679 | Lemma for qnumcl 16680 and qdencl 16681. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β ((numerβπ΄) β β€ β§ (denomβπ΄) β β)) | ||
Theorem | qnumcl 16680 | The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (numerβπ΄) β β€) | ||
Theorem | qdencl 16681 | The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (denomβπ΄) β β) | ||
Theorem | fnum 16682 | Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ numer:ββΆβ€ | ||
Theorem | fden 16683 | Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ denom:ββΆβ | ||
Theorem | qnumdenbi 16684 | 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.) |
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β (((π΅ gcd πΆ) = 1 β§ π΄ = (π΅ / πΆ)) β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) | ||
Theorem | qnumdencoprm 16685 | The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β ((numerβπ΄) gcd (denomβπ΄)) = 1) | ||
Theorem | qeqnumdivden 16686 | Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β π΄ = ((numerβπ΄) / (denomβπ΄))) | ||
Theorem | qmuldeneqnum 16687 | Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (π΄ Β· (denomβπ΄)) = (numerβπ΄)) | ||
Theorem | divnumden 16688 | Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β) β ((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅)))) | ||
Theorem | divdenle 16689 | Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β) β (denomβ(π΄ / π΅)) β€ π΅) | ||
Theorem | qnumgt0 16690 | A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (0 < π΄ β 0 < (numerβπ΄))) | ||
Theorem | qgt0numnn 16691 | A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β β§ 0 < π΄) β (numerβπ΄) β β) | ||
Theorem | nn0gcdsq 16692 | Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β0 β§ π΅ β β0) β ((π΄ gcd π΅)β2) = ((π΄β2) gcd (π΅β2))) | ||
Theorem | zgcdsq 16693 | nn0gcdsq 16692 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅)β2) = ((π΄β2) gcd (π΅β2))) | ||
Theorem | numdensq 16694 | Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β ((numerβ(π΄β2)) = ((numerβπ΄)β2) β§ (denomβ(π΄β2)) = ((denomβπ΄)β2))) | ||
Theorem | numsq 16695 | Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (numerβ(π΄β2)) = ((numerβπ΄)β2)) | ||
Theorem | densq 16696 | Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (denomβ(π΄β2)) = ((denomβπ΄)β2)) | ||
Theorem | qden1elz 16697 | A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β ((denomβπ΄) = 1 β π΄ β β€)) | ||
Theorem | zsqrtelqelz 16698 | If an integer has a rational square root, that root is must be an integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β€ β§ (ββπ΄) β β) β (ββπ΄) β β€) | ||
Theorem | nonsq 16699 | Any integer strictly between two adjacent squares has an irrational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (((π΄ β β0 β§ π΅ β β0) β§ ((π΅β2) < π΄ β§ π΄ < ((π΅ + 1)β2))) β Β¬ (ββπ΄) β β) | ||
Syntax | codz 16700 | Extend class notation with the order function on the class of integers modulo N. |
class odβ€ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |