Home | Intuitionistic Logic Explorer Theorem List (p. 106 of 110) | < 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 | nndvdslegcd 10501 | A positive integer which divides both positive operands of the operator is bounded by it. (Contributed by AV, 9-Aug-2020.) |
Theorem | gcdcl 10502 | Closure of the operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdnncl 10503 | Closure of the operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
Theorem | gcdcld 10504 | Closure of the operator. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | gcd2n0cl 10505 | Closure of the operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
Theorem | zeqzmulgcd 10506* | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | divgcdz 10507 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
Theorem | gcdf 10508 | Domain and codomain of the operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.) |
Theorem | gcdcom 10509 | The operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divgcdnn 10510 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | divgcdnnr 10511 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
Theorem | gcdeq0 10512 | The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdn0gt0 10513 | The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcd0id 10514 | The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | gcdid0 10515 | 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 10516 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdneg 10517 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | neggcd 10518 | Negating one operand of the operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | gcdaddm 10519 | 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 10520 | 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 10521 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcd1 10522 | 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 10523 | The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | gcdabs1 10524 | of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdabs2 10525 | of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | modgcd 10526 | The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | 1gcd 10527 | 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 10528 | 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 10529* | Lemma for Bézout's identity. The is-bezout predicate holds for . (Contributed by Jim Kingdon, 6-Jan-2022.) |
Theorem | bezoutlemstep 10530* | 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 10531* | 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 10532* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemb 10533* | Lemma for Bézout's identity. The is-bezout condition is satisfied by . (Contributed by Jim Kingdon, 30-Dec-2021.) |
Theorem | bezoutlemex 10534* | 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 10535* | Lemma for Bézout's identity. Like bezoutlemex 10534 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlemaz 10536* | Lemma for Bézout's identity. Like bezoutlemzz 10535 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembz 10537* | Lemma for Bézout's identity. Like bezoutlemaz 10536 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
Theorem | bezoutlembi 10538* | Lemma for Bézout's identity. Like bezoutlembz 10537 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 10539* | 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 10540* | 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 10541* | 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 10542* | 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 10543* | Alternate definition of the operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
Theorem | bezout 10544* |
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 10545 | 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 10546 | Biconditional form of dvdsgcd 10545. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dfgcd2 10547* | Alternate definition of the operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
Theorem | gcdass 10548 | 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 10549 | 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 10550 | Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | mulgcdr 10551 | Reverse distribution law for the operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcddiv 10552 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdmultiple 10553 | 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 10554 | Extend gcdmultiple 10553 so can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | gcdzeq 10555 | A positive integer is equal to its gcd with an integer if and only if divides . Generalization of gcdeq 10556. (Contributed by AV, 1-Jul-2020.) |
Theorem | gcdeq 10556 | 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 10557 | Unidirectional form of dvdssq 10564. (Contributed by Scott Fenton, 19-Apr-2014.) |
Theorem | dvdsmulgcd 10558 | 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 10559 | 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 10560 | 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 10561 | 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 10562 | Square distributes over GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dvdssqlem 10563 | Lemma for dvdssq 10564. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | dvdssq 10564 | Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | bezoutr 10565 | Partial converse to bezout 10544. 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 10566 | Converse of bezout 10544 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.) |
Theorem | nn0seqcvgd 10567* | 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 10568 | Lemma for ialgr0 10570. Expressing algrflemg 5882 in a form suitable for theorems such as iseq1 9533 or iseqfcl 9535. (Contributed by Jim Kingdon, 22-Jul-2021.) |
Theorem | ialgrlemconst 10569 | Lemma for ialgr0 10570. Closure of a constant function, in a form suitable for theorems such as iseq1 9533 or iseqfcl 9535. (Contributed by Jim Kingdon, 22-Jul-2021.) |
Theorem | ialgr0 10570 | The value of the algorithm iterator at is the initial state . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | ialgrf 10571 |
An algorithm is a step function on a state space .
An algorithm acts on an initial state by
iteratively applying
to give , , and so
on. An algorithm is said to halt if a fixed point of is reached
after a finite number of iterations.
The algorithm iterator "runs" the algorithm so that is the state after iterations of on the initial state . Domain and codomain of the algorithm iterator . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | ialgrp1 10572 | The value of the algorithm iterator at . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
Theorem | ialginv 10573* | If is an invariant of , its value is unchanged after any number of iterations of . (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ialgcvg 10574* |
One way to prove that an algorithm halts is to construct a countdown
function whose value is guaranteed to decrease for
each iteration of until it reaches . That is, if
is not a fixed point of , then
.
If is a countdown function for algorithm , the sequence reaches after at most steps, where is the value of for the initial state . (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | algcvgblem 10575 | Lemma for algcvgb 10576. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | algcvgb 10576 | Two ways of expressing that is a countdown function for algorithm . The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | ialgcvga 10577* | The countdown function remains after steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | ialgfx 10578* | If reaches a fixed point when the countdown function reaches , remains fixed after steps. (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | eucalgval2 10579* | The value of the step function for Euclid's Algorithm on an ordered pair. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | eucalgval 10580* |
Euclid's Algorithm eucialg 10585 computes the greatest common divisor of two
nonnegative integers by repeatedly replacing the larger of them with its
remainder modulo the smaller until the remainder is 0.
The value of the step function for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | eucalgf 10581* | Domain and codomain of the step function for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
Theorem | eucalginv 10582* | The invariant of the step function for Euclid's Algorithm is the operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.) |
Theorem | eucalglt 10583* | The second member of the state decreases with each iteration of the step function for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.) |
Theorem | eucialgcvga 10584* | Once Euclid's Algorithm halts after steps, the second element of the state remains 0 . (Contributed by Jim Kingdon, 11-Jan-2022.) |
Theorem | eucialg 10585* |
Euclid's Algorithm computes the greatest common divisor of two
nonnegative integers by repeatedly replacing the larger of them with
its remainder modulo the smaller until the remainder is 0. Theorem
1.15 in [ApostolNT] p. 20.
Upon halting, the 1st member of the final state is equal to the gcd of the values comprising the input state . This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Jim Kingdon, 11-Jan-2022.) |
According to Wikipedia ("Least common multiple", 27-Aug-2020, https://en.wikipedia.org/wiki/Least_common_multiple): "In arithmetic and number theory, the least common multiple, lowest common multiple, or smallest common multiple of two integers a and b, usually denoted by lcm(a, b), is the smallest positive integer that is divisible by both a and b. Since division of integers by zero is undefined, this definition has meaning only if a and b are both different from zero. However, some authors define lcm(a,0) as 0 for all a, which is the result of taking the lcm to be the least upper bound in the lattice of divisibility." In this section, an operation calculating the least common multiple of two integers (df-lcm 10587). The definition is valid for all integers, including negative integers and 0, obeying the above mentioned convention. | ||
Syntax | clcm 10586 | Extend the definition of a class to include the least common multiple operator. |
lcm | ||
Definition | df-lcm 10587* | Define the lcm operator. For example, lcm . (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
lcm inf | ||
Theorem | lcmmndc 10588 | Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.) |
DECID | ||
Theorem | lcmval 10589* | Value of the lcm operator. lcm is the least common multiple of and . If either or is , the result is defined conventionally as . Contrast with df-gcd 10483 and gcdval 10495. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
lcm inf | ||
Theorem | lcmcom 10590 | The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
lcm lcm | ||
Theorem | lcm0val 10591 | The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 10590 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
lcm | ||
Theorem | lcmn0val 10592* | The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
lcm inf | ||
Theorem | lcmcllem 10593* | Lemma for lcmn0cl 10594 and dvdslcm 10595. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
lcm | ||
Theorem | lcmn0cl 10594 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | dvdslcm 10595 | The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm lcm | ||
Theorem | lcmledvds 10596 | A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
lcm | ||
Theorem | lcmeq0 10597 | The lcm of two integers is zero iff either is zero. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcmcl 10598 | Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | gcddvdslcm 10599 | The greatest common divisor of two numbers divides their least common multiple. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm | ||
Theorem | lcmneg 10600 | Negating one operand of the lcm operator does not alter the result. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
lcm lcm |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |