![]() |
Intuitionistic Logic Explorer Theorem List (p. 121 of 149) | < 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 | bezoutlemb 12001* | Lemma for BΓ©zout's identity. The is-bezout condition is satisfied by π΅. (Contributed by Jim Kingdon, 30-Dec-2021.) |
β’ (π β βπ β β€ βπ‘ β β€ π = ((π΄ Β· π ) + (π΅ Β· π‘))) & β’ (π β π΄ β β0) & β’ (π β π΅ β β0) β β’ (π β [π΅ / π]π) | ||
Theorem | bezoutlemex 12002* | 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 12003* | Lemma for BΓ©zout's identity. Like bezoutlemex 12002 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 12004* | Lemma for BΓ©zout's identity. Like bezoutlemzz 12003 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 12005* | Lemma for BΓ©zout's identity. Like bezoutlemaz 12004 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 12006* | Lemma for BΓ©zout's identity. Like bezoutlembz 12005 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 12007* | 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 12008* | 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 12009* | 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 12010* | 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 12011* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = (β©π β β0 βπ§ β β€ (π§ β₯ π β (π§ β₯ π β§ π§ β₯ π)))) | ||
Theorem | bezout 12012* |
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 12013 | 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 12014 | Biconditional form of dvdsgcd 12013. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π gcd π))) | ||
Theorem | dfgcd2 12015* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
β’ ((π β β€ β§ π β β€) β (π· = (π gcd π) β (0 β€ π· β§ (π· β₯ π β§ π· β₯ π) β§ βπ β β€ ((π β₯ π β§ π β₯ π) β π β₯ π·)))) | ||
Theorem | gcdass 12016 | 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 12017 | 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 12018 | 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 12019 | 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 12020 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β) β§ (πΆ β₯ π΄ β§ πΆ β₯ π΅)) β ((π΄ gcd π΅) / πΆ) = ((π΄ / πΆ) gcd (π΅ / πΆ))) | ||
Theorem | gcdmultiple 12021 | 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 12022 | Extend gcdmultiple 12021 so π can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π β β€) β (π gcd (π Β· π)) = π) | ||
Theorem | gcdzeq 12023 | A positive integer π΄ is equal to its gcd with an integer π΅ if and only if π΄ divides π΅. Generalization of gcdeq 12024. (Contributed by AV, 1-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β€) β ((π΄ gcd π΅) = π΄ β π΄ β₯ π΅)) | ||
Theorem | gcdeq 12024 | π΄ 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 12025 | Unidirectional form of dvdssq 12032. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdsmulgcd 12026 | 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 12027 | 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 12028 | 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 12029 | 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 12030 | 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 12031 | Lemma for dvdssq 12032. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π β β) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdssq 12032 | 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 12033 | Partial converse to bezout 12012. 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 12034 | Converse of bezout 12012 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 12035* | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
β’ ((π΄ β β β§ βπ₯ β β DECID π₯ β π΄ β§ βπ¦ π¦ β π΄) β inf(π΄, β, < ) β π΄) | ||
Theorem | nnminle 12036* | 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 12035. (Contributed by Jim Kingdon, 26-Sep-2024.) |
β’ ((π΄ β β β§ βπ₯ β β DECID π₯ β π΄ β§ π΅ β π΄) β inf(π΄, β, < ) β€ π΅) | ||
Theorem | nnwodc 12037* | 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 12038* | 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 12039* | 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 12040* | 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 12041* | 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 12042 | Lemma for ialgr0 12044. Expressing algrflemg 6231 in a form suitable for theorems such as seq3-1 10460 or seqf 10461. (Contributed by Jim Kingdon, 22-Jul-2021.) |
β’ (π β πΉ:πβΆπ) β β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(πΉ β 1st )π¦) β π) | ||
Theorem | ialgrlemconst 12043 | Lemma for ialgr0 12044. Closure of a constant function, in a form suitable for theorems such as seq3-1 10460 or seqf 10461. (Contributed by Jim Kingdon, 22-Jul-2021.) |
β’ π = (β€β₯βπ) & β’ (π β π΄ β π) β β’ ((π β§ π₯ β (β€β₯βπ)) β ((π Γ {π΄})βπ₯) β π) | ||
Theorem | ialgr0 12044 | 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 12045 |
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 12046 | 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 12047* | 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 12048* |
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 12049 | Lemma for algcvgb 12050. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β0 β§ π β β0) β ((π β 0 β π < π) β ((π β 0 β π < π) β§ (π = 0 β π = 0)))) | ||
Theorem | algcvgb 12050 | 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 12051* | The countdown function πΆ remains 0 after π steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ πΉ:πβΆπ & β’ π = seq0((πΉ β 1st ), (β0 Γ {π΄})) & β’ πΆ:πβΆβ0 & β’ (π§ β π β ((πΆβ(πΉβπ§)) β 0 β (πΆβ(πΉβπ§)) < (πΆβπ§))) & β’ π = (πΆβπ΄) β β’ (π΄ β π β (πΎ β (β€β₯βπ) β (πΆβ(π βπΎ)) = 0)) | ||
Theorem | algfx 12052* | 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 12053* | 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 12054* |
Euclid's Algorithm eucalg 12059 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 12055* | 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 12056* | 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 12057* | 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 12058* | 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 12059* |
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 12061). The definition is valid for all integers, including negative integers and 0, obeying the above mentioned convention. | ||
Syntax | clcm 12060 | Extend the definition of a class to include the least common multiple operator. |
class lcm | ||
Definition | df-lcm 12061* | 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 12062 | Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.) |
β’ ((π β β€ β§ π β β€) β DECID (π = 0 β¨ π = 0)) | ||
Theorem | lcmval 12063* | 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 11944 and gcdval 11960. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) = if((π = 0 β¨ π = 0), 0, inf({π β β β£ (π β₯ π β§ π β₯ π)}, β, < ))) | ||
Theorem | lcmcom 12064 | The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) = (π lcm π)) | ||
Theorem | lcm0val 12065 | The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 12064 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (π β β€ β (π lcm 0) = 0) | ||
Theorem | lcmn0val 12066* | 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 12067* | Lemma for lcmn0cl 12068 and dvdslcm 12069. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β¨ π = 0)) β (π lcm π) β {π β β β£ (π β₯ π β§ π β₯ π)}) | ||
Theorem | lcmn0cl 12068 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β¨ π = 0)) β (π lcm π) β β) | ||
Theorem | dvdslcm 12069 | The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π β₯ (π lcm π) β§ π β₯ (π lcm π))) | ||
Theorem | lcmledvds 12070 | 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 12071 | The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β ((π lcm π) = 0 β (π = 0 β¨ π = 0))) | ||
Theorem | lcmcl 12072 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) β β0) | ||
Theorem | gcddvdslcm 12073 | The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) β₯ (π lcm π)) | ||
Theorem | lcmneg 12074 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm -π) = (π lcm π)) | ||
Theorem | neglcm 12075 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (-π lcm π) = (π lcm π)) | ||
Theorem | lcmabs 12076 | 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 12077 | Lemma for lcmgcd 12078 and lcmdvds 12079. 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 12078 |
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 12012; see, e.g., https://proofwiki.org/wiki/Product_of_GCD_and_LCM 12012 and https://math.stackexchange.com/a/470827 12012. 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 12065 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β ((π lcm π) Β· (π gcd π)) = (absβ(π Β· π))) | ||
Theorem | lcmdvds 12079 | The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((π β₯ πΎ β§ π β₯ πΎ) β (π lcm π) β₯ πΎ)) | ||
Theorem | lcmid 12080 | The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β β€ β (π lcm π) = (absβπ)) | ||
Theorem | lcm1 12081 | 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 12082 | 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 12083 | 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 12084 | Biconditional form of lcmdvds 12079. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((π β₯ πΎ β§ π β₯ πΎ) β (π lcm π) β₯ πΎ)) | ||
Theorem | lcmass 12085 | 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 12086 | 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 12087 | 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 12088. The negation, i.e. two integers are not coprime, can be expressed either by (π΄ gcd π΅) β 1, see ncoprmgcdne1b 12089, or equivalently by 1 < (π΄ gcd π΅), see ncoprmgcdgt1b 12090. A proof of Euclid's lemma based on coprimality is provided in coprmdvds 12092 (as opposed to Euclid's lemma for primes). | ||
Theorem | coprmgcdb 12088* | 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 12089* | 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 12090* | 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 12091 | 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 12092 | 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 12093 | 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 12094 | One half of rpmulgcd2 12095, which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ gcd (π Β· π)) β₯ ((πΎ gcd π) Β· (πΎ gcd π))) | ||
Theorem | rpmulgcd2 12095 | 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 12096 | Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.) |
β’ (((π β β€ β§ π β β β§ (π gcd π) = 1) β§ (π β β€ β§ π β β β§ (π gcd π) = 1) β§ (π / π) = (π / π)) β (π = π β§ π = π)) | ||
Theorem | qredeu 12097* | Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013.) |
β’ (π΄ β β β β!π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π΄ = ((1st βπ₯) / (2nd βπ₯)))) | ||
Theorem | rpmul 12098 | 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)) | ||
Theorem | rpdvds 12099 | 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 | congr 12100* | 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 π) β βπ β β€ (π Β· π) = (π΄ β π΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |