![]() |
Metamath
Proof Explorer Theorem List (p. 166 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gcdabsOLD 16501 | Obsolete version of gcdabs 16500 as of 15-Sep-2024. (Contributed by Paul Chapman, 31-Mar-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ ((π β β€ β§ π β β€) β ((absβπ) gcd (absβπ)) = (π gcd π)) | ||
Theorem | modgcd 16502 | The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β) β ((π mod π) gcd π) = (π gcd π)) | ||
Theorem | 1gcd 16503 | The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π β β€ β (1 gcd π) = 1) | ||
Theorem | gcdmultipled 16504 | The greatest common divisor of a nonnegative integer π and a multiple of it is π itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π β π β β0) & β’ (π β π β β€) β β’ (π β (π gcd (π Β· π)) = π) | ||
Theorem | gcdmultiplez 16505 | The GCD of a multiple of an integer is the integer itself. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by AV, 12-Jan-2023.) |
β’ ((π β β β§ π β β€) β (π gcd (π Β· π)) = π) | ||
Theorem | gcdmultiple 16506 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by AV, 12-Jan-2023.) |
β’ ((π β β β§ π β β) β (π gcd (π Β· π)) = π) | ||
Theorem | dvdsgcdidd 16507 | The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π β₯ π) β β’ (π β (π gcd π) = π) | ||
Theorem | 6gcd4e2 16508 | The greatest common divisor of six and four is two. To calculate this gcd, a simple form of Euclid's algorithm is used: (6 gcd 4) = ((4 + 2) gcd 4) = (2 gcd 4) and (2 gcd 4) = (2 gcd (2 + 2)) = (2 gcd 2) = 2. (Contributed by AV, 27-Aug-2020.) |
β’ (6 gcd 4) = 2 | ||
Theorem | bezoutlem1 16509* | Lemma for bezout 16513. (Contributed by Mario Carneiro, 15-Mar-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) β β’ (π β (π΄ β 0 β (absβπ΄) β π)) | ||
Theorem | bezoutlem2 16510* | Lemma for bezout 16513. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β πΊ β π) | ||
Theorem | bezoutlem3 16511* | Lemma for bezout 16513. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (πΆ β π β πΊ β₯ πΆ)) | ||
Theorem | bezoutlem4 16512* | Lemma for bezout 16513. (Contributed by Mario Carneiro, 22-Feb-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (π΄ gcd π΅) β π) | ||
Theorem | bezout 16513* | BΓ©zout's identity: For any integers π΄ and π΅, there are integers π₯, π¦ such that (π΄ gcd π΅) = π΄ Β· π₯ + π΅ Β· π¦. This is Metamath 100 proof #60. (Contributed by Mario Carneiro, 22-Feb-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β βπ₯ β β€ βπ¦ β β€ (π΄ gcd π΅) = ((π΄ Β· π₯) + (π΅ Β· π¦))) | ||
Theorem | dvdsgcd 16514 | 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 16515 | Biconditional form of dvdsgcd 16514. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π gcd π))) | ||
Theorem | dfgcd2 16516* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
β’ ((π β β€ β§ π β β€) β (π· = (π gcd π) β (0 β€ π· β§ (π· β₯ π β§ π· β₯ π) β§ βπ β β€ ((π β₯ π β§ π β₯ π) β π β₯ π·)))) | ||
Theorem | gcdass 16517 | 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 16518 | 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 16519 | 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 16520 | 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 16521 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β) β§ (πΆ β₯ π΄ β§ πΆ β₯ π΅)) β ((π΄ gcd π΅) / πΆ) = ((π΄ / πΆ) gcd (π΅ / πΆ))) | ||
Theorem | gcdzeq 16522 | A positive integer π΄ is equal to its gcd with an integer π΅ if and only if π΄ divides π΅. Generalization of gcdeq 16523. (Contributed by AV, 1-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β€) β ((π΄ gcd π΅) = π΄ β π΄ β₯ π΅)) | ||
Theorem | gcdeq 16523 | π΄ 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 16524 | Unidirectional form of dvdssq 16532. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdsmulgcd 16525 | A divisibility equivalent for odmulg 19510. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΅ β β€ β§ πΆ β β€) β (π΄ β₯ (π΅ Β· πΆ) β π΄ β₯ (π΅ Β· (πΆ gcd π΄)))) | ||
Theorem | rpmulgcd 16526 | 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 16527 | 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 | rprpwr 16528 | If π΄ and π΅ are relatively prime, then so are π΄ and π΅βπ. Originally a subproof of rppwr 16529. (Contributed by SN, 21-Aug-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β) β ((π΄ gcd π΅) = 1 β (π΄ gcd (π΅βπ)) = 1)) | ||
Theorem | rppwr 16529 | 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 16530 | 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 16531 | Lemma for dvdssq 16532. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π β β) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdssq 16532 | 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 16533 | Partial converse to bezout 16513. 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 16534 | Converse of bezout 16513 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 | nn0seqcvgd 16535* | 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 | seq1st 16536 | A sequence whose iteration function ignores the second argument is only affected by the first point of the initial value function. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ π = seqπ((πΉ β 1st ), (π Γ {π΄})) β β’ ((π β β€ β§ π΄ β π) β π = seqπ((πΉ β 1st ), {β¨π, π΄β©})) | ||
Theorem | algr0 16537 | The value of the algorithm iterator π at 0 is the initial state π΄. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
β’ π = (β€β₯βπ) & β’ π = seqπ((πΉ β 1st ), (π Γ {π΄})) & β’ (π β π β β€) & β’ (π β π΄ β π) β β’ (π β (π βπ) = π΄) | ||
Theorem | algrf 16538 |
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 16539 | The value of the algorithm iterator π at (πΎ + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ π = (β€β₯βπ) & β’ π = seqπ((πΉ β 1st ), (π Γ {π΄})) & β’ (π β π β β€) & β’ (π β π΄ β π) & β’ (π β πΉ:πβΆπ) β β’ ((π β§ πΎ β π) β (π β(πΎ + 1)) = (πΉβ(π βπΎ))) | ||
Theorem | alginv 16540* | 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 16541* |
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 16542 | Lemma for algcvgb 16543. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β0 β§ π β β0) β ((π β 0 β π < π) β ((π β 0 β π < π) β§ (π = 0 β π = 0)))) | ||
Theorem | algcvgb 16543 | 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 16544* | The countdown function πΆ remains 0 after π steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ πΉ:πβΆπ & β’ π = seq0((πΉ β 1st ), (β0 Γ {π΄})) & β’ πΆ:πβΆβ0 & β’ (π§ β π β ((πΆβ(πΉβπ§)) β 0 β (πΆβ(πΉβπ§)) < (πΆβπ§))) & β’ π = (πΆβπ΄) β β’ (π΄ β π β (πΎ β (β€β₯βπ) β (πΆβ(π βπΎ)) = 0)) | ||
Theorem | algfx 16545* | 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 16546* | 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 16547* |
Euclid's Algorithm eucalg 16552 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 16548* | 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 16549* | 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 16550* | 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 16551* | 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 16552* |
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 first 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. ... The lcm of more than two integers is also well-defined: it is the smallest positive integer hat is divisible by each of them." In this section, an operation calculating the least common multiple of two integers (df-lcm 16555) as well as a function mapping a set of integers to their least common multiple (df-lcmf 16556) are provided. Both definitions are valid for all integers, including negative integers and 0, obeying the above mentioned convention. It is shown by lcmfpr 16592 that the two definitions are compatible. | ||
Syntax | clcm 16553 | Extend the definition of a class to include the least common multiple operator. |
class lcm | ||
Syntax | clcmf 16554 | Extend the definition of a class to include the least common multiple function. |
class lcm | ||
Definition | df-lcm 16555* | Define the lcm operator. For example, (6 lcm 9) = 18 (ex-lcm 30307). (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
β’ lcm = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β¨ π¦ = 0), 0, inf({π β β β£ (π₯ β₯ π β§ π¦ β₯ π)}, β, < ))) | ||
Definition | df-lcmf 16556* | Define the lcm function on a set of integers. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.) |
β’ lcm = (π§ β π« β€ β¦ if(0 β π§, 0, inf({π β β β£ βπ β π§ π β₯ π}, β, < ))) | ||
Theorem | lcmval 16557* | 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 16464 and gcdval 16465. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) = if((π = 0 β¨ π = 0), 0, inf({π β β β£ (π β₯ π β§ π β₯ π)}, β, < ))) | ||
Theorem | lcmcom 16558 | The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) = (π lcm π)) | ||
Theorem | lcm0val 16559 | The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 16558 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (π β β€ β (π lcm 0) = 0) | ||
Theorem | lcmn0val 16560* | 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 16561* | Lemma for lcmn0cl 16562 and dvdslcm 16563. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β¨ π = 0)) β (π lcm π) β {π β β β£ (π β₯ π β§ π β₯ π)}) | ||
Theorem | lcmn0cl 16562 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β¨ π = 0)) β (π lcm π) β β) | ||
Theorem | dvdslcm 16563 | The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π β₯ (π lcm π) β§ π β₯ (π lcm π))) | ||
Theorem | lcmledvds 16564 | 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 16565 | The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β ((π lcm π) = 0 β (π = 0 β¨ π = 0))) | ||
Theorem | lcmcl 16566 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) β β0) | ||
Theorem | gcddvdslcm 16567 | The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) β₯ (π lcm π)) | ||
Theorem | lcmneg 16568 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm -π) = (π lcm π)) | ||
Theorem | neglcm 16569 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (-π lcm π) = (π lcm π)) | ||
Theorem | lcmabs 16570 | 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 16571 | Lemma for lcmgcd 16572 and lcmdvds 16573. 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 16572 |
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 1arith 16890 or of BΓ©zout's identity bezout 16513; see e.g., https://proofwiki.org/wiki/Product_of_GCD_and_LCM 16513 and https://math.stackexchange.com/a/470827 16513. 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 16559 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β ((π lcm π) Β· (π gcd π)) = (absβ(π Β· π))) | ||
Theorem | lcmdvds 16573 | The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((π β₯ πΎ β§ π β₯ πΎ) β (π lcm π) β₯ πΎ)) | ||
Theorem | lcmid 16574 | The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β β€ β (π lcm π) = (absβπ)) | ||
Theorem | lcm1 16575 | 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 16576 | 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 16577 | 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 16578 | Biconditional form of lcmdvds 16573. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((π β₯ πΎ β§ π β₯ πΎ) β (π lcm π) β₯ πΎ)) | ||
Theorem | lcmass 16579 | 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 16580 | The least common multiple of three and two is six. In contrast to 3lcm2e6 16698, this proof does not use the property of 2 and 3 being prime, therefore it is much longer. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 27-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (3 lcm 2) = 6 | ||
Theorem | 6lcm4e12 16581 | The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020.) |
β’ (6 lcm 4) = ;12 | ||
Theorem | absproddvds 16582* | The absolute value of the product of the elements of a finite subset of the integers is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020.) |
β’ (π β π β β€) & β’ (π β π β Fin) & β’ π = (absββπ§ β π π§) β β’ (π β βπ β π π β₯ π) | ||
Theorem | absprodnn 16583* | The absolute value of the product of the elements of a finite subset of the integers not containing 0 is a poitive integer. (Contributed by AV, 21-Aug-2020.) |
β’ (π β π β β€) & β’ (π β π β Fin) & β’ π = (absββπ§ β π π§) & β’ (π β 0 β π) β β’ (π β π β β) | ||
Theorem | fissn0dvds 16584* | For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β βπ β β βπ β π π β₯ π) | ||
Theorem | fissn0dvdsn0 16585* | For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β {π β β β£ βπ β π π β₯ π} β β ) | ||
Theorem | lcmfval 16586* | Value of the lcm function. (lcmβπ) is the least common multiple of the integers contained in the finite subset of integers π. If at least one of the elements of π is 0, the result is defined conventionally as 0. (Contributed by AV, 21-Apr-2020.) (Revised by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β Fin) β (lcmβπ) = if(0 β π, 0, inf({π β β β£ βπ β π π β₯ π}, β, < ))) | ||
Theorem | lcmf0val 16587 | The value, by convention, of the least common multiple for a set containing 0 is 0. (Contributed by AV, 21-Apr-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ 0 β π) β (lcmβπ) = 0) | ||
Theorem | lcmfn0val 16588* | The value of the lcm function for a set without 0. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β (lcmβπ) = inf({π β β β£ βπ β π π β₯ π}, β, < )) | ||
Theorem | lcmfnnval 16589* | The value of the lcm function for a subset of the positive integers. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.) |
β’ ((π β β β§ π β Fin) β (lcmβπ) = inf({π β β β£ βπ β π π β₯ π}, β, < )) | ||
Theorem | lcmfcllem 16590* | Lemma for lcmfn0cl 16591 and dvdslcmf 16596. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β (lcmβπ) β {π β β β£ βπ β π π β₯ π}) | ||
Theorem | lcmfn0cl 16591 | Closure of the lcm function. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β (lcmβπ) β β) | ||
Theorem | lcmfpr 16592 | The value of the lcm function for an unordered pair is the value of the lcm operator for both elements. (Contributed by AV, 22-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (lcmβ{π, π}) = (π lcm π)) | ||
Theorem | lcmfcl 16593 | Closure of the lcm function. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin) β (lcmβπ) β β0) | ||
Theorem | lcmfnncl 16594 | Closure of the lcm function. (Contributed by AV, 20-Apr-2020.) |
β’ ((π β β β§ π β Fin) β (lcmβπ) β β) | ||
Theorem | lcmfeq0b 16595 | The least common multiple of a set of integers is 0 iff at least one of its element is 0. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin) β ((lcmβπ) = 0 β 0 β π)) | ||
Theorem | dvdslcmf 16596* | The least common multiple of a set of integers is divisible by each of its elements. (Contributed by AV, 22-Aug-2020.) |
β’ ((π β β€ β§ π β Fin) β βπ₯ β π π₯ β₯ (lcmβπ)) | ||
Theorem | lcmfledvds 16597* | A positive integer which is divisible by all elements of a set of integers bounds the least common multiple of the set. (Contributed by AV, 22-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β ((πΎ β β β§ βπ β π π β₯ πΎ) β (lcmβπ) β€ πΎ)) | ||
Theorem | lcmf 16598* | Characterization of the least common multiple of a set of integers (without 0): A positiven integer is the least common multiple of a set of integers iff it divides each of the elements of the set and every integer which divides each of the elements of the set is greater than or equal to this integer. (Contributed by AV, 22-Aug-2020.) |
β’ ((πΎ β β β§ (π β β€ β§ π β Fin β§ 0 β π)) β (πΎ = (lcmβπ) β (βπ β π π β₯ πΎ β§ βπ β β (βπ β π π β₯ π β πΎ β€ π)))) | ||
Theorem | lcmf0 16599 | The least common multiple of the empty set is 1. (Contributed by AV, 22-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (lcmββ ) = 1 | ||
Theorem | lcmfsn 16600 | The least common multiple of a singleton is its absolute value. (Contributed by AV, 22-Aug-2020.) |
β’ (π β β€ β (lcmβ{π}) = (absβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |