P. 125 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12401-12500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oddp1d2 12401	An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo 9552 and zeo2 9553. (Contributed by AV, 22-Jun-2021.)
|- ( N e. ZZ -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
Theorem	zob 12402	Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.)
|- ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
Theorem	oddm1d2 12403	An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.)
|- ( N e. ZZ -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
Theorem	ltoddhalfle 12404	An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ M e. ZZ ) -> ( M < ( N / 2 ) <-> M <_ ( ( N - 1 ) / 2 ) ) )
Theorem	halfleoddlt 12405	An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N /\ M e. ZZ ) -> ( ( N / 2 ) <_ M <-> ( N / 2 ) < M ) )
Theorem	opoe 12406	The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ -. 2 || B ) ) -> 2 || ( A + B ) )
Theorem	omoe 12407	The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ -. 2 || B ) ) -> 2 || ( A - B ) )
Theorem	opeo 12408	The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ 2 || B ) ) -> -. 2 || ( A + B ) )
Theorem	omeo 12409	The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ 2 || B ) ) -> -. 2 || ( A - B ) )
Theorem	m1expe 12410	Exponentiation of -1 by an even power. Variant of m1expeven 10808. (Contributed by AV, 25-Jun-2021.)
|- ( 2 || N -> ( -u 1 ^ N ) = 1 )
Theorem	m1expo 12411	Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( -u 1 ^ N ) = -u 1 )
Theorem	m1exp1 12412	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 12413	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 12414	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 12415	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 12416	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 12417	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 12418	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 12419	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 12420	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 12421	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 12422	0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
|- 2 || 0
Theorem	n2dvds1 12423	2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -. 2 || 1
Theorem	n2dvdsm1 12424	2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
|- -. 2 || -u 1
Theorem	z2even 12425	2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
|- 2 || 2
Theorem	n2dvds3 12426	2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.)
|- -. 2 || 3
Theorem	z4even 12427	4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
|- 2 || 4
Theorem	4dvdseven 12428	An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.)
|- ( 4 || N -> 2 || N )
5.1.3  The division algorithm
Theorem	divalglemnn 12429*	Lemma for divalg 12435. 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 12430	Lemma for divalg 12435. 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 12431	Lemma for divalg 12435. 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 12432*	Lemma for divalg 12435. 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 12433*	Lemma for divalg 12435. 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 12434*	Lemma for divalg 12435. 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 12435*	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 12436*	Express the division algorithm as stated in divalg 12435 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 12437*	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 12438	The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor (compare divalg2 12437 and divalgb 12436). 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 12439	The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor. Variant of divalgmod 12438. (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 12440*	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 12441	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 12442	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 12443	Special case of ndvdsadd 12442. 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 12444	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	5ndvds3 12445	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 3
Theorem	5ndvds6 12446	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 6
Theorem	flodddiv4 12447	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 12448	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 12449	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 12450	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 ) )
5.1.4  Bit sequences
Syntax	cbits 12451	Define the binary bits of an integer.
class bits
Definition	df-bits 12452*	Define the binary bits of an integer. The expression M e. (bits ` N ) means that the M-th bit of N is 1 (and its negation means the bit is 0). (Contributed by Mario Carneiro, 4-Sep-2016.)
|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
Theorem	bitsfval 12453*	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> (bits ` N ) = { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } )
Theorem	bitsval 12454	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( M e. (bits ` N ) <-> ( N e. ZZ /\ M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
Theorem	bitsval2 12455	Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. (bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
Theorem	bitsss 12456	The set of bits of an integer is a subset of NN0. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- (bits ` N ) C_ NN0
Theorem	bitsf 12457	The bits function is a function from integers to subsets of nonnegative integers. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- bits : ZZ --> ~P NN0
Theorem	bitsdc 12458	Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
|- ( ( N e. ZZ /\ M e. NN0 ) -> DECID M e. (bits ` N ) )
Theorem	bits0 12459	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( 0 e. (bits ` N ) <-> -. 2 || N ) )
Theorem	bits0e 12460	The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> -. 0 e. (bits ` ( 2 x. N ) ) )
Theorem	bits0o 12461	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 12462	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 12463	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 12464	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 12465*	Lemma for bitsfzo 12466. (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 12466	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 12467	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 12468	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 12469	The bit complement of N is -u N - 1. (Thus, by bitsfi 12468, 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 12470	The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.)
|- (bits ` 0 ) = (/)
Theorem	m1bits 12471	The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- (bits ` -u 1 ) = NN0
Theorem	bitsinv1lem 12472	Lemma for bitsinv1 12473. (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 12473*	There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 12469), 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 12474	Extend the definition of a class to include the greatest common divisor operator.
class gcd
Definition	df-gcd 12475*	Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 (ex-gcd 16095). (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 12476	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 12477*	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 12478*	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 12479*	Closure of the supremum used in defining gcd. A lemma for gcdval 12480 and gcdn0cl 12483. (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 12480*	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 12481	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 12482*	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 12483	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 12484	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 12485	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 12486	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 12487	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 12488	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 12489	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 12490	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 12491*	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 12492	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 12493	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 12494	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 12495	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 12496	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 12497	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 12498	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 12499	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 12500	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 ) )