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 | nnehalf 11601 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) |
Theorem | nn0o1gt2 11602 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) |
Theorem | nno 11603 | An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) |
Theorem | nn0o 11604 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.) |
Theorem | nn0ob 11605 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
Theorem | nn0oddm1d2 11606 | A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
Theorem | nnoddm1d2 11607 | A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
Theorem | z0even 11608 | 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
Theorem | n2dvds1 11609 | 2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | n2dvdsm1 11610 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
Theorem | z2even 11611 | 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
Theorem | n2dvds3 11612 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) |
Theorem | z4even 11613 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
Theorem | 4dvdseven 11614 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) |
Theorem | divalglemnn 11615* | Lemma for divalg 11621. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.) |
Theorem | divalglemqt 11616 | Lemma for divalg 11621. The case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.) |
Theorem | divalglemnqt 11617 | Lemma for divalg 11621. The case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.) |
Theorem | divalglemeunn 11618* | Lemma for divalg 11621. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
Theorem | divalglemex 11619* | Lemma for divalg 11621. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.) |
Theorem | divalglemeuneg 11620* | Lemma for divalg 11621. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
Theorem | divalg 11621* | 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 11622* | Express the division algorithm as stated in divalg 11621 in terms of . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | divalg2 11623* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divalgmod 11624 | The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor (compare divalg2 11623 and divalgb 11622). 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 11625 | The result of the operator satisfies the requirements for the remainder in the division algorithm for a positive divisor. Variant of divalgmod 11624. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
Theorem | modremain 11626* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
Theorem | ndvdssub 11627 | 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 11628 | 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 11629 | Special case of ndvdsadd 11628. If an integer greater than divides , it does not divide . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ndvdsi 11630 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | flodddiv4 11631 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) |
Theorem | fldivndvdslt 11632 | 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 11633 | 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 11634 | 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 11635 | Extend the definition of a class to include the greatest common divisor operator. |
Definition | df-gcd 11636* | Define the operator. For example, (ex-gcd 12943). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdmndc 11637 | Decidablity lemma used in various proofs related to . (Contributed by Jim Kingdon, 12-Dec-2021.) |
DECID | ||
Theorem | zsupcllemstep 11638* | Lemma for zsupcl 11640. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zsupcllemex 11639* | Lemma for zsupcl 11640. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
DECID | ||
Theorem | zsupcl 11640* | 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 11641* | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
inf inf | ||
Theorem | infssuzex 11642* | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
DECID | ||
Theorem | infssuzledc 11643* | 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 11644* | 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 11645* | There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.) |
Theorem | gcdsupex 11646* | Existence of the supremum used in defining . (Contributed by Jim Kingdon, 12-Dec-2021.) |
Theorem | gcdsupcl 11647* | Closure of the supremum used in defining . A lemma for gcdval 11648 and gcdn0cl 11651. (Contributed by Jim Kingdon, 11-Dec-2021.) |
Theorem | gcdval 11648* | 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 11649 | The value, by convention, of the operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0val 11650* | The value of the operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0cl 11651 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcddvds 11652 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdslegcd 11653 | An integer which divides both operands of the operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | nndvdslegcd 11654 | A positive integer which divides both positive operands of the operator is bounded by it. (Contributed by AV, 9-Aug-2020.) |
Theorem | gcdcl 11655 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdnncl 11656 | Closure of the operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
Theorem | gcdcld 11657 | Closure of the operator. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | gcd2n0cl 11658 | Closure of the operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
Theorem | zeqzmulgcd 11659* | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | divgcdz 11660 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | gcdf 11661 | Domain and codomain of the operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Theorem | gcdcom 11662 | The operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divgcdnn 11663 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | divgcdnnr 11664 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | gcdeq0 11665 | The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0gt0 11666 | The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcd0id 11667 | The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdid0 11668 | 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 11669 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdneg 11670 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | neggcd 11671 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcdaddm 11672 | 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 11673 | 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 11674 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcd1 11675 | 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 11676 | The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdabs1 11677 | of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdabs2 11678 | of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | modgcd 11679 | The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | 1gcd 11680 | 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 11681 | The greatest common divisor of a nonnegative integer and a multiple of it is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Theorem | dvdsgcdidd 11682 | The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
Theorem | 6gcd4e2 11683 | 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 11684* | Lemma for Bézout's identity. The is-bezout predicate holds for . (Contributed by Jim Kingdon, 6-Jan-2022.) |
Theorem | bezoutlemstep 11685* | 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 11686* | 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 11687* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemb 11688* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemex 11689* | 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 11690* | Lemma for Bézout's identity. Like bezoutlemex 11689 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlemaz 11691* | Lemma for Bézout's identity. Like bezoutlemzz 11690 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembz 11692* | Lemma for Bézout's identity. Like bezoutlemaz 11691 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembi 11693* | Lemma for Bézout's identity. Like bezoutlembz 11692 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 11694* | 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 11695* | 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 11696* | 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 11697* | 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 11698* | Alternate definition of the operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
Theorem | bezout 11699* |
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 11700 | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |