![]() |
Metamath
Proof Explorer Theorem List (p. 165 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sadadd2 16401* | Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ πΎ = β‘(bits βΎ β0) β β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) | ||
Theorem | sadadd3 16402* | Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ πΎ = β‘(bits βΎ β0) β β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) mod (2βπ)) = (((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))) mod (2βπ))) | ||
Theorem | sadcl 16403 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) β β0) | ||
Theorem | sadcom 16404 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) = (π΅ sadd π΄)) | ||
Theorem | saddisjlem 16405* | Lemma for sadadd 16408. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β (π΄ β© π΅) = β ) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ sadd π΅) β π β (π΄ βͺ π΅))) | ||
Theorem | saddisj 16406 | The sum of disjoint sequences is the union of the sequences. (In this case, there are no carried bits.) (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β (π΄ β© π΅) = β ) β β’ (π β (π΄ sadd π΅) = (π΄ βͺ π΅)) | ||
Theorem | sadaddlem 16407* | Lemma for sadadd 16408. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β (bitsβπ΄), π β (bitsβπ΅), β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ πΎ = β‘(bits βΎ β0) & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) β β’ (π β (((bitsβπ΄) sadd (bitsβπ΅)) β© (0..^π)) = (bitsβ((π΄ + π΅) mod (2βπ)))) | ||
Theorem | sadadd 16408 |
For sequences that correspond to valid integers, the adder sequence
function produces the sequence for the sum. This is effectively a proof
of the correctness of the ripple carry adder, implemented with logic
gates corresponding to df-had 1596 and df-cad 1609.
It is interesting to consider in what sense the sadd function can be said to be "adding" things outside the range of the bits function, that is, when adding sequences that are not eventually constant and so do not denote any integer. The correct interpretation is that the sequences are representations of 2-adic integers, which have a natural ring structure. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((bitsβπ΄) sadd (bitsβπ΅)) = (bitsβ(π΄ + π΅))) | ||
Theorem | sadid1 16409 | The adder sequence function has a left identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π΄ β β0 β (π΄ sadd β ) = π΄) | ||
Theorem | sadid2 16410 | The adder sequence function has a right identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π΄ β β0 β (β sadd π΄) = π΄) | ||
Theorem | sadasslem 16411 | Lemma for sadass 16412. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β πΆ β β0) & β’ (π β π β β0) β β’ (π β (((π΄ sadd π΅) sadd πΆ) β© (0..^π)) = ((π΄ sadd (π΅ sadd πΆ)) β© (0..^π))) | ||
Theorem | sadass 16412 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ πΆ β β0) β ((π΄ sadd π΅) sadd πΆ) = (π΄ sadd (π΅ sadd πΆ))) | ||
Theorem | sadeq 16413 | Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β0) β β’ (π β ((π΄ sadd π΅) β© (0..^π)) = (((π΄ β© (0..^π)) sadd (π΅ β© (0..^π))) β© (0..^π))) | ||
Theorem | bitsres 16414 | Restrict the bits of a number to an upper integer set. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β€ β§ π β β0) β ((bitsβπ΄) β© (β€β₯βπ)) = (bitsβ((ββ(π΄ / (2βπ))) Β· (2βπ)))) | ||
Theorem | bitsuz 16415 | The bits of a number are all at least π iff the number is divisible by 2βπ. (Contributed by Mario Carneiro, 21-Sep-2016.) |
β’ ((π΄ β β€ β§ π β β0) β ((2βπ) β₯ π΄ β (bitsβπ΄) β (β€β₯βπ))) | ||
Theorem | bitsshft 16416* | Shifting a bit sequence to the left (toward the more significant bits) causes the number to be multiplied by a power of two. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ ((π΄ β β€ β§ π β β0) β {π β β0 β£ (π β π) β (bitsβπ΄)} = (bitsβ(π΄ Β· (2βπ)))) | ||
Definition | df-smu 16417* | Define the multiplication of two bit sequences, using repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ smul = (π₯ β π« β0, π¦ β π« β0 β¦ {π β β0 β£ π β (seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π₯ β§ (π β π) β π¦)})), (π β β0 β¦ if(π = 0, β , (π β 1))))β(π + 1))}) | ||
Theorem | smufval 16418* | The multiplication of two bit sequences as repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β (π΄ smul π΅) = {π β β0 β£ π β (πβ(π + 1))}) | ||
Theorem | smupf 16419* | The sequence of partial sums of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β π:β0βΆπ« β0) | ||
Theorem | smup0 16420* | The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β (πβ0) = β ) | ||
Theorem | smupp1 16421* | The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (πβ(π + 1)) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) | ||
Theorem | smuval 16422* | Define the addition of two bit sequences, using df-had 1596 and df-cad 1609 bit operations. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ smul π΅) β π β (πβ(π + 1)))) | ||
Theorem | smuval2 16423* | The partial sum sequence stabilizes at π after the π + 1-th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ (π β π β (β€β₯β(π + 1))) β β’ (π β (π β (π΄ smul π΅) β π β (πβπ))) | ||
Theorem | smupvallem 16424* | If π΄ only has elements less than π, then all elements of the partial sum sequence past π already equal the final value. (Contributed by Mario Carneiro, 20-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ (π β π΄ β (0..^π)) & β’ (π β π β (β€β₯βπ)) β β’ (π β (πβπ) = (π΄ smul π΅)) | ||
Theorem | smucl 16425 | The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ smul π΅) β β0) | ||
Theorem | smu01lem 16426* | Lemma for smu01 16427 and smu02 16428. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ ((π β§ (π β β0 β§ π β β0)) β Β¬ (π β π΄ β§ (π β π) β π΅)) β β’ (π β (π΄ smul π΅) = β ) | ||
Theorem | smu01 16427 | Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π΄ β β0 β (π΄ smul β ) = β ) | ||
Theorem | smu02 16428 | Multiplication of a sequence by 0 on the left. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π΄ β β0 β (β smul π΄) = β ) | ||
Theorem | smupval 16429* | Rewrite the elements of the partial sum sequence in terms of sequence multiplication. (Contributed by Mario Carneiro, 20-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (πβπ) = ((π΄ β© (0..^π)) smul π΅)) | ||
Theorem | smup1 16430* | Rewrite smupp1 16421 using only smul instead of the internal recursive function π. (Contributed by Mario Carneiro, 20-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β0) β β’ (π β ((π΄ β© (0..^(π + 1))) smul π΅) = (((π΄ β© (0..^π)) smul π΅) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) | ||
Theorem | smueqlem 16431* | Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β0) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ π = seq0((π β π« β0, π β β0 β¦ (π sadd {π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))})), (π β β0 β¦ if(π = 0, β , (π β 1)))) β β’ (π β ((π΄ smul π΅) β© (0..^π)) = (((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β© (0..^π))) | ||
Theorem | smueq 16432 | Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β0) β β’ (π β ((π΄ smul π΅) β© (0..^π)) = (((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β© (0..^π))) | ||
Theorem | smumullem 16433 | Lemma for smumul 16434. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) β β’ (π β (((bitsβπ΄) β© (0..^π)) smul (bitsβπ΅)) = (bitsβ((π΄ mod (2βπ)) Β· π΅))) | ||
Theorem | smumul 16434 |
For sequences that correspond to valid integers, the sequence
multiplication function produces the sequence for the product. This is
effectively a proof of the correctness of the multiplication process,
implemented in terms of logic gates for df-sad 16392, whose correctness is
verified in sadadd 16408.
Outside this range, the sequences cannot be representing integers, but the smul function still "works". This extended function is best interpreted in terms of the ring structure of the 2-adic integers. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((bitsβπ΄) smul (bitsβπ΅)) = (bitsβ(π΄ Β· π΅))) | ||
Syntax | cgcd 16435 | Extend the definition of a class to include the greatest common divisor operator. |
class gcd | ||
Definition | df-gcd 16436* | Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 29710). For an alternate definition, based on the definition in [ApostolNT] p. 15, see dfgcd2 16488. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ gcd = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β§ π¦ = 0), 0, sup({π β β€ β£ (π β₯ π₯ β§ π β₯ π¦)}, β, < ))) | ||
Theorem | gcdval 16437* | The value of the gcd operator. (π gcd π) is the greatest common divisor of π and π. If π and π are both 0, the result is defined conventionally as 0. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = if((π = 0 β§ π = 0), 0, sup({π β β€ β£ (π β₯ π β§ π β₯ π)}, β, < ))) | ||
Theorem | gcd0val 16438 | The value, by convention, of the gcd operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (0 gcd 0) = 0 | ||
Theorem | gcdn0val 16439* | The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β (π gcd π) = sup({π β β€ β£ (π β₯ π β§ π β₯ π)}, β, < )) | ||
Theorem | gcdcllem1 16440* | Lemma for gcdn0cl 16443, gcddvds 16444 and dvdslegcd 16445. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π = {π§ β β€ β£ βπ β π΄ π§ β₯ π} β β’ ((π΄ β β€ β§ βπ β π΄ π β 0) β (π β β β§ βπ₯ β β€ βπ¦ β π π¦ β€ π₯)) | ||
Theorem | gcdcllem2 16441* | Lemma for gcdn0cl 16443, gcddvds 16444 and dvdslegcd 16445. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π = {π§ β β€ β£ βπ β {π, π}π§ β₯ π} & β’ π = {π§ β β€ β£ (π§ β₯ π β§ π§ β₯ π)} β β’ ((π β β€ β§ π β β€) β π = π) | ||
Theorem | gcdcllem3 16442* | Lemma for gcdn0cl 16443, gcddvds 16444 and dvdslegcd 16445. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π = {π§ β β€ β£ βπ β {π, π}π§ β₯ π} & β’ π = {π§ β β€ β£ (π§ β₯ π β§ π§ β₯ π)} β β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β (sup(π , β, < ) β β β§ (sup(π , β, < ) β₯ π β§ sup(π , β, < ) β₯ π) β§ ((πΎ β β€ β§ πΎ β₯ π β§ πΎ β₯ π) β πΎ β€ sup(π , β, < )))) | ||
Theorem | gcdn0cl 16443 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β (π gcd π) β β) | ||
Theorem | gcddvds 16444 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) | ||
Theorem | dvdslegcd 16445 | An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β€ (π gcd π))) | ||
Theorem | nndvdslegcd 16446 | A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020.) |
β’ ((πΎ β β β§ π β β β§ π β β) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β€ (π gcd π))) | ||
Theorem | gcdcl 16447 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) β β0) | ||
Theorem | gcdnncl 16448 | Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
β’ ((π β β β§ π β β) β (π gcd π) β β) | ||
Theorem | gcdcld 16449 | Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π gcd π) β β0) | ||
Theorem | gcd2n0cl 16450 | Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π gcd π) β β) | ||
Theorem | zeqzmulgcd 16451* | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β€) β βπ β β€ π΄ = (π Β· (π΄ gcd π΅))) | ||
Theorem | divgcdz 16452 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π΅ β 0) β (π΄ / (π΄ gcd π΅)) β β€) | ||
Theorem | gcdf 16453 | Domain and codomain of the gcd operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.) |
β’ gcd :(β€ Γ β€)βΆβ0 | ||
Theorem | gcdcom 16454 | The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = (π gcd π)) | ||
Theorem | gcdcomd 16455 | The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π gcd π) = (π gcd π)) | ||
Theorem | divgcdnn 16456 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
β’ ((π΄ β β β§ π΅ β β€) β (π΄ / (π΄ gcd π΅)) β β) | ||
Theorem | divgcdnnr 16457 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
β’ ((π΄ β β β§ π΅ β β€) β (π΄ / (π΅ gcd π΄)) β β) | ||
Theorem | gcdeq0 16458 | The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β ((π gcd π) = 0 β (π = 0 β§ π = 0))) | ||
Theorem | gcdn0gt0 16459 | The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ ((π β β€ β§ π β β€) β (Β¬ (π = 0 β§ π = 0) β 0 < (π gcd π))) | ||
Theorem | gcd0id 16460 | The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β (0 gcd π) = (absβπ)) | ||
Theorem | gcdid0 16461 | The gcd of an integer and 0 is the integer's absolute value. Theorem 1.4(d)2 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ (π β β€ β (π gcd 0) = (absβπ)) | ||
Theorem | nn0gcdid0 16462 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ (π β β0 β (π gcd 0) = π) | ||
Theorem | gcdneg 16463 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π gcd -π) = (π gcd π)) | ||
Theorem | neggcd 16464 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ ((π β β€ β§ π β β€) β (-π gcd π) = (π gcd π)) | ||
Theorem | gcdaddmlem 16465 | Lemma for gcdaddm 16466. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ πΎ β β€ & β’ π β β€ & β’ π β β€ β β’ (π gcd π) = (π gcd ((πΎ Β· π) + π)) | ||
Theorem | gcdaddm 16466 | Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (π gcd π) = (π gcd (π + (πΎ Β· π)))) | ||
Theorem | gcdadd 16467 | The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = (π gcd (π + π))) | ||
Theorem | gcdid 16468 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ (π β β€ β (π gcd π) = (absβπ)) | ||
Theorem | gcd1 16469 | The gcd of a number with 1 is 1. Theorem 1.4(d)1 in [ApostolNT] p. 16. (Contributed by Mario Carneiro, 19-Feb-2014.) |
β’ (π β β€ β (π gcd 1) = 1) | ||
Theorem | gcdabs1 16470 | gcd of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β ((absβπ) gcd π) = (π gcd π)) | ||
Theorem | gcdabs2 16471 | gcd of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π gcd (absβπ)) = (π gcd π)) | ||
Theorem | gcdabs 16472 | The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) (Proof shortened by SN, 15-Sep-2024.) |
β’ ((π β β€ β§ π β β€) β ((absβπ) gcd (absβπ)) = (π gcd π)) | ||
Theorem | gcdabsOLD 16473 | Obsolete version of gcdabs 16472 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 16474 | 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 16475 | 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 16476 | 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 16477 | 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 16478 | 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 16479 | 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 16480 | 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 16481* | Lemma for bezout 16485. (Contributed by Mario Carneiro, 15-Mar-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) β β’ (π β (π΄ β 0 β (absβπ΄) β π)) | ||
Theorem | bezoutlem2 16482* | Lemma for bezout 16485. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β πΊ β π) | ||
Theorem | bezoutlem3 16483* | Lemma for bezout 16485. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (πΆ β π β πΊ β₯ πΆ)) | ||
Theorem | bezoutlem4 16484* | Lemma for bezout 16485. (Contributed by Mario Carneiro, 22-Feb-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (π΄ gcd π΅) β π) | ||
Theorem | bezout 16485* | 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 16486 | 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 16487 | Biconditional form of dvdsgcd 16486. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π gcd π))) | ||
Theorem | dfgcd2 16488* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
β’ ((π β β€ β§ π β β€) β (π· = (π gcd π) β (0 β€ π· β§ (π· β₯ π β§ π· β₯ π) β§ βπ β β€ ((π β₯ π β§ π β₯ π) β π β₯ π·)))) | ||
Theorem | gcdass 16489 | 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 16490 | 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 16491 | 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 16492 | 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 16493 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β) β§ (πΆ β₯ π΄ β§ πΆ β₯ π΅)) β ((π΄ gcd π΅) / πΆ) = ((π΄ / πΆ) gcd (π΅ / πΆ))) | ||
Theorem | gcdzeq 16494 | A positive integer π΄ is equal to its gcd with an integer π΅ if and only if π΄ divides π΅. Generalization of gcdeq 16495. (Contributed by AV, 1-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β€) β ((π΄ gcd π΅) = π΄ β π΄ β₯ π΅)) | ||
Theorem | gcdeq 16495 | π΄ 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 16496 | Unidirectional form of dvdssq 16504. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (πβ2) β₯ (πβ2))) | ||
Theorem | dvdsmulgcd 16497 | A divisibility equivalent for odmulg 19424. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΅ β β€ β§ πΆ β β€) β (π΄ β₯ (π΅ Β· πΆ) β π΄ β₯ (π΅ Β· (πΆ gcd π΄)))) | ||
Theorem | rpmulgcd 16498 | 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 16499 | 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 16500 | If π΄ and π΅ are relatively prime, then so are π΄ and π΅βπ. Originally a subproof of rppwr 16501. (Contributed by SN, 21-Aug-2024.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β) β ((π΄ gcd π΅) = 1 β (π΄ gcd (π΅βπ)) = 1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |