![]() |
Metamath
Proof Explorer Theorem List (p. 166 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gcdmultipled 16501 | 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 16502 | 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 16503 | 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 16504 | 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 16505 | 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 16506* | Lemma for bezout 16510. (Contributed by Mario Carneiro, 15-Mar-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) β β’ (π β (π΄ β 0 β (absβπ΄) β π)) | ||
Theorem | bezoutlem2 16507* | Lemma for bezout 16510. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β πΊ β π) | ||
Theorem | bezoutlem3 16508* | Lemma for bezout 16510. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (πΆ β π β πΊ β₯ πΆ)) | ||
Theorem | bezoutlem4 16509* | Lemma for bezout 16510. (Contributed by Mario Carneiro, 22-Feb-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (π΄ gcd π΅) β π) | ||
Theorem | bezout 16510* | 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 16511 | 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 16512 | Biconditional form of dvdsgcd 16511. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π gcd π))) | ||
Theorem | dfgcd2 16513* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
β’ ((π β β€ β§ π β β€) β (π· = (π gcd π) β (0 β€ π· β§ (π· β₯ π β§ π· β₯ π) β§ βπ β β€ ((π β₯ π β§ π β₯ π) β π β₯ π·)))) | ||
Theorem | gcdass 16514 | 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 16515 | 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 16516 | 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 16517 | 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 16518 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β) β§ (πΆ β₯ π΄ β§ πΆ β₯ π΅)) β ((π΄ gcd π΅) / πΆ) = ((π΄ / πΆ) gcd (π΅ / πΆ))) | ||
Theorem | gcdzeq 16519 | A positive integer π΄ is equal to its gcd with an integer π΅ if and only if π΄ divides π΅. Generalization of gcdeq 16520. (Contributed by AV, 1-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β€) β ((π΄ gcd π΅) = π΄ β π΄ β₯ π΅)) | ||
Theorem | gcdeq 16520 | π΄ 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 16521 | Unidirectional form of dvdssq 16529. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdsmulgcd 16522 | A divisibility equivalent for odmulg 19502. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΅ β β€ β§ πΆ β β€) β (π΄ β₯ (π΅ Β· πΆ) β π΄ β₯ (π΅ Β· (πΆ gcd π΄)))) | ||
Theorem | rpmulgcd 16523 | 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 16524 | 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 16525 | If π΄ and π΅ are relatively prime, then so are π΄ and π΅βπ. Originally a subproof of rppwr 16526. (Contributed by SN, 21-Aug-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β) β ((π΄ gcd π΅) = 1 β (π΄ gcd (π΅βπ)) = 1)) | ||
Theorem | rppwr 16526 | 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 16527 | 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 16528 | Lemma for dvdssq 16529. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ π β β) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdssq 16529 | 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 16530 | Partial converse to bezout 16510. 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 16531 | Converse of bezout 16510 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 16532* | 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 16533 | 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 16534 | 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 16535 |
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 16536 | 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 16537* | 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 16538* |
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 16539 | Lemma for algcvgb 16540. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β0 β§ π β β0) β ((π β 0 β π < π) β ((π β 0 β π < π) β§ (π = 0 β π = 0)))) | ||
Theorem | algcvgb 16540 | 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 16541* | The countdown function πΆ remains 0 after π steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ πΉ:πβΆπ & β’ π = seq0((πΉ β 1st ), (β0 Γ {π΄})) & β’ πΆ:πβΆβ0 & β’ (π§ β π β ((πΆβ(πΉβπ§)) β 0 β (πΆβ(πΉβπ§)) < (πΆβπ§))) & β’ π = (πΆβπ΄) β β’ (π΄ β π β (πΎ β (β€β₯βπ) β (πΆβ(π βπΎ)) = 0)) | ||
Theorem | algfx 16542* | 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 16543* | 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 16544* |
Euclid's Algorithm eucalg 16549 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 16545* | 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 16546* | 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 16547* | 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 16548* | 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 16549* |
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 16552) as well as a function mapping a set of integers to their least common multiple (df-lcmf 16553) are provided. Both definitions are valid for all integers, including negative integers and 0, obeying the above mentioned convention. It is shown by lcmfpr 16589 that the two definitions are compatible. | ||
Syntax | clcm 16550 | Extend the definition of a class to include the least common multiple operator. |
class lcm | ||
Syntax | clcmf 16551 | Extend the definition of a class to include the least common multiple function. |
class lcm | ||
Definition | df-lcm 16552* | Define the lcm operator. For example, (6 lcm 9) = 18 (ex-lcm 30255). (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
β’ lcm = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β¨ π¦ = 0), 0, inf({π β β β£ (π₯ β₯ π β§ π¦ β₯ π)}, β, < ))) | ||
Definition | df-lcmf 16553* | 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 16554* | 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 16461 and gcdval 16462. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) = if((π = 0 β¨ π = 0), 0, inf({π β β β£ (π β₯ π β§ π β₯ π)}, β, < ))) | ||
Theorem | lcmcom 16555 | The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) = (π lcm π)) | ||
Theorem | lcm0val 16556 | The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 16555 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (π β β€ β (π lcm 0) = 0) | ||
Theorem | lcmn0val 16557* | 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 16558* | Lemma for lcmn0cl 16559 and dvdslcm 16560. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β¨ π = 0)) β (π lcm π) β {π β β β£ (π β₯ π β§ π β₯ π)}) | ||
Theorem | lcmn0cl 16559 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β¨ π = 0)) β (π lcm π) β β) | ||
Theorem | dvdslcm 16560 | The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π β₯ (π lcm π) β§ π β₯ (π lcm π))) | ||
Theorem | lcmledvds 16561 | 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 16562 | The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β ((π lcm π) = 0 β (π = 0 β¨ π = 0))) | ||
Theorem | lcmcl 16563 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm π) β β0) | ||
Theorem | gcddvdslcm 16564 | The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) β₯ (π lcm π)) | ||
Theorem | lcmneg 16565 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (π lcm -π) = (π lcm π)) | ||
Theorem | neglcm 16566 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β (-π lcm π) = (π lcm π)) | ||
Theorem | lcmabs 16567 | 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 16568 | Lemma for lcmgcd 16569 and lcmdvds 16570. 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 16569 |
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 16887 or of BΓ©zout's identity bezout 16510; see e.g., https://proofwiki.org/wiki/Product_of_GCD_and_LCM 16510 and https://math.stackexchange.com/a/470827 16510. 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 16556 to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((π β β€ β§ π β β€) β ((π lcm π) Β· (π gcd π)) = (absβ(π Β· π))) | ||
Theorem | lcmdvds 16570 | The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((π β₯ πΎ β§ π β₯ πΎ) β (π lcm π) β₯ πΎ)) | ||
Theorem | lcmid 16571 | The lcm of an integer and itself is its absolute value. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β β€ β (π lcm π) = (absβπ)) | ||
Theorem | lcm1 16572 | 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 16573 | 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 16574 | 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 16575 | Biconditional form of lcmdvds 16570. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((π β₯ πΎ β§ π β₯ πΎ) β (π lcm π) β₯ πΎ)) | ||
Theorem | lcmass 16576 | 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 16577 | The least common multiple of three and two is six. In contrast to 3lcm2e6 16695, 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 16578 | The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020.) |
β’ (6 lcm 4) = ;12 | ||
Theorem | absproddvds 16579* | 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 16580* | 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 16581* | 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 16582* | 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 16583* | 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 16584 | 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 16585* | 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 16586* | 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 16587* | Lemma for lcmfn0cl 16588 and dvdslcmf 16593. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β (lcmβπ) β {π β β β£ βπ β π π β₯ π}) | ||
Theorem | lcmfn0cl 16588 | Closure of the lcm function. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin β§ 0 β π) β (lcmβπ) β β) | ||
Theorem | lcmfpr 16589 | 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 16590 | Closure of the lcm function. (Contributed by AV, 21-Aug-2020.) |
β’ ((π β β€ β§ π β Fin) β (lcmβπ) β β0) | ||
Theorem | lcmfnncl 16591 | Closure of the lcm function. (Contributed by AV, 20-Apr-2020.) |
β’ ((π β β β§ π β Fin) β (lcmβπ) β β) | ||
Theorem | lcmfeq0b 16592 | 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 16593* | 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 16594* | 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 16595* | 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 16596 | 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 16597 | The least common multiple of a singleton is its absolute value. (Contributed by AV, 22-Aug-2020.) |
β’ (π β β€ β (lcmβ{π}) = (absβπ)) | ||
Theorem | lcmftp 16598 | The least common multiple of a triple of integers is the least common multiple of the third integer and the least common multiple of the first two integers. Although there would be a shorter proof using lcmfunsn 16606, this explicit proof (not based on induction) should be kept. (Proof modification is discouraged.) (Contributed by AV, 23-Aug-2020.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β (lcmβ{π΄, π΅, πΆ}) = ((π΄ lcm π΅) lcm πΆ)) | ||
Theorem | lcmfunsnlem1 16599* | Lemma for lcmfdvds 16604 and lcmfunsnlem 16603 (Induction step part 1). (Contributed by AV, 25-Aug-2020.) |
β’ (((π§ β β€ β§ π¦ β β€ β§ π¦ β Fin) β§ (βπ β β€ (βπ β π¦ π β₯ π β (lcmβπ¦) β₯ π) β§ βπ β β€ (lcmβ(π¦ βͺ {π})) = ((lcmβπ¦) lcm π))) β βπ β β€ (βπ β (π¦ βͺ {π§})π β₯ π β (lcmβ(π¦ βͺ {π§})) β₯ π)) | ||
Theorem | lcmfunsnlem2lem1 16600* | Lemma 1 for lcmfunsnlem2 16602. (Contributed by AV, 26-Aug-2020.) |
β’ (((0 β π¦ β§ π§ β 0 β§ π β 0) β§ (π β β€ β§ ((π§ β β€ β§ π¦ β β€ β§ π¦ β Fin) β§ (βπ β β€ (βπ β π¦ π β₯ π β (lcmβπ¦) β₯ π) β§ βπ β β€ (lcmβ(π¦ βͺ {π})) = ((lcmβπ¦) lcm π))))) β βπ β β (βπ β ((π¦ βͺ {π§}) βͺ {π})π β₯ π β ((lcmβ(π¦ βͺ {π§})) lcm π) β€ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |