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	oddm1even 12401	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
Theorem	oddp1even 12402	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )
Theorem	oexpneg 12403	The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.)
|- ( ( A e. CC /\ N e. NN /\ -. 2 || N ) -> ( -u A ^ N ) = -u ( A ^ N ) )
Theorem	mod2eq0even 12404	An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.)
|- ( N e. ZZ -> ( ( N mod 2 ) = 0 <-> 2 || N ) )
Theorem	mod2eq1n2dvds 12405	An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see example 3 in [ApostolNT] p. 107. (Contributed by AV, 24-May-2020.)
|- ( N e. ZZ -> ( ( N mod 2 ) = 1 <-> -. 2 || N ) )
Theorem	oddnn02np1 12406*	A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.)
|- ( N e. NN0 -> ( -. 2 || N <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )
Theorem	oddge22np1 12407*	An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.)
|- ( N e. ( ZZ>= ` 2 ) -> ( -. 2 || N <-> E. n e. NN ( ( 2 x. n ) + 1 ) = N ) )
Theorem	evennn02n 12408*	A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.)
|- ( N e. NN0 -> ( 2 || N <-> E. n e. NN0 ( 2 x. n ) = N ) )
Theorem	evennn2n 12409*	A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.)
|- ( N e. NN -> ( 2 || N <-> E. n e. NN ( 2 x. n ) = N ) )
Theorem	2tp1odd 12410	A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.)
|- ( ( A e. ZZ /\ B = ( ( 2 x. A ) + 1 ) ) -> -. 2 || B )
Theorem	mulsucdiv2z 12411	An integer multiplied with its successor divided by 2 yields an integer, i.e. an integer multiplied with its successor is even. (Contributed by AV, 19-Jul-2021.)
|- ( N e. ZZ -> ( ( N x. ( N + 1 ) ) / 2 ) e. ZZ )
Theorem	sqoddm1div8z 12412	A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.)
|- ( ( N e. ZZ /\ -. 2 || N ) -> ( ( ( N ^ 2 ) - 1 ) / 8 ) e. ZZ )
Theorem	2teven 12413	A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.)
|- ( ( A e. ZZ /\ B = ( 2 x. A ) ) -> 2 || B )
Theorem	zeo5 12414	An integer is either even or odd, version of zeo3 12394 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020.)
|- ( N e. ZZ -> ( 2 || N \/ 2 || ( N + 1 ) ) )
Theorem	evend2 12415	An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo 9563 and zeo2 9564. (Contributed by AV, 22-Jun-2021.)
|- ( N e. ZZ -> ( 2 || N <-> ( N / 2 ) e. ZZ ) )
Theorem	oddp1d2 12416	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 9563 and zeo2 9564. (Contributed by AV, 22-Jun-2021.)
|- ( N e. ZZ -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
Theorem	zob 12417	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 12418	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 12419	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 12420	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 12421	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 12422	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 12423	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 12424	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 12425	Exponentiation of -1 by an even power. Variant of m1expeven 10820. (Contributed by AV, 25-Jun-2021.)
|- ( 2 || N -> ( -u 1 ^ N ) = 1 )
Theorem	m1expo 12426	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 12427	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 12428	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 12429	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 12430	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 12431	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 12432	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 12433	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 12434	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 12435	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 12436	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 12437	0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
|- 2 || 0
Theorem	n2dvds1 12438	2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -. 2 || 1
Theorem	n2dvdsm1 12439	2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
|- -. 2 || -u 1
Theorem	z2even 12440	2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
|- 2 || 2
Theorem	n2dvds3 12441	2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.)
|- -. 2 || 3
Theorem	z4even 12442	4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
|- 2 || 4
Theorem	4dvdseven 12443	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 12444*	Lemma for divalg 12450. 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 12445	Lemma for divalg 12450. 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 12446	Lemma for divalg 12450. 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 12447*	Lemma for divalg 12450. 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 12448*	Lemma for divalg 12450. 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 12449*	Lemma for divalg 12450. 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 12450*	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 12451*	Express the division algorithm as stated in divalg 12450 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 12452*	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 12453	The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor (compare divalg2 12452 and divalgb 12451). 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 12454	The result of the mod operator satisfies the requirements for the remainder R in the division algorithm for a positive divisor. Variant of divalgmod 12453. (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 12455*	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 12456	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 12457	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 12458	Special case of ndvdsadd 12457. 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 12459	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 12460	5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 3
Theorem	5ndvds6 12461	5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
|- -. 5 || 6
Theorem	flodddiv4 12462	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 12463	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 12464	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 12465	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 12466	Define the binary bits of an integer.
class bits
Definition	df-bits 12467*	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 12468*	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 12469	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 12470	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 12471	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 12472	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 12473	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 12474	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( 0 e. (bits ` N ) <-> -. 2 || N ) )
Theorem	bits0e 12475	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 12476	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 12477	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 12478	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 12479	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 12480*	Lemma for bitsfzo 12481. (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 12481	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 12482	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 12483	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 12484	The bit complement of N is -u N - 1. (Thus, by bitsfi 12483, 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 12485	The bits of zero. (Contributed by Mario Carneiro, 6-Sep-2016.)
|- (bits ` 0 ) = (/)
Theorem	m1bits 12486	The bits of negative one. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- (bits ` -u 1 ) = NN0
Theorem	bitsinv1lem 12487	Lemma for bitsinv1 12488. (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 12488*	There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp 12484), 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 12489	Extend the definition of a class to include the greatest common divisor operator.
class gcd
Definition	df-gcd 12490*	Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 (ex-gcd 16150). (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 12491	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 12492*	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 12493*	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 12494*	Closure of the supremum used in defining gcd. A lemma for gcdval 12495 and gcdn0cl 12498. (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 12495*	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 12496	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 12497*	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 12498	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 12499	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 12500	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 ) ) )