Home | Intuitionistic Logic Explorer Theorem List (p. 117 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | n2dvds3 11601 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) |
Theorem | z4even 11602 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
Theorem | 4dvdseven 11603 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) |
Theorem | divalglemnn 11604* | Lemma for divalg 11610. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.) |
Theorem | divalglemqt 11605 | Lemma for divalg 11610. The case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.) |
Theorem | divalglemnqt 11606 | Lemma for divalg 11610. The case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.) |
Theorem | divalglemeunn 11607* | Lemma for divalg 11610. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
Theorem | divalglemex 11608* | Lemma for divalg 11610. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.) |
Theorem | divalglemeuneg 11609* | Lemma for divalg 11610. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
Theorem | divalg 11610* | The division algorithm (theorem). Dividing an integer by a nonzero integer produces a (unique) quotient and a unique remainder . Theorem 1.14 in [ApostolNT] p. 19. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divalgb 11611* | Express the division algorithm as stated in divalg 11610 in terms of . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | divalg2 11612* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divalgmod 11613 | The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor (compare divalg2 11612 and divalgb 11611). This demonstration theorem justifies the use of to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.) |
Theorem | divalgmodcl 11614 | The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor. Variant of divalgmod 11613. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
Theorem | modremain 11615* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
Theorem | ndvdssub 11616 | Corollary of the division algorithm. If an integer greater than divides , then it does not divide any of , ... . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ndvdsadd 11617 | Corollary of the division algorithm. If an integer greater than divides , then it does not divide any of , ... . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ndvdsp1 11618 | Special case of ndvdsadd 11617. If an integer greater than divides , it does not divide . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ndvdsi 11619 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | flodddiv4 11620 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) |
Theorem | fldivndvdslt 11621 | The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.) |
Theorem | flodddiv4lt 11622 | The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.) |
Theorem | flodddiv4t2lthalf 11623 | The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.) |
Syntax | cgcd 11624 | Extend the definition of a class to include the greatest common divisor operator. |
Definition | df-gcd 11625* | Define the operator. For example, (ex-gcd 12932). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdmndc 11626 | Decidablity lemma used in various proofs related to . (Contributed by Jim Kingdon, 12-Dec-2021.) |
DECID | ||
Theorem | zsupcllemstep 11627* | Lemma for zsupcl 11629. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zsupcllemex 11628* | Lemma for zsupcl 11629. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zsupcl 11629* | Closure of supremum for decidable integer properties. The property which defines the set we are taking the supremum of must (a) be true at (which corresponds to the nonempty condition of classical supremum theorems), (b) decidable at each value after , and (c) be false after (which corresponds to the upper bound condition found in classical supremum theorems). (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zssinfcl 11630* | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
inf inf | ||
Theorem | infssuzex 11631* | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID | ||
Theorem | infssuzledc 11632* | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID inf | ||
Theorem | infssuzcldc 11633* | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.) |
DECID inf | ||
Theorem | dvdsbnd 11634* | There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.) |
Theorem | gcdsupex 11635* | Existence of the supremum used in defining . (Contributed by Jim Kingdon, 12-Dec-2021.) |
Theorem | gcdsupcl 11636* | Closure of the supremum used in defining . A lemma for gcdval 11637 and gcdn0cl 11640. (Contributed by Jim Kingdon, 11-Dec-2021.) |
Theorem | gcdval 11637* | The value of the operator. is the greatest common divisor of and . If and are both , the result is defined conventionally as . (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.) |
Theorem | gcd0val 11638 | The value, by convention, of the operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0val 11639* | The value of the operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0cl 11640 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcddvds 11641 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdslegcd 11642 | An integer which divides both operands of the operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | nndvdslegcd 11643 | A positive integer which divides both positive operands of the operator is bounded by it. (Contributed by AV, 9-Aug-2020.) |
Theorem | gcdcl 11644 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdnncl 11645 | Closure of the operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
Theorem | gcdcld 11646 | Closure of the operator. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | gcd2n0cl 11647 | Closure of the operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
Theorem | zeqzmulgcd 11648* | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | divgcdz 11649 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | gcdf 11650 | Domain and codomain of the operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Theorem | gcdcom 11651 | The operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divgcdnn 11652 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | divgcdnnr 11653 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | gcdeq0 11654 | The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0gt0 11655 | The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcd0id 11656 | The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdid0 11657 | 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.) |
Theorem | nn0gcdid0 11658 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdneg 11659 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | neggcd 11660 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcdaddm 11661 | Adding a multiple of one operand of the operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdadd 11662 | The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014.) |
Theorem | gcdid 11663 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcd1 11664 | 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.) |
Theorem | gcdabs 11665 | The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdabs1 11666 | of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdabs2 11667 | of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | modgcd 11668 | The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | 1gcd 11669 | The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdmultipled 11670 | The greatest common divisor of a nonnegative integer and a multiple of it is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Theorem | dvdsgcdidd 11671 | The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Theorem | 6gcd4e2 11672 | The greatest common divisor of six and four is two. To calculate this gcd, a simple form of Euclid's algorithm is used: and . (Contributed by AV, 27-Aug-2020.) |
Theorem | bezoutlemnewy 11673* | Lemma for Bézout's identity. The is-bezout predicate holds for . (Contributed by Jim Kingdon, 6-Jan-2022.) |
Theorem | bezoutlemstep 11674* | Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.) |
Theorem | bezoutlemmain 11675* | Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlema 11676* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemb 11677* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemex 11678* | Lemma for Bézout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.) |
Theorem | bezoutlemzz 11679* | Lemma for Bézout's identity. Like bezoutlemex 11678 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlemaz 11680* | Lemma for Bézout's identity. Like bezoutlemzz 11679 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembz 11681* | Lemma for Bézout's identity. Like bezoutlemaz 11680 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembi 11682* | Lemma for Bézout's identity. Like bezoutlembz 11681 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlemmo 11683* | Lemma for Bézout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
Theorem | bezoutlemeu 11684* | Lemma for Bézout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
Theorem | bezoutlemle 11685* | Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both and . (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
Theorem | bezoutlemsup 11686* | Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both and . (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
Theorem | dfgcd3 11687* | Alternate definition of the operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
Theorem | bezout 11688* |
Bézout's identity: For any integers and , there are
integers such that
. This
is Metamath 100 proof #60.
The proof is constructive, in the sense that it applies the Extended Euclidian Algorithm to constuct a number which can be shown to be and which satisfies the rest of the theorem. In the presence of excluded middle, it is common to prove Bézout's identity by taking the smallest number which satisfies the Bézout condition, and showing it is the greatest common divisor. But we do not have the ability to show that number exists other than by providing a way to determine it. (Contributed by Mario Carneiro, 22-Feb-2014.) |
Theorem | dvdsgcd 11689 | 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.) |
Theorem | dvdsgcdb 11690 | Biconditional form of dvdsgcd 11689. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dfgcd2 11691* | Alternate definition of the operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
Theorem | gcdass 11692 | Associative law for operator. Theorem 1.4(b) in [ApostolNT] p. 16. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | mulgcd 11693 | Distribute multiplication by a nonnegative integer over gcd. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
Theorem | absmulgcd 11694 | Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | mulgcdr 11695 | Reverse distribution law for the operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcddiv 11696 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdmultiple 11697 | The GCD of a multiple of a number is the number itself. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdmultiplez 11698 | Extend gcdmultiple 11697 so can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdzeq 11699 | A positive integer is equal to its gcd with an integer if and only if divides . Generalization of gcdeq 11700. (Contributed by AV, 1-Jul-2020.) |
Theorem | gcdeq 11700 | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |