P. 126 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12501-12600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bits0o 12501	The zeroth bit of an odd number is one. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> 0 e. (bits ` ( ( 2 x. N ) + 1 ) ) )
Theorem	bitsp1 12502	The M + 1-th bit of N is the M-th bit of |_ ( N / 2 ). (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. (bits ` N ) <-> M e. (bits ` ( |_ ` ( N / 2 ) ) ) ) )
Theorem	bitsp1e 12503	The M + 1-th bit of 2 N is the M-th bit of N. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. (bits ` ( 2 x. N ) ) <-> M e. (bits ` N ) ) )
Theorem	bitsp1o 12504	The M + 1-th bit of 2 N + 1 is the M-th bit of N. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. (bits ` ( ( 2 x. N ) + 1 ) ) <-> M e. (bits ` N ) ) )
Theorem	bitsfzolem 12505*	Lemma for bitsfzo 12506. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 1-Oct-2020.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> (bits ` N ) C_ ( 0..^ M ) )   &    |- S = inf ( { n e. NN0 | N < ( 2 ^ n ) } , RR , < )   =>    |- ( ph -> N e. ( 0..^ ( 2 ^ M ) ) )
Theorem	bitsfzo 12506	The bits of a number are all at positions less than M iff the number is nonnegative and less than 2 ^ M. (Contributed by Mario Carneiro, 5-Sep-2016.) (Proof shortened by AV, 1-Oct-2020.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( N e. ( 0..^ ( 2 ^ M ) ) <-> (bits ` N ) C_ ( 0..^ M ) ) )
Theorem	bitsmod 12507	Truncating the bit sequence after some M is equivalent to reducing the argument mod 2 ^ M. (Contributed by Mario Carneiro, 6-Sep-2016.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> (bits ` ( N mod ( 2 ^ M ) ) ) = ( (bits ` N ) i^i ( 0..^ M ) ) )
Theorem	bitsfi 12508	Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. NN0 -> (bits ` N ) e. Fin )
Theorem	bitscmp 12509	The bit complement of N is -u N - 1. (Thus, by bitsfi 12508, all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( NN0 \ (bits ` N ) ) = (bits ` ( -u N - 1 ) ) )
Theorem	0bits 12510	The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.)
|- (bits ` 0 ) = (/)
Theorem	m1bits 12511	The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- (bits ` -u 1 ) = NN0
Theorem	bitsinv1lem 12512	Lemma for bitsinv1 12513. (Contributed by Mario Carneiro, 22-Sep-2016.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ ( M + 1 ) ) ) = ( ( N mod ( 2 ^ M ) ) + if ( M e. (bits ` N ) , ( 2 ^ M ) , 0 ) ) )
Theorem	bitsinv1 12513*	There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 12509), part 1. (Contributed by Mario Carneiro, 7-Sep-2016.)
|- ( N e. NN0 -> sum_ n e. (bits ` N ) ( 2 ^ n ) = N )
5.1.5  The greatest common divisor operator
Syntax	cgcd 12514	Extend the definition of a class to include the greatest common divisor operator.
class gcd
Definition	df-gcd 12515*	Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 (ex-gcd 16263). (Contributed by Paul Chapman, 21-Mar-2011.)
|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
Theorem	gcdmndc 12516	Decidablity lemma used in various proofs related to gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> DECID ( M = 0 /\ N = 0 ) )
Theorem	dvdsbnd 12517*	There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.)
|- ( ( A e. ZZ /\ A =/= 0 ) -> E. n e. NN A. m e. ( ZZ>= ` n ) -. m || A )
Theorem	gcdsupex 12518*	Existence of the supremum used in defining gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
|- ( ( ( X e. ZZ /\ Y e. ZZ ) /\ -. ( X = 0 /\ Y = 0 ) ) -> E. x e. ZZ ( A. y e. { n e. ZZ | ( n || X /\ n || Y ) } -. x < y /\ A. y e. RR ( y < x -> E. z e. { n e. ZZ | ( n || X /\ n || Y ) } y < z ) ) )
Theorem	gcdsupcl 12519*	Closure of the supremum used in defining gcd. A lemma for gcdval 12520 and gcdn0cl 12523. (Contributed by Jim Kingdon, 11-Dec-2021.)
|- ( ( ( X e. ZZ /\ Y e. ZZ ) /\ -. ( X = 0 /\ Y = 0 ) ) -> sup ( { n e. ZZ | ( n || X /\ n || Y ) } , RR , < ) e. NN )
Theorem	gcdval 12520*	The value of the gcd operator. ( M gcd N ) is the greatest common divisor of M and N. If M and N are both 0, the result is defined conventionally as 0. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = if ( ( M = 0 /\ N = 0 ) , 0 , sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) ) )
Theorem	gcd0val 12521	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 12522*	The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = sup ( { n e. ZZ | ( n || M /\ n || N ) } , RR , < ) )
Theorem	gcdn0cl 12523	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )
Theorem	gcddvds 12524	The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
Theorem	dvdslegcd 12525	An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) )
Theorem	nndvdslegcd 12526	A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020.)
|- ( ( K e. NN /\ M e. NN /\ N e. NN ) -> ( ( K || M /\ K || N ) -> K <_ ( M gcd N ) ) )
Theorem	gcdcl 12527	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
Theorem	gcdnncl 12528	Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.)
|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN )
Theorem	gcdcld 12529	Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( M gcd N ) e. NN0 )
Theorem	gcd2n0cl 12530	Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.)
|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M gcd N ) e. NN )
Theorem	zeqzmulgcd 12531*	An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> E. n e. ZZ A = ( n x. ( A gcd B ) ) )
Theorem	divgcdz 12532	An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ /\ B =/= 0 ) -> ( A / ( A gcd B ) ) e. ZZ )
Theorem	gcdf 12533	Domain and codomain of the gcd operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- gcd : ( ZZ X. ZZ ) --> NN0
Theorem	gcdcom 12534	The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( N gcd M ) )
Theorem	gcdcomd 12535	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( M gcd N ) = ( N gcd M ) )
Theorem	divgcdnn 12536	A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.)
|- ( ( A e. NN /\ B e. ZZ ) -> ( A / ( A gcd B ) ) e. NN )
Theorem	divgcdnnr 12537	A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.)
|- ( ( A e. NN /\ B e. ZZ ) -> ( A / ( B gcd A ) ) e. NN )
Theorem	gcdeq0 12538	The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) = 0 <-> ( M = 0 /\ N = 0 ) ) )
Theorem	gcdn0gt0 12539	The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) <-> 0 < ( M gcd N ) ) )
Theorem	gcd0id 12540	The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> ( 0 gcd N ) = ( abs ` N ) )
Theorem	gcdid0 12541	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.)
|- ( N e. ZZ -> ( N gcd 0 ) = ( abs ` N ) )
Theorem	nn0gcdid0 12542	The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( N e. NN0 -> ( N gcd 0 ) = N )
Theorem	gcdneg 12543	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) = ( M gcd N ) )
Theorem	neggcd 12544	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M gcd N ) = ( M gcd N ) )
Theorem	gcdaddm 12545	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.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) ) )
Theorem	gcdadd 12546	The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + M ) ) )
Theorem	gcdid 12547	The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( N e. ZZ -> ( N gcd N ) = ( abs ` N ) )
Theorem	gcd1 12548	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.)
|- ( M e. ZZ -> ( M gcd 1 ) = 1 )
Theorem	gcdabs 12549	The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
Theorem	gcdabs1 12550	gcd of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( N e. ZZ /\ M e. ZZ ) -> ( ( abs ` N ) gcd M ) = ( N gcd M ) )
Theorem	gcdabs2 12551	gcd of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( N e. ZZ /\ M e. ZZ ) -> ( N gcd ( abs ` M ) ) = ( N gcd M ) )
Theorem	modgcd 12552	The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) gcd N ) = ( M gcd N ) )
Theorem	1gcd 12553	The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( M e. ZZ -> ( 1 gcd M ) = 1 )
Theorem	gcdmultipled 12554	The greatest common divisor of a nonnegative integer M and a multiple of it is M itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> M e. NN0 )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( M gcd ( N x. M ) ) = M )
Theorem	dvdsgcdidd 12555	The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> M e. NN )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> M || N )   =>    |- ( ph -> ( M gcd N ) = M )
Theorem	6gcd4e2 12556	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
5.1.6  Bézout's identity
Theorem	bezoutlemnewy 12557*	Lemma for Bézout's identity. The is-bezout predicate holds for ( y mod W ). (Contributed by Jim Kingdon, 6-Jan-2022.)
|- ( ph <-> E. s e. ZZ E. t e. ZZ r = ( ( A x. s ) + ( B x. t ) ) )   &    |- ( th -> A e. NN0 )   &    |- ( th -> B e. NN0 )   &    |- ( th -> W e. NN )   &    |- ( th -> [ y / r ] ph )   &    |- ( th -> y e. NN0 )   &    |- ( th -> [. W / r ]. ph )   =>    |- ( th -> [. ( y mod W ) / r ]. ph )
Theorem	bezoutlemstep 12558*	Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.)
|- ( ph <-> E. s e. ZZ E. t e. ZZ r = ( ( A x. s ) + ( B x. t ) ) )   &    |- ( th -> A e. NN0 )   &    |- ( th -> B e. NN0 )   &    |- ( th -> W e. NN )   &    |- ( th -> [ y / r ] ph )   &    |- ( th -> y e. NN0 )   &    |- ( th -> [. W / r ]. ph )   &    |- ( ps <-> A. z e. NN0 ( z || r -> ( z || x /\ z || y ) ) )   &    |- ( ( th /\ [. ( y mod W ) / r ]. ph ) -> E. r e. NN0 ( [. ( y mod W ) / x ]. [. W / y ]. ps /\ ph ) )   &    |- F/ x th   &    |- F/ r th   =>    |- ( th -> E. r e. NN0 ( [. W / x ]. ps /\ ph ) )
Theorem	bezoutlemmain 12559*	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.)
|- ( ph <-> E. s e. ZZ E. t e. ZZ r = ( ( A x. s ) + ( B x. t ) ) )   &    |- ( ps <-> A. z e. NN0 ( z || r -> ( z || x /\ z || y ) ) )   &    |- ( th -> A e. NN0 )   &    |- ( th -> B e. NN0 )   =>    |- ( th -> A. x e. NN0 ( [ x / r ] ph -> A. y e. NN0 ( [ y / r ] ph -> E. r e. NN0 ( ps /\ ph ) ) ) )
Theorem	bezoutlema 12560*	Lemma for Bézout's identity. The is-bezout condition is satisfied by A. (Contributed by Jim Kingdon, 30-Dec-2021.)
|- ( ph <-> E. s e. ZZ E. t e. ZZ r = ( ( A x. s ) + ( B x. t ) ) )   &    |- ( th -> A e. NN0 )   &    |- ( th -> B e. NN0 )   =>    |- ( th -> [. A / r ]. ph )
Theorem	bezoutlemb 12561*	Lemma for Bézout's identity. The is-bezout condition is satisfied by B. (Contributed by Jim Kingdon, 30-Dec-2021.)
|- ( ph <-> E. s e. ZZ E. t e. ZZ r = ( ( A x. s ) + ( B x. t ) ) )   &    |- ( th -> A e. NN0 )   &    |- ( th -> B e. NN0 )   =>    |- ( th -> [. B / r ]. ph )
Theorem	bezoutlemex 12562*	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.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> E. d e. NN0 ( A. z e. NN0 ( z || d -> ( z || A /\ z || B ) ) /\ E. x e. ZZ E. y e. ZZ d = ( ( A x. x ) + ( B x. y ) ) ) )
Theorem	bezoutlemzz 12563*	Lemma for Bézout's identity. Like bezoutlemex 12562 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> E. d e. NN0 ( A. z e. ZZ ( z || d -> ( z || A /\ z || B ) ) /\ E. x e. ZZ E. y e. ZZ d = ( ( A x. x ) + ( B x. y ) ) ) )
Theorem	bezoutlemaz 12564*	Lemma for Bézout's identity. Like bezoutlemzz 12563 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
|- ( ( A e. ZZ /\ B e. NN0 ) -> E. d e. NN0 ( A. z e. ZZ ( z || d -> ( z || A /\ z || B ) ) /\ E. x e. ZZ E. y e. ZZ d = ( ( A x. x ) + ( B x. y ) ) ) )
Theorem	bezoutlembz 12565*	Lemma for Bézout's identity. Like bezoutlemaz 12564 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> E. d e. NN0 ( A. z e. ZZ ( z || d -> ( z || A /\ z || B ) ) /\ E. x e. ZZ E. y e. ZZ d = ( ( A x. x ) + ( B x. y ) ) ) )
Theorem	bezoutlembi 12566*	Lemma for Bézout's identity. Like bezoutlembz 12565 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> E. d e. NN0 ( A. z e. ZZ ( z || d <-> ( z || A /\ z || B ) ) /\ E. x e. ZZ E. y e. ZZ d = ( ( A x. x ) + ( B x. y ) ) ) )
Theorem	bezoutlemmo 12567*	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.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> A. z e. ZZ ( z || D <-> ( z || A /\ z || B ) ) )   &    |- ( ph -> E e. NN0 )   &    |- ( ph -> A. z e. ZZ ( z || E <-> ( z || A /\ z || B ) ) )   =>    |- ( ph -> D = E )
Theorem	bezoutlemeu 12568*	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.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> A. z e. ZZ ( z || D <-> ( z || A /\ z || B ) ) )   =>    |- ( ph -> E! d e. NN0 A. z e. ZZ ( z || d <-> ( z || A /\ z || B ) ) )
Theorem	bezoutlemle 12569*	Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both A and B. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> A. z e. ZZ ( z || D <-> ( z || A /\ z || B ) ) )   &    |- ( ph -> -. ( A = 0 /\ B = 0 ) )   =>    |- ( ph -> A. z e. ZZ ( ( z || A /\ z || B ) -> z <_ D ) )
Theorem	bezoutlemsup 12570*	Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both A and B. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> A. z e. ZZ ( z || D <-> ( z || A /\ z || B ) ) )   &    |- ( ph -> -. ( A = 0 /\ B = 0 ) )   =>    |- ( ph -> D = sup ( { z e. ZZ | ( z || A /\ z || B ) } , RR , < ) )
Theorem	dfgcd3 12571*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( iota_ d e. NN0 A. z e. ZZ ( z || d <-> ( z || M /\ z || N ) ) ) )
Theorem	bezout 12572*	Bézout's identity: For any integers A and B, there are integers x , y such that ( A gcd B ) = A x. x + B x. y. 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 ( A gcd B ) 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.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )
Theorem	dvdsgcd 12573	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.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M gcd N ) ) )
Theorem	dvdsgcdb 12574	Biconditional form of dvdsgcd 12573. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) <-> K || ( M gcd N ) ) )
Theorem	dfgcd2 12575*	Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( D = ( M gcd N ) <-> ( 0 <_ D /\ ( D || M /\ D || N ) /\ A. e e. ZZ ( ( e || M /\ e || N ) -> e || D ) ) ) )
Theorem	gcdass 12576	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.)
|- ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N gcd M ) gcd P ) = ( N gcd ( M gcd P ) ) )
Theorem	mulgcd 12577	Distribute multiplication by a nonnegative integer over gcd. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 30-May-2014.)
|- ( ( K e. NN0 /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( K x. ( M gcd N ) ) )
Theorem	absmulgcd 12578	Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) gcd ( K x. N ) ) = ( abs ` ( K x. ( M gcd N ) ) ) )
Theorem	mulgcdr 12579	Reverse distribution law for the gcd operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ C e. NN0 ) -> ( ( A x. C ) gcd ( B x. C ) ) = ( ( A gcd B ) x. C ) )
Theorem	gcddiv 12580	Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ ( C || A /\ C || B ) ) -> ( ( A gcd B ) / C ) = ( ( A / C ) gcd ( B / C ) ) )
Theorem	gcdmultiple 12581	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.)
|- ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M )
Theorem	gcdmultiplez 12582	Extend gcdmultiple 12581 so N can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M )
Theorem	gcdzeq 12583	A positive integer A is equal to its gcd with an integer B if and only if A divides B. Generalization of gcdeq 12584. (Contributed by AV, 1-Jul-2020.)
|- ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) )
Theorem	gcdeq 12584	A is equal to its gcd with B if and only if A divides B. (Contributed by Mario Carneiro, 23-Feb-2014.) (Proof shortened by AV, 8-Aug-2021.)
|- ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) = A <-> A || B ) )
Theorem	dvdssqim 12585	Unidirectional form of dvdssq 12592. (Contributed by Scott Fenton, 19-Apr-2014.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( M ^ 2 ) || ( N ^ 2 ) ) )
Theorem	dvdsmulgcd 12586	Relationship between the order of an element and that of a multiple. (a divisibility equivalent). (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( B e. ZZ /\ C e. ZZ ) -> ( A || ( B x. C ) <-> A || ( B x. ( C gcd A ) ) ) )
Theorem	rpmulgcd 12587	If K and M are relatively prime, then the GCD of K and M x. N is the GCD of K and N. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( K e. NN /\ M e. NN /\ N e. NN ) /\ ( K gcd M ) = 1 ) -> ( K gcd ( M x. N ) ) = ( K gcd N ) )
Theorem	rplpwr 12588	If A and B are relatively prime, then so are A ^ N and B. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd B ) = 1 ) )
Theorem	rppwr 12589	If A and B are relatively prime, then so are A ^ N and B ^ N. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
Theorem	sqgcd 12590	Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( M e. NN /\ N e. NN ) -> ( ( M gcd N ) ^ 2 ) = ( ( M ^ 2 ) gcd ( N ^ 2 ) ) )
Theorem	dvdssqlem 12591	Lemma for dvdssq 12592. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( M e. NN /\ N e. NN ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )
Theorem	dvdssq 12592	Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( M ^ 2 ) || ( N ^ 2 ) ) )
Theorem	bezoutr 12593	Partial converse to bezout 12572. Existence of a linear combination does not set the GCD, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || ( ( A x. X ) + ( B x. Y ) ) )
Theorem	bezoutr1 12594	Converse of bezout 12572 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = 1 -> ( A gcd B ) = 1 ) )
5.1.7  Decidable sets of integers
Theorem	nnmindc 12595*	An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ E. y y e. A ) -> inf ( A , RR , < ) e. A )
Theorem	nnminle 12596*	The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 12595. (Contributed by Jim Kingdon, 26-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ B e. A ) -> inf ( A , RR , < ) <_ B )
Theorem	nnwodc 12597*	Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.)
|- ( ( A C_ NN /\ E. w w e. A /\ A. j e. NN DECID j e. A ) -> E. x e. A A. y e. A x <_ y )
Theorem	uzwodc 12598*	Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)
|- ( ( S C_ ( ZZ>= ` M ) /\ E. x x e. S /\ A. x e. ( ZZ>= ` M )DECID x e. S ) -> E. j e. S A. k e. S j <_ k )
Theorem	nnwofdc 12599*	Well-ordering principle: any inhabited decidable set of positive integers has a least element. This version allows x and y to be present in A as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ y A   =>    |- ( ( A C_ NN /\ E. z z e. A /\ A. j e. NN DECID j e. A ) -> E. x e. A A. y e. A x <_ y )
Theorem	nnwosdc 12600*	Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( ( E. x e. NN ph /\ A. x e. NN DECID ph ) -> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) )