P. 104 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10301-10400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	m1exp1 10301	Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.)
|- ( N e. ZZ -> ( ( -u 1 ^ N ) = 1 <-> 2 || N ) )
Theorem	nn0enne 10302	A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.)
|- ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )
Theorem	nn0ehalf 10303	The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.)
|- ( ( N e. NN0 /\ 2 || N ) -> ( N / 2 ) e. NN0 )
Theorem	nnehalf 10304	The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.)
|- ( ( N e. NN /\ 2 || N ) -> ( N / 2 ) e. NN )
Theorem	nn0o1gt2 10305	An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )
Theorem	nno 10306	An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN )
Theorem	nn0o 10307	An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
Theorem	nn0ob 10308	Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
|- ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	nn0oddm1d2 10309	A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.)
|- ( N e. NN0 -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	nnoddm1d2 10310	A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.)
|- ( N e. NN -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. NN ) )
Theorem	z0even 10311	0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
|- 2 || 0
Theorem	n2dvds1 10312	2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -. 2 || 1
Theorem	n2dvdsm1 10313	2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
|- -. 2 || -u 1
Theorem	z2even 10314	2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
|- 2 || 2
Theorem	n2dvds3 10315	2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.)
|- -. 2 || 3
Theorem	z4even 10316	4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
|- 2 || 4
Theorem	4dvdseven 10317	An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.)
|- ( 4 || N -> 2 || N )
4.1.3  The division algorithm
Theorem	divalglemnn 10318*	Lemma for divalg 10324. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.)
|- ( ( N e. ZZ /\ D e. NN ) -> E. r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
Theorem	divalglemqt 10319	Lemma for divalg 10324. The Q = T case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.)
|- ( ph -> D e. ZZ )   &    |- ( ph -> R e. ZZ )   &    |- ( ph -> S e. ZZ )   &    |- ( ph -> Q e. ZZ )   &    |- ( ph -> T e. ZZ )   &    |- ( ph -> Q = T )   &    |- ( ph -> ( ( Q x. D ) + R ) = ( ( T x. D ) + S ) )   =>    |- ( ph -> R = S )
Theorem	divalglemnqt 10320	Lemma for divalg 10324. The Q < T case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.)
|- ( ph -> D e. NN )   &    |- ( ph -> R e. ZZ )   &    |- ( ph -> S e. ZZ )   &    |- ( ph -> Q e. ZZ )   &    |- ( ph -> T e. ZZ )   &    |- ( ph -> 0 <_ S )   &    |- ( ph -> R < D )   &    |- ( ph -> ( ( Q x. D ) + R ) = ( ( T x. D ) + S ) )   =>    |- ( ph -> -. Q < T )
Theorem	divalglemeunn 10321*	Lemma for divalg 10324. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
|- ( ( N e. ZZ /\ D e. NN ) -> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
Theorem	divalglemex 10322*	Lemma for divalg 10324. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.)
|- ( ( N e. ZZ /\ D e. ZZ /\ D =/= 0 ) -> E. r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
Theorem	divalglemeuneg 10323*	Lemma for divalg 10324. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
|- ( ( N e. ZZ /\ D e. ZZ /\ D < 0 ) -> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
Theorem	divalg 10324*	The division algorithm (theorem). Dividing an integer N by a nonzero integer D produces a (unique) quotient q and a unique remainder 0 <_ r < ( abs ` D ). Theorem 1.14 in [ApostolNT] p. 19. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( N e. ZZ /\ D e. ZZ /\ D =/= 0 ) -> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) )
Theorem	divalgb 10325*	Express the division algorithm as stated in divalg 10324 in terms of ||. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( N e. ZZ /\ D e. ZZ /\ D =/= 0 ) -> ( E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` D ) /\ N = ( ( q x. D ) + r ) ) <-> E! r e. NN0 ( r < ( abs ` D ) /\ D || ( N - r ) ) ) )
Theorem	divalg2 10326*	The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( N e. ZZ /\ D e. NN ) -> E! r e. NN0 ( r < D /\ D || ( N - r ) ) )
Theorem	divalgmod 10327	The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor (compare divalg2 10326 and divalgb 10325). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.)
|- ( ( N e. ZZ /\ D e. NN ) -> ( R = ( N mod D ) <-> ( R e. NN0 /\ ( R < D /\ D || ( N - R ) ) ) ) )
Theorem	divalgmodcl 10328	The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor. Variant of divalgmod 10327. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.)
|- ( ( N e. ZZ /\ D e. NN /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D || ( N - R ) ) ) )
Theorem	modremain 10329*	The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.)
|- ( ( N e. ZZ /\ D e. NN /\ ( R e. NN0 /\ R < D ) ) -> ( ( N mod D ) = R <-> E. z e. ZZ ( ( z x. D ) + R ) = N ) )
Theorem	ndvdssub 10330	Corollary of the division algorithm. If an integer D greater than 1 divides N, then it does not divide any of N - 1, N - 2... N - ( D - 1 ). (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N - K ) ) )
Theorem	ndvdsadd 10331	Corollary of the division algorithm. If an integer D greater than 1 divides N, then it does not divide any of N + 1, N + 2... N + ( D - 1 ). (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( N e. ZZ /\ D e. NN /\ ( K e. NN /\ K < D ) ) -> ( D || N -> -. D || ( N + K ) ) )
Theorem	ndvdsp1 10332	Special case of ndvdsadd 10331. If an integer D greater than 1 divides N, it does not divide N + 1. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( N e. ZZ /\ D e. NN /\ 1 < D ) -> ( D || N -> -. D || ( N + 1 ) ) )
Theorem	ndvdsi 10333	A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN   &    |- Q e. NN0   &    |- R e. NN   &    |- ( ( A x. Q ) + R ) = B   &    |- R < A   =>    |- -. A || B
Theorem	flodddiv4 10334	The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.)
|- ( ( M e. ZZ /\ N = ( ( 2 x. M ) + 1 ) ) -> ( |_ ` ( N / 4 ) ) = if ( 2 || M , ( M / 2 ) , ( ( M - 1 ) / 2 ) ) )
Theorem	fldivndvdslt 10335	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.)
|- ( ( K e. ZZ /\ ( L e. ZZ /\ L =/= 0 ) /\ -. L || K ) -> ( |_ ` ( K / L ) ) < ( K / L ) )
Theorem	flodddiv4lt 10336	The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( |_ ` ( N / 4 ) ) < ( N / 4 ) )
Theorem	flodddiv4t2lthalf 10337	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.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( ( |_ ` ( N / 4 ) ) x. 2 ) < ( N / 2 ) )
4.1.4  The greatest common divisor operator
Syntax	cgcd 10338	Extend the definition of a class to include the greatest common divisor operator.
class gcd
Definition	df-gcd 10339*	Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 (ex-gcd 10568). (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 10340	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	zsupcllemstep 10341*	Lemma for zsupcl 10343. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.)
|- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> DECID ps )   =>    |- ( K e. ( ZZ>= ` M ) -> ( ( ( ph /\ A. n e. ( ZZ>= ` K ) -. ps ) -> E. x e. ZZ ( A. y e. { n e. ZZ | ps } -. x < y /\ A. y e. RR ( y < x -> E. z e. { n e. ZZ | ps } y < z ) ) ) -> ( ( ph /\ A. n e. ( ZZ>= ` ( K + 1 ) ) -. ps ) -> E. x e. ZZ ( A. y e. { n e. ZZ | ps } -. x < y /\ A. y e. RR ( y < x -> E. z e. { n e. ZZ | ps } y < z ) ) ) ) )
Theorem	zsupcllemex 10342*	Lemma for zsupcl 10343. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.)
|- ( ph -> M e. ZZ )   &    |- ( n = M -> ( ps <-> ch ) )   &    |- ( ph -> ch )   &    |- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> DECID ps )   &    |- ( ph -> E. j e. ( ZZ>= ` M ) A. n e. ( ZZ>= ` j ) -. ps )   =>    |- ( ph -> E. x e. ZZ ( A. y e. { n e. ZZ | ps } -. x < y /\ A. y e. RR ( y < x -> E. z e. { n e. ZZ | ps } y < z ) ) )
Theorem	zsupcl 10343*	Closure of supremum for decidable integer properties. The property which defines the set we are taking the supremum of must (a) be true at M (which corresponds to the non-empty condition of classical supremum theorems), (b) decidable at each value after M, and (c) be false after j (which corresponds to the upper bound condition found in classical supremum theorems). (Contributed by Jim Kingdon, 7-Dec-2021.)
|- ( ph -> M e. ZZ )   &    |- ( n = M -> ( ps <-> ch ) )   &    |- ( ph -> ch )   &    |- ( ( ph /\ n e. ( ZZ>= ` M ) ) -> DECID ps )   &    |- ( ph -> E. j e. ( ZZ>= ` M ) A. n e. ( ZZ>= ` j ) -. ps )   =>    |- ( ph -> sup ( { n e. ZZ | ps } , RR , < ) e. ( ZZ>= ` M ) )
Theorem	zssinfcl 10344*	The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. B -. y < x /\ A. y e. RR ( x < y -> E. z e. B z < y ) ) )   &    |- ( ph -> B C_ ZZ )   &    |- ( ph -> inf ( B , RR , < ) e. ZZ )   =>    |- ( ph -> inf ( B , RR , < ) e. B )
Theorem	infssuzex 10345*	Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- S = { n e. ( ZZ>= ` M ) | ps }   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ n e. ( M ... A ) ) -> DECID ps )   =>    |- ( ph -> E. x e. RR ( A. y e. S -. y < x /\ A. y e. RR ( x < y -> E. z e. S z < y ) ) )
Theorem	infssuzledc 10346*	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.)
|- ( ph -> M e. ZZ )   &    |- S = { n e. ( ZZ>= ` M ) | ps }   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ n e. ( M ... A ) ) -> DECID ps )   =>    |- ( ph -> inf ( S , RR , < ) <_ A )
Theorem	infssuzcldc 10347*	The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- S = { n e. ( ZZ>= ` M ) | ps }   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ n e. ( M ... A ) ) -> DECID ps )   =>    |- ( ph -> inf ( S , RR , < ) e. S )
Theorem	dvdsbnd 10348*	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 10349*	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 10350*	Closure of the supremum used in defining gcd. A lemma for gcdval 10351 and gcdn0cl 10354. (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 10351*	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 10352	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 10353*	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 10354	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 10355	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 10356	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 10357	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 10358	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 10359	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 10360	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 10361	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 10362*	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 10363	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 10364	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 10365	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	divgcdnn 10366	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 10367	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 10368	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 10369	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 10370	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 10371	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 10372	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 10373	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 10374	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 10375	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 10376	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 10377	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 10378	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 10379	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 10380	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 10381	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 10382	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 10383	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	6gcd4e2 10384	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
4.1.5  Bézout's identity
Theorem	bezoutlemnewy 10385*	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 10386*	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 10387*	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 10388*	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 10389*	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 10390*	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 10391*	Lemma for Bézout's identity. Like bezoutlemex 10390 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 10392*	Lemma for Bézout's identity. Like bezoutlemzz 10391 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 10393*	Lemma for Bézout's identity. Like bezoutlemaz 10392 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 10394*	Lemma for Bézout's identity. Like bezoutlembz 10393 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 10395*	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 10396*	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 10397*	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 10398*	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 10399*	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 10400*	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 ) ) )