![]() |
Metamath
Proof Explorer Theorem List (p. 165 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sadval 16401* | The full adder sequence is the half adder function applied to the inputs and the carry sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ sadd π΅) β hadd(π β π΄, π β π΅, β β (πΆβπ)))) | ||
Theorem | sadcaddlem 16402* | Lemma for sadcadd 16403. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ πΎ = β‘(bits βΎ β0) & β’ (π β (β β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β β’ (π β (β β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))) | ||
Theorem | sadcadd 16403* | Non-recursive definition of the carry sequence. (Contributed by Mario Carneiro, 8-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ πΎ = β‘(bits βΎ β0) β β’ (π β (β β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) | ||
Theorem | sadadd2lem 16404* | Lemma for sadadd2 16405. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) & β’ πΎ = β‘(bits βΎ β0) & β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^π))) + if(β β (πΆβπ), (2βπ), 0)) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β β’ (π β ((πΎβ((π΄ sadd π΅) β© (0..^(π + 1)))) + if(β β (πΆβ(π + 1)), (2β(π + 1)), 0)) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))) | ||
Theorem | sadadd2 16405* | 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 16406* | 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 16407 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) β β0) | ||
Theorem | sadcom 16408 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ sadd π΅) = (π΅ sadd π΄)) | ||
Theorem | saddisjlem 16409* | Lemma for sadadd 16412. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β (π΄ β© π΅) = β ) & β’ πΆ = seq0((π β 2o, π β β0 β¦ if(cadd(π β π΄, π β π΅, β β π), 1o, β )), (π β β0 β¦ if(π = 0, β , (π β 1)))) & β’ (π β π β β0) β β’ (π β (π β (π΄ sadd π΅) β π β (π΄ βͺ π΅))) | ||
Theorem | saddisj 16410 | 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 16411* | Lemma for sadadd 16412. (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 16412 |
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 1593 and df-cad 1606.
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 16413 | 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 16414 | 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 16415 | Lemma for sadass 16416. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β πΆ β β0) & β’ (π β π β β0) β β’ (π β (((π΄ sadd π΅) sadd πΆ) β© (0..^π)) = ((π΄ sadd (π΅ sadd πΆ)) β© (0..^π))) | ||
Theorem | sadass 16416 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0 β§ πΆ β β0) β ((π΄ sadd π΅) sadd πΆ) = (π΄ sadd (π΅ sadd πΆ))) | ||
Theorem | sadeq 16417 | 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 16418 | 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 16419 | 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 16420* | 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 16421* | 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 16422* | 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 16423* | 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 16424* | 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 16425* | 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 16426* | Define the addition of two bit sequences, using df-had 1593 and df-cad 1606 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 16427* | 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 16428* | 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 16429 | The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ smul π΅) β β0) | ||
Theorem | smu01lem 16430* | Lemma for smu01 16431 and smu02 16432. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ ((π β§ (π β β0 β§ π β β0)) β Β¬ (π β π΄ β§ (π β π) β π΅)) β β’ (π β (π΄ smul π΅) = β ) | ||
Theorem | smu01 16431 | Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016.) |
β’ (π΄ β β0 β (π΄ smul β ) = β ) | ||
Theorem | smu02 16432 | Multiplication of a sequence by 0 on the left. (Contributed by Mario Carneiro, 9-Sep-2016.) |
β’ (π΄ β β0 β (β smul π΄) = β ) | ||
Theorem | smupval 16433* | 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 16434* | Rewrite smupp1 16425 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 16435* | 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 16436 | 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 16437 | Lemma for smumul 16438. (Contributed by Mario Carneiro, 22-Sep-2016.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ (π β π β β0) β β’ (π β (((bitsβπ΄) β© (0..^π)) smul (bitsβπ΅)) = (bitsβ((π΄ mod (2βπ)) Β· π΅))) | ||
Theorem | smumul 16438 |
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 16396, whose correctness is
verified in sadadd 16412.
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 16439 | Extend the definition of a class to include the greatest common divisor operator. |
class gcd | ||
Definition | df-gcd 16440* | Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 29977). For an alternate definition, based on the definition in [ApostolNT] p. 15, see dfgcd2 16492. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ gcd = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β§ π¦ = 0), 0, sup({π β β€ β£ (π β₯ π₯ β§ π β₯ π¦)}, β, < ))) | ||
Theorem | gcdval 16441* | 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 16442 | 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 16443* | 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 16444* | Lemma for gcdn0cl 16447, gcddvds 16448 and dvdslegcd 16449. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π = {π§ β β€ β£ βπ β π΄ π§ β₯ π} β β’ ((π΄ β β€ β§ βπ β π΄ π β 0) β (π β β β§ βπ₯ β β€ βπ¦ β π π¦ β€ π₯)) | ||
Theorem | gcdcllem2 16445* | Lemma for gcdn0cl 16447, gcddvds 16448 and dvdslegcd 16449. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π = {π§ β β€ β£ βπ β {π, π}π§ β₯ π} & β’ π = {π§ β β€ β£ (π§ β₯ π β§ π§ β₯ π)} β β’ ((π β β€ β§ π β β€) β π = π) | ||
Theorem | gcdcllem3 16446* | Lemma for gcdn0cl 16447, gcddvds 16448 and dvdslegcd 16449. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π = {π§ β β€ β£ βπ β {π, π}π§ β₯ π} & β’ π = {π§ β β€ β£ (π§ β₯ π β§ π§ β₯ π)} β β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β (sup(π , β, < ) β β β§ (sup(π , β, < ) β₯ π β§ sup(π , β, < ) β₯ π) β§ ((πΎ β β€ β§ πΎ β₯ π β§ πΎ β₯ π) β πΎ β€ sup(π , β, < )))) | ||
Theorem | gcdn0cl 16447 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β (π gcd π) β β) | ||
Theorem | gcddvds 16448 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) | ||
Theorem | dvdslegcd 16449 | 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 16450 | 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 16451 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) β β0) | ||
Theorem | gcdnncl 16452 | Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
β’ ((π β β β§ π β β) β (π gcd π) β β) | ||
Theorem | gcdcld 16453 | Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π gcd π) β β0) | ||
Theorem | gcd2n0cl 16454 | Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π gcd π) β β) | ||
Theorem | zeqzmulgcd 16455* | 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 16456 | 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 16457 | 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 16458 | The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π gcd π) = (π gcd π)) | ||
Theorem | gcdcomd 16459 | The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
β’ (π β π β β€) & β’ (π β π β β€) β β’ (π β (π gcd π) = (π gcd π)) | ||
Theorem | divgcdnn 16460 | 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 16461 | 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 16462 | 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 16463 | 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 16464 | 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 16465 | 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 16466 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ (π β β0 β (π gcd 0) = π) | ||
Theorem | gcdneg 16467 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π gcd -π) = (π gcd π)) | ||
Theorem | neggcd 16468 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ ((π β β€ β§ π β β€) β (-π gcd π) = (π gcd π)) | ||
Theorem | gcdaddmlem 16469 | Lemma for gcdaddm 16470. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ πΎ β β€ & β’ π β β€ & β’ π β β€ β β’ (π gcd π) = (π gcd ((πΎ Β· π) + π)) | ||
Theorem | gcdaddm 16470 | 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 16471 | 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 16472 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ (π β β€ β (π gcd π) = (absβπ)) | ||
Theorem | gcd1 16473 | 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 16474 | 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 16475 | 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 16476 | 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 16477 | Obsolete version of gcdabs 16476 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 16478 | 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 16479 | 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 16480 | 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 16481 | 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 16482 | 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 16483 | 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 16484 | 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 16485* | Lemma for bezout 16489. (Contributed by Mario Carneiro, 15-Mar-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) β β’ (π β (π΄ β 0 β (absβπ΄) β π)) | ||
Theorem | bezoutlem2 16486* | Lemma for bezout 16489. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β πΊ β π) | ||
Theorem | bezoutlem3 16487* | Lemma for bezout 16489. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (πΆ β π β πΊ β₯ πΆ)) | ||
Theorem | bezoutlem4 16488* | Lemma for bezout 16489. (Contributed by Mario Carneiro, 22-Feb-2014.) |
β’ π = {π§ β β β£ βπ₯ β β€ βπ¦ β β€ π§ = ((π΄ Β· π₯) + (π΅ Β· π¦))} & β’ (π β π΄ β β€) & β’ (π β π΅ β β€) & β’ πΊ = inf(π, β, < ) & β’ (π β Β¬ (π΄ = 0 β§ π΅ = 0)) β β’ (π β (π΄ gcd π΅) β π) | ||
Theorem | bezout 16489* | 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 16490 | 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 16491 | Biconditional form of dvdsgcd 16490. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π gcd π))) | ||
Theorem | dfgcd2 16492* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
β’ ((π β β€ β§ π β β€) β (π· = (π gcd π) β (0 β€ π· β§ (π· β₯ π β§ π· β₯ π) β§ βπ β β€ ((π β₯ π β§ π β₯ π) β π β₯ π·)))) | ||
Theorem | gcdass 16493 | 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 16494 | 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 16495 | 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 16496 | 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 16497 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β) β§ (πΆ β₯ π΄ β§ πΆ β₯ π΅)) β ((π΄ gcd π΅) / πΆ) = ((π΄ / πΆ) gcd (π΅ / πΆ))) | ||
Theorem | gcdzeq 16498 | A positive integer π΄ is equal to its gcd with an integer π΅ if and only if π΄ divides π΅. Generalization of gcdeq 16499. (Contributed by AV, 1-Jul-2020.) |
β’ ((π΄ β β β§ π΅ β β€) β ((π΄ gcd π΅) = π΄ β π΄ β₯ π΅)) | ||
Theorem | gcdeq 16499 | π΄ 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 16500 | Unidirectional form of dvdssq 16508. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (πβ2) β₯ (πβ2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |