![]() |
Intuitionistic Logic Explorer Theorem List (p. 121 of 150) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bezoutlemmain 12001* | Lemma for Bรฉzout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.) |
โข (๐ โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) & โข (๐ โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ))) & โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) โ โข (๐ โ โ๐ฅ โ โ0 ([๐ฅ / ๐]๐ โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐)))) | ||
Theorem | bezoutlema 12002* | Lemma for Bรฉzout's identity. The is-bezout condition is satisfied by ๐ด. (Contributed by Jim Kingdon, 30-Dec-2021.) |
โข (๐ โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) & โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) โ โข (๐ โ [๐ด / ๐]๐) | ||
Theorem | bezoutlemb 12003* | Lemma for Bรฉzout's identity. The is-bezout condition is satisfied by ๐ต. (Contributed by Jim Kingdon, 30-Dec-2021.) |
โข (๐ โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) & โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ต โ โ0) โ โข (๐ โ [๐ต / ๐]๐) | ||
Theorem | bezoutlemex 12004* | Lemma for Bรฉzout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0) โ โ๐ โ โ0 (โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) | ||
Theorem | bezoutlemzz 12005* | Lemma for Bรฉzout's identity. Like bezoutlemex 12004 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) | ||
Theorem | bezoutlemaz 12006* | Lemma for Bรฉzout's identity. Like bezoutlemzz 12005 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
โข ((๐ด โ โค โง ๐ต โ โ0) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) | ||
Theorem | bezoutlembz 12007* | Lemma for Bรฉzout's identity. Like bezoutlemaz 12006 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) | ||
Theorem | bezoutlembi 12008* | Lemma for Bรฉzout's identity. Like bezoutlembz 12007 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ โ๐ โ โ0 (โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)) โง โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ)))) | ||
Theorem | bezoutlemmo 12009* | Lemma for Bรฉzout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ท โ โ0) & โข (๐ โ โ๐ง โ โค (๐ง โฅ ๐ท โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) & โข (๐ โ ๐ธ โ โ0) & โข (๐ โ โ๐ง โ โค (๐ง โฅ ๐ธ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) โ โข (๐ โ ๐ท = ๐ธ) | ||
Theorem | bezoutlemeu 12010* | Lemma for Bรฉzout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ท โ โ0) & โข (๐ โ โ๐ง โ โค (๐ง โฅ ๐ท โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) โ โข (๐ โ โ!๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) | ||
Theorem | bezoutlemle 12011* | Lemma for Bรฉzout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both ๐ด and ๐ต. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ท โ โ0) & โข (๐ โ โ๐ง โ โค (๐ง โฅ ๐ท โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) & โข (๐ โ ยฌ (๐ด = 0 โง ๐ต = 0)) โ โข (๐ โ โ๐ง โ โค ((๐ง โฅ ๐ด โง ๐ง โฅ ๐ต) โ ๐ง โค ๐ท)) | ||
Theorem | bezoutlemsup 12012* | Lemma for Bรฉzout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both ๐ด and ๐ต. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐ท โ โ0) & โข (๐ โ โ๐ง โ โค (๐ง โฅ ๐ท โ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต))) & โข (๐ โ ยฌ (๐ด = 0 โง ๐ต = 0)) โ โข (๐ โ ๐ท = sup({๐ง โ โค โฃ (๐ง โฅ ๐ด โง ๐ง โฅ ๐ต)}, โ, < )) | ||
Theorem | dfgcd3 12013* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (โฉ๐ โ โ0 โ๐ง โ โค (๐ง โฅ ๐ โ (๐ง โฅ ๐ โง ๐ง โฅ ๐)))) | ||
Theorem | bezout 12014* |
Bรฉzout's identity: For any integers ๐ด and ๐ต, there are
integers ๐ฅ, ๐ฆ such that (๐ด gcd ๐ต) = ๐ด ยท ๐ฅ + ๐ต ยท ๐ฆ. This
is Metamath 100 proof #60.
The proof is constructive, in the sense that it applies the Extended Euclidian Algorithm to constuct a number which can be shown to be (๐ด gcd ๐ต) and which satisfies the rest of the theorem. In the presence of excluded middle, it is common to prove Bรฉzout's identity by taking the smallest number which satisfies the Bรฉzout condition, and showing it is the greatest common divisor. But we do not have the ability to show that number exists other than by providing a way to determine it. (Contributed by Mario Carneiro, 22-Feb-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ โ๐ฅ โ โค โ๐ฆ โ โค (๐ด gcd ๐ต) = ((๐ด ยท ๐ฅ) + (๐ต ยท ๐ฆ))) | ||
Theorem | dvdsgcd 12015 | An integer which divides each of two others also divides their gcd. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 30-May-2014.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ gcd ๐))) | ||
Theorem | dvdsgcdb 12016 | Biconditional form of dvdsgcd 12015. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ gcd ๐))) | ||
Theorem | dfgcd2 12017* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ท = (๐ gcd ๐) โ (0 โค ๐ท โง (๐ท โฅ ๐ โง ๐ท โฅ ๐) โง โ๐ โ โค ((๐ โฅ ๐ โง ๐ โฅ ๐) โ ๐ โฅ ๐ท)))) | ||
Theorem | gcdass 12018 | Associative law for gcd operator. Theorem 1.4(b) in [ApostolNT] p. 16. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) gcd ๐) = (๐ gcd (๐ gcd ๐))) | ||
Theorem | mulgcd 12019 | Distribute multiplication by a nonnegative integer over gcd. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
โข ((๐พ โ โ0 โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) gcd (๐พ ยท ๐)) = (๐พ ยท (๐ gcd ๐))) | ||
Theorem | absmulgcd 12020 | Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) gcd (๐พ ยท ๐)) = (absโ(๐พ ยท (๐ gcd ๐)))) | ||
Theorem | mulgcdr 12021 | Reverse distribution law for the gcd operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ0) โ ((๐ด ยท ๐ถ) gcd (๐ต ยท ๐ถ)) = ((๐ด gcd ๐ต) ยท ๐ถ)) | ||
Theorem | gcddiv 12022 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง (๐ถ โฅ ๐ด โง ๐ถ โฅ ๐ต)) โ ((๐ด gcd ๐ต) / ๐ถ) = ((๐ด / ๐ถ) gcd (๐ต / ๐ถ))) | ||
Theorem | gcdmultiple 12023 | The GCD of a multiple of a number is the number itself. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ โ โ โง ๐ โ โ) โ (๐ gcd (๐ ยท ๐)) = ๐) | ||
Theorem | gcdmultiplez 12024 | Extend gcdmultiple 12023 so ๐ can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ โ โ โง ๐ โ โค) โ (๐ gcd (๐ ยท ๐)) = ๐) | ||
Theorem | gcdzeq 12025 | A positive integer ๐ด is equal to its gcd with an integer ๐ต if and only if ๐ด divides ๐ต. Generalization of gcdeq 12026. (Contributed by AV, 1-Jul-2020.) |
โข ((๐ด โ โ โง ๐ต โ โค) โ ((๐ด gcd ๐ต) = ๐ด โ ๐ด โฅ ๐ต)) | ||
Theorem | gcdeq 12026 | ๐ด is equal to its gcd with ๐ต if and only if ๐ด divides ๐ต. (Contributed by Mario Carneiro, 23-Feb-2014.) (Proof shortened by AV, 8-Aug-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด gcd ๐ต) = ๐ด โ ๐ด โฅ ๐ต)) | ||
Theorem | dvdssqim 12027 | Unidirectional form of dvdssq 12034. (Contributed by Scott Fenton, 19-Apr-2014.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐โ2) โฅ (๐โ2))) | ||
Theorem | dvdsmulgcd 12028 | Relationship between the order of an element and that of a multiple. (a divisibility equivalent). (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ต โ โค โง ๐ถ โ โค) โ (๐ด โฅ (๐ต ยท ๐ถ) โ ๐ด โฅ (๐ต ยท (๐ถ gcd ๐ด)))) | ||
Theorem | rpmulgcd 12029 | If ๐พ and ๐ are relatively prime, then the GCD of ๐พ and ๐ ยท ๐ is the GCD of ๐พ and ๐. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โง (๐พ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) = (๐พ gcd ๐)) | ||
Theorem | rplpwr 12030 | If ๐ด and ๐ต are relatively prime, then so are ๐ดโ๐ and ๐ต. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd ๐ต) = 1)) | ||
Theorem | rppwr 12031 | If ๐ด and ๐ต are relatively prime, then so are ๐ดโ๐ and ๐ตโ๐. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ) โ ((๐ด gcd ๐ต) = 1 โ ((๐ดโ๐) gcd (๐ตโ๐)) = 1)) | ||
Theorem | sqgcd 12032 | Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐)โ2) = ((๐โ2) gcd (๐โ2))) | ||
Theorem | dvdssqlem 12033 | Lemma for dvdssq 12034. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ (๐โ2) โฅ (๐โ2))) | ||
Theorem | dvdssq 12034 | Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (๐โ2) โฅ (๐โ2))) | ||
Theorem | bezoutr 12035 | Partial converse to bezout 12014. Existence of a linear combination does not set the GCD, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โ (๐ด gcd ๐ต) โฅ ((๐ด ยท ๐) + (๐ต ยท ๐))) | ||
Theorem | bezoutr1 12036 | Converse of bezout 12014 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ โ โค โง ๐ โ โค)) โ (((๐ด ยท ๐) + (๐ต ยท ๐)) = 1 โ (๐ด gcd ๐ต) = 1)) | ||
Theorem | nnmindc 12037* | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
โข ((๐ด โ โ โง โ๐ฅ โ โ DECID ๐ฅ โ ๐ด โง โ๐ฆ ๐ฆ โ ๐ด) โ inf(๐ด, โ, < ) โ ๐ด) | ||
Theorem | nnminle 12038* | The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 12037. (Contributed by Jim Kingdon, 26-Sep-2024.) |
โข ((๐ด โ โ โง โ๐ฅ โ โ DECID ๐ฅ โ ๐ด โง ๐ต โ ๐ด) โ inf(๐ด, โ, < ) โค ๐ต) | ||
Theorem | nnwodc 12039* | Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.) |
โข ((๐ด โ โ โง โ๐ค ๐ค โ ๐ด โง โ๐ โ โ DECID ๐ โ ๐ด) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | uzwodc 12040* | Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.) |
โข ((๐ โ (โคโฅโ๐) โง โ๐ฅ ๐ฅ โ ๐ โง โ๐ฅ โ (โคโฅโ๐)DECID ๐ฅ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ ๐ โค ๐) | ||
Theorem | nnwofdc 12041* | Well-ordering principle: any inhabited decidable set of positive integers has a least element. This version allows ๐ฅ and ๐ฆ to be present in ๐ด as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.) |
โข โฒ๐ฅ๐ด & โข โฒ๐ฆ๐ด โ โข ((๐ด โ โ โง โ๐ง ๐ง โ ๐ด โง โ๐ โ โ DECID ๐ โ ๐ด) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | nnwosdc 12042* | Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.) |
โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) โ โข ((โ๐ฅ โ โ ๐ โง โ๐ฅ โ โ DECID ๐) โ โ๐ฅ โ โ (๐ โง โ๐ฆ โ โ (๐ โ ๐ฅ โค ๐ฆ))) | ||
Theorem | nn0seqcvgd 12043* | A strictly-decreasing nonnegative integer sequence with initial term ๐ reaches zero by the ๐ th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข (๐ โ ๐น:โ0โถโ0) & โข (๐ โ ๐ = (๐นโ0)) & โข ((๐ โง ๐ โ โ0) โ ((๐นโ(๐ + 1)) โ 0 โ (๐นโ(๐ + 1)) < (๐นโ๐))) โ โข (๐ โ (๐นโ๐) = 0) | ||
Theorem | ialgrlem1st 12044 | Lemma for ialgr0 12046. Expressing algrflemg 6233 in a form suitable for theorems such as seq3-1 10462 or seqf 10463. (Contributed by Jim Kingdon, 22-Jul-2021.) |
โข (๐ โ ๐น:๐โถ๐) โ โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ(๐น โ 1st )๐ฆ) โ ๐) | ||
Theorem | ialgrlemconst 12045 | Lemma for ialgr0 12046. Closure of a constant function, in a form suitable for theorems such as seq3-1 10462 or seqf 10463. (Contributed by Jim Kingdon, 22-Jul-2021.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ด โ ๐) โ โข ((๐ โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ ร {๐ด})โ๐ฅ) โ ๐) | ||
Theorem | ialgr0 12046 | The value of the algorithm iterator ๐ at 0 is the initial state ๐ด. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = seq๐((๐น โ 1st ), (๐ ร {๐ด})) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐น:๐โถ๐) โ โข (๐ โ (๐ โ๐) = ๐ด) | ||
Theorem | algrf 12047 |
An algorithm is a step function ๐น:๐โถ๐ on a state space ๐.
An algorithm acts on an initial state ๐ด โ ๐ by iteratively applying
๐น to give ๐ด, (๐นโ๐ด), (๐นโ(๐นโ๐ด)) and so
on. An algorithm is said to halt if a fixed point of ๐น is
reached
after a finite number of iterations.
The algorithm iterator ๐ :โ0โถ๐ "runs" the algorithm ๐น so that (๐ โ๐) is the state after ๐ iterations of ๐น on the initial state ๐ด. Domain and codomain of the algorithm iterator ๐ . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = seq๐((๐น โ 1st ), (๐ ร {๐ด})) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐น:๐โถ๐) โ โข (๐ โ ๐ :๐โถ๐) | ||
Theorem | algrp1 12048 | The value of the algorithm iterator ๐ at (๐พ + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = seq๐((๐น โ 1st ), (๐ ร {๐ด})) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐น:๐โถ๐) โ โข ((๐ โง ๐พ โ ๐) โ (๐ โ(๐พ + 1)) = (๐นโ(๐ โ๐พ))) | ||
Theorem | alginv 12049* | If ๐ผ is an invariant of ๐น, then its value is unchanged after any number of iterations of ๐น. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ๐ = seq0((๐น โ 1st ), (โ0 ร {๐ด})) & โข ๐น:๐โถ๐ & โข (๐ฅ โ ๐ โ (๐ผโ(๐นโ๐ฅ)) = (๐ผโ๐ฅ)) โ โข ((๐ด โ ๐ โง ๐พ โ โ0) โ (๐ผโ(๐ โ๐พ)) = (๐ผโ(๐ โ0))) | ||
Theorem | algcvg 12050* |
One way to prove that an algorithm halts is to construct a countdown
function ๐ถ:๐โถโ0 whose
value is guaranteed to decrease for
each iteration of ๐น until it reaches 0. That is, if ๐ โ ๐
is not a fixed point of ๐น, then
(๐ถโ(๐นโ๐)) < (๐ถโ๐).
If ๐ถ is a countdown function for algorithm ๐น, the sequence (๐ถโ(๐ โ๐)) reaches 0 after at most ๐ steps, where ๐ is the value of ๐ถ for the initial state ๐ด. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ๐น:๐โถ๐ & โข ๐ = seq0((๐น โ 1st ), (โ0 ร {๐ด})) & โข ๐ถ:๐โถโ0 & โข (๐ง โ ๐ โ ((๐ถโ(๐นโ๐ง)) โ 0 โ (๐ถโ(๐นโ๐ง)) < (๐ถโ๐ง))) & โข ๐ = (๐ถโ๐ด) โ โข (๐ด โ ๐ โ (๐ถโ(๐ โ๐)) = 0) | ||
Theorem | algcvgblem 12051 | Lemma for algcvgb 12052. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โ0 โง ๐ โ โ0) โ ((๐ โ 0 โ ๐ < ๐) โ ((๐ โ 0 โ ๐ < ๐) โง (๐ = 0 โ ๐ = 0)))) | ||
Theorem | algcvgb 12052 | Two ways of expressing that ๐ถ is a countdown function for algorithm ๐น. The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ๐น:๐โถ๐ & โข ๐ถ:๐โถโ0 โ โข (๐ โ ๐ โ (((๐ถโ(๐นโ๐)) โ 0 โ (๐ถโ(๐นโ๐)) < (๐ถโ๐)) โ (((๐ถโ๐) โ 0 โ (๐ถโ(๐นโ๐)) < (๐ถโ๐)) โง ((๐ถโ๐) = 0 โ (๐ถโ(๐นโ๐)) = 0)))) | ||
Theorem | algcvga 12053* | The countdown function ๐ถ remains 0 after ๐ steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ๐น:๐โถ๐ & โข ๐ = seq0((๐น โ 1st ), (โ0 ร {๐ด})) & โข ๐ถ:๐โถโ0 & โข (๐ง โ ๐ โ ((๐ถโ(๐นโ๐ง)) โ 0 โ (๐ถโ(๐นโ๐ง)) < (๐ถโ๐ง))) & โข ๐ = (๐ถโ๐ด) โ โข (๐ด โ ๐ โ (๐พ โ (โคโฅโ๐) โ (๐ถโ(๐ โ๐พ)) = 0)) | ||
Theorem | algfx 12054* | If ๐น reaches a fixed point when the countdown function ๐ถ reaches 0, ๐น remains fixed after ๐ steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ๐น:๐โถ๐ & โข ๐ = seq0((๐น โ 1st ), (โ0 ร {๐ด})) & โข ๐ถ:๐โถโ0 & โข (๐ง โ ๐ โ ((๐ถโ(๐นโ๐ง)) โ 0 โ (๐ถโ(๐นโ๐ง)) < (๐ถโ๐ง))) & โข ๐ = (๐ถโ๐ด) & โข (๐ง โ ๐ โ ((๐ถโ๐ง) = 0 โ (๐นโ๐ง) = ๐ง)) โ โข (๐ด โ ๐ โ (๐พ โ (โคโฅโ๐) โ (๐ โ๐พ) = (๐ โ๐))) | ||
Theorem | eucalgval2 12055* | The value of the step function ๐ธ for Euclid's Algorithm on an ordered pair. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) โ โข ((๐ โ โ0 โง ๐ โ โ0) โ (๐๐ธ๐) = if(๐ = 0, โจ๐, ๐โฉ, โจ๐, (๐ mod ๐)โฉ)) | ||
Theorem | eucalgval 12056* |
Euclid's Algorithm eucalg 12061 computes the greatest common divisor of two
nonnegative integers by repeatedly replacing the larger of them with its
remainder modulo the smaller until the remainder is 0.
The value of the step function ๐ธ for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) โ โข (๐ โ (โ0 ร โ0) โ (๐ธโ๐) = if((2nd โ๐) = 0, ๐, โจ(2nd โ๐), ( mod โ๐)โฉ)) | ||
Theorem | eucalgf 12057* | Domain and codomain of the step function ๐ธ for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) โ โข ๐ธ:(โ0 ร โ0)โถ(โ0 ร โ0) | ||
Theorem | eucalginv 12058* | The invariant of the step function ๐ธ for Euclid's Algorithm is the gcd operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) โ โข (๐ โ (โ0 ร โ0) โ ( gcd โ(๐ธโ๐)) = ( gcd โ๐)) | ||
Theorem | eucalglt 12059* | The second member of the state decreases with each iteration of the step function ๐ธ for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) โ โข (๐ โ (โ0 ร โ0) โ ((2nd โ(๐ธโ๐)) โ 0 โ (2nd โ(๐ธโ๐)) < (2nd โ๐))) | ||
Theorem | eucalgcvga 12060* | Once Euclid's Algorithm halts after ๐ steps, the second element of the state remains 0 . (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 29-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) & โข ๐ = seq0((๐ธ โ 1st ), (โ0 ร {๐ด})) & โข ๐ = (2nd โ๐ด) โ โข (๐ด โ (โ0 ร โ0) โ (๐พ โ (โคโฅโ๐) โ (2nd โ(๐ โ๐พ)) = 0)) | ||
Theorem | eucalg 12061* |
Euclid's Algorithm computes the greatest common divisor of two
nonnegative integers by repeatedly replacing the larger of them with its
remainder modulo the smaller until the remainder is 0. Theorem 1.15 in
[ApostolNT] p. 20.
Upon halting, the 1st member of the final state (๐ โ๐) is equal to the gcd of the values comprising the input state โจ๐, ๐โฉ. This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Paul Chapman, 31-Mar-2011.) (Proof shortened by Mario Carneiro, 29-May-2014.) |
โข ๐ธ = (๐ฅ โ โ0, ๐ฆ โ โ0 โฆ if(๐ฆ = 0, โจ๐ฅ, ๐ฆโฉ, โจ๐ฆ, (๐ฅ mod ๐ฆ)โฉ)) & โข ๐ = seq0((๐ธ โ 1st ), (โ0 ร {๐ด})) & โข ๐ด = โจ๐, ๐โฉ โ โข ((๐ โ โ0 โง ๐ โ โ0) โ (1st โ(๐ โ๐)) = (๐ gcd ๐)) | ||
According to Wikipedia ("Least common multiple", 27-Aug-2020, https://en.wikipedia.org/wiki/Least_common_multiple): "In arithmetic and number theory, the least common multiple, lowest common multiple, or smallest common multiple of two integers a and b, usually denoted by lcm(a, b), is the smallest positive integer that is divisible by both a and b. Since division of integers by zero is undefined, this definition has meaning only if a and b are both different from zero. However, some authors define lcm(a,0) as 0 for all a, which is the result of taking the lcm to be the least upper bound in the lattice of divisibility." In this section, an operation calculating the least common multiple of two integers (df-lcm 12063). The definition is valid for all integers, including negative integers and 0, obeying the above mentioned convention. | ||
Syntax | clcm 12062 | Extend the definition of a class to include the least common multiple operator. |
class lcm | ||
Definition | df-lcm 12063* | Define the lcm operator. For example, (6 lcm 9) = 18. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
โข lcm = (๐ฅ โ โค, ๐ฆ โ โค โฆ if((๐ฅ = 0 โจ ๐ฆ = 0), 0, inf({๐ โ โ โฃ (๐ฅ โฅ ๐ โง ๐ฆ โฅ ๐)}, โ, < ))) | ||
Theorem | lcmmndc 12064 | Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.) |
โข ((๐ โ โค โง ๐ โ โค) โ DECID (๐ = 0 โจ ๐ = 0)) | ||
Theorem | lcmval 12065* | Value of the lcm operator. (๐ lcm ๐) is the least common multiple of ๐ and ๐. If either ๐ or ๐ is 0, the result is defined conventionally as 0. Contrast with df-gcd 11946 and gcdval 11962. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) = if((๐ = 0 โจ ๐ = 0), 0, inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < ))) | ||
Theorem | lcmcom 12066 | The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) = (๐ lcm ๐)) | ||
Theorem | lcm0val 12067 | The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 12066 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
โข (๐ โ โค โ (๐ lcm 0) = 0) | ||
Theorem | lcmn0val 12068* | The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ (๐ = 0 โจ ๐ = 0)) โ (๐ lcm ๐) = inf({๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}, โ, < )) | ||
Theorem | lcmcllem 12069* | Lemma for lcmn0cl 12070 and dvdslcm 12071. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ (๐ = 0 โจ ๐ = 0)) โ (๐ lcm ๐) โ {๐ โ โ โฃ (๐ โฅ ๐ โง ๐ โฅ ๐)}) | ||
Theorem | lcmn0cl 12070 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข (((๐ โ โค โง ๐ โ โค) โง ยฌ (๐ = 0 โจ ๐ = 0)) โ (๐ lcm ๐) โ โ) | ||
Theorem | dvdslcm 12071 | The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ (๐ lcm ๐) โง ๐ โฅ (๐ lcm ๐))) | ||
Theorem | lcmledvds 12072 | A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
โข (((๐พ โ โ โง ๐ โ โค โง ๐ โ โค) โง ยฌ (๐ = 0 โจ ๐ = 0)) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โค ๐พ)) | ||
Theorem | lcmeq0 12073 | The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ lcm ๐) = 0 โ (๐ = 0 โจ ๐ = 0))) | ||
Theorem | lcmcl 12074 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm ๐) โ โ0) | ||
Theorem | gcddvdslcm 12075 | The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) โฅ (๐ lcm ๐)) | ||
Theorem | lcmneg 12076 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ lcm -๐) = (๐ lcm ๐)) | ||
Theorem | neglcm 12077 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ (-๐ lcm ๐) = (๐ lcm ๐)) | ||
Theorem | lcmabs 12078 | The lcm of two integers is the same as that of their absolute values. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ ((absโ๐) lcm (absโ๐)) = (๐ lcm ๐)) | ||
Theorem | lcmgcdlem 12079 | Lemma for lcmgcd 12080 and lcmdvds 12081. Prove them for positive ๐, ๐, and ๐พ. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐)) โง ((๐พ โ โ โง (๐ โฅ ๐พ โง ๐ โฅ ๐พ)) โ (๐ lcm ๐) โฅ ๐พ))) | ||
Theorem | lcmgcd 12080 |
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 (๐ gcd ๐) = 1.
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 12014; see, e.g., https://proofwiki.org/wiki/Product_of_GCD_and_LCM 12014 and https://math.stackexchange.com/a/470827 12014. 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 12067 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ lcm ๐) ยท (๐ gcd ๐)) = (absโ(๐ ยท ๐))) | ||
Theorem | lcmdvds 12081 | The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) | ||
Theorem | lcmid 12082 | The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข (๐ โ โค โ (๐ lcm ๐) = (absโ๐)) | ||
Theorem | lcm1 12083 | The lcm of an integer and 1 is the absolute value of the integer. (Contributed by AV, 23-Aug-2020.) |
โข (๐ โ โค โ (๐ lcm 1) = (absโ๐)) | ||
Theorem | lcmgcdnn 12084 | 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 ๐) ยท (๐ gcd ๐)) = (๐ ยท ๐)) | ||
Theorem | lcmgcdeq 12085 | 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 ๐) = (๐ gcd ๐) โ (absโ๐) = (absโ๐))) | ||
Theorem | lcmdvdsb 12086 | Biconditional form of lcmdvds 12081. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ lcm ๐) โฅ ๐พ)) | ||
Theorem | lcmass 12087 | 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 12088 | 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.) |
โข (3 lcm 2) = 6 | ||
Theorem | 6lcm4e12 12089 | The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020.) |
โข (6 lcm 4) = ;12 | ||
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 (๐ด gcd ๐ต) = 1. The equivalence of the definitions is shown by coprmgcdb 12090. The negation, i.e. two integers are not coprime, can be expressed either by (๐ด gcd ๐ต) โ 1, see ncoprmgcdne1b 12091, or equivalently by 1 < (๐ด gcd ๐ต), see ncoprmgcdgt1b 12092. A proof of Euclid's lemma based on coprimality is provided in coprmdvds 12094 (as opposed to Euclid's lemma for primes). | ||
Theorem | coprmgcdb 12090* | 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.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ โ โ ((๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ ๐ = 1) โ (๐ด gcd ๐ต) = 1)) | ||
Theorem | ncoprmgcdne1b 12091* | 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.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ โ (โคโฅโ2)(๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ (๐ด gcd ๐ต) โ 1)) | ||
Theorem | ncoprmgcdgt1b 12092* | 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.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (โ๐ โ (โคโฅโ2)(๐ โฅ ๐ด โง ๐ โฅ ๐ต) โ 1 < (๐ด gcd ๐ต))) | ||
Theorem | coprmdvds1 12093 | 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.) |
โข ((๐น โ โ โง ๐บ โ โ โง (๐น gcd ๐บ) = 1) โ ((๐ผ โ โ โง ๐ผ โฅ ๐น โง ๐ผ โฅ ๐บ) โ ๐ผ = 1)) | ||
Theorem | coprmdvds 12094 | 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.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ (๐ ยท ๐) โง (๐พ gcd ๐) = 1) โ ๐พ โฅ ๐)) | ||
Theorem | coprmdvds2 12095 | If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014.) |
โข (((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โง (๐ gcd ๐) = 1) โ ((๐ โฅ ๐พ โง ๐ โฅ ๐พ) โ (๐ ยท ๐) โฅ ๐พ)) | ||
Theorem | mulgcddvds 12096 | One half of rpmulgcd2 12097, which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ gcd (๐ ยท ๐)) โฅ ((๐พ gcd ๐) ยท (๐พ gcd ๐))) | ||
Theorem | rpmulgcd2 12097 | 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.) |
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) = ((๐พ gcd ๐) ยท (๐พ gcd ๐))) | ||
Theorem | qredeq 12098 | Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.) |
โข (((๐ โ โค โง ๐ โ โ โง (๐ gcd ๐) = 1) โง (๐ โ โค โง ๐ โ โ โง (๐ gcd ๐) = 1) โง (๐ / ๐) = (๐ / ๐)) โ (๐ = ๐ โง ๐ = ๐)) | ||
Theorem | qredeu 12099* | Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013.) |
โข (๐ด โ โ โ โ!๐ฅ โ (โค ร โ)(((1st โ๐ฅ) gcd (2nd โ๐ฅ)) = 1 โง ๐ด = ((1st โ๐ฅ) / (2nd โ๐ฅ)))) | ||
Theorem | rpmul 12100 | 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.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (((๐พ gcd ๐) = 1 โง (๐พ gcd ๐) = 1) โ (๐พ gcd (๐ ยท ๐)) = 1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |