Home | Intuitionistic Logic Explorer Theorem List (p. 109 of 114) | < 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 | divalg2 10801* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divalgmod 10802 | The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor (compare divalg2 10801 and divalgb 10800). 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 10803 | The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor. Variant of divalgmod 10802. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
Theorem | modremain 10804* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
Theorem | ndvdssub 10805 | 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 10806 | 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 10807 | Special case of ndvdsadd 10806. If an integer greater than divides , it does not divide . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ndvdsi 10808 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | flodddiv4 10809 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) |
Theorem | fldivndvdslt 10810 | 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 10811 | 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 10812 | 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 10813 | Extend the definition of a class to include the greatest common divisor operator. |
Definition | df-gcd 10814* | Define the operator. For example, (ex-gcd 11096). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdmndc 10815 | Decidablity lemma used in various proofs related to . (Contributed by Jim Kingdon, 12-Dec-2021.) |
DECID | ||
Theorem | zsupcllemstep 10816* | Lemma for zsupcl 10818. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zsupcllemex 10817* | Lemma for zsupcl 10818. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zsupcl 10818* | 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 10819* | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
inf inf | ||
Theorem | infssuzex 10820* | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID | ||
Theorem | infssuzledc 10821* | 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 10822* | 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 10823* | There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.) |
Theorem | gcdsupex 10824* | Existence of the supremum used in defining . (Contributed by Jim Kingdon, 12-Dec-2021.) |
Theorem | gcdsupcl 10825* | Closure of the supremum used in defining . A lemma for gcdval 10826 and gcdn0cl 10829. (Contributed by Jim Kingdon, 11-Dec-2021.) |
Theorem | gcdval 10826* | 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 10827 | The value, by convention, of the operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0val 10828* | The value of the operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0cl 10829 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcddvds 10830 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdslegcd 10831 | An integer which divides both operands of the operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | nndvdslegcd 10832 | A positive integer which divides both positive operands of the operator is bounded by it. (Contributed by AV, 9-Aug-2020.) |
Theorem | gcdcl 10833 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdnncl 10834 | Closure of the operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
Theorem | gcdcld 10835 | Closure of the operator. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | gcd2n0cl 10836 | Closure of the operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
Theorem | zeqzmulgcd 10837* | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | divgcdz 10838 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | gcdf 10839 | Domain and codomain of the operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Theorem | gcdcom 10840 | The operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divgcdnn 10841 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | divgcdnnr 10842 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | gcdeq0 10843 | The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0gt0 10844 | The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcd0id 10845 | The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdid0 10846 | 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 10847 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdneg 10848 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | neggcd 10849 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcdaddm 10850 | 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 10851 | 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 10852 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcd1 10853 | 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 10854 | The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdabs1 10855 | of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdabs2 10856 | of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | modgcd 10857 | The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | 1gcd 10858 | The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | 6gcd4e2 10859 | 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 10860* | Lemma for Bézout's identity. The is-bezout predicate holds for . (Contributed by Jim Kingdon, 6-Jan-2022.) |
Theorem | bezoutlemstep 10861* | 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 10862* | 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 10863* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemb 10864* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemex 10865* | 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 10866* | Lemma for Bézout's identity. Like bezoutlemex 10865 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlemaz 10867* | Lemma for Bézout's identity. Like bezoutlemzz 10866 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembz 10868* | Lemma for Bézout's identity. Like bezoutlemaz 10867 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembi 10869* | Lemma for Bézout's identity. Like bezoutlembz 10868 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 10870* | 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 10871* | 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 10872* | 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 10873* | 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 10874* | Alternate definition of the operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
Theorem | bezout 10875* |
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 10876 | 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 10877 | Biconditional form of dvdsgcd 10876. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dfgcd2 10878* | Alternate definition of the operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
Theorem | gcdass 10879 | 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 10880 | 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 10881 | Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | mulgcdr 10882 | Reverse distribution law for the operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcddiv 10883 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdmultiple 10884 | 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 10885 | Extend gcdmultiple 10884 so can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdzeq 10886 | A positive integer is equal to its gcd with an integer if and only if divides . Generalization of gcdeq 10887. (Contributed by AV, 1-Jul-2020.) |
Theorem | gcdeq 10887 | 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.) |
Theorem | dvdssqim 10888 | Unidirectional form of dvdssq 10895. (Contributed by Scott Fenton, 19-Apr-2014.) |
Theorem | dvdsmulgcd 10889 | Relationship between the order of an element and that of a multiple. (a divisibility equivalent). (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Theorem | rpmulgcd 10890 | 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.) |
Theorem | rplpwr 10891 | If and are relatively prime, then so are and . (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | rppwr 10892 | If and are relatively prime, then so are and . (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | sqgcd 10893 | Square distributes over GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dvdssqlem 10894 | Lemma for dvdssq 10895. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dvdssq 10895 | Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | bezoutr 10896 | Partial converse to bezout 10875. Existence of a linear combination does not set the GCD, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
Theorem | bezoutr1 10897 | Converse of bezout 10875 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.) |
Theorem | nn0seqcvgd 10898* | A strictly-decreasing nonnegative integer sequence with initial term reaches zero by the th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ialgrlem1st 10899 | Lemma for ialgr0 10901. Expressing algrflemg 5952 in a form suitable for theorems such as iseq1 9791 or iseqfcl 9793. (Contributed by Jim Kingdon, 22-Jul-2021.) |
Theorem | ialgrlemconst 10900 | Lemma for ialgr0 10901. Closure of a constant function, in a form suitable for theorems such as iseq1 9791 or iseqfcl 9793. (Contributed by Jim Kingdon, 22-Jul-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |