Type  Label  Description 
Statement 

Theorem  oddm1even 11801 
An integer is odd iff its predecessor is even. (Contributed by Mario
Carneiro, 5Sep2016.)



Theorem  oddp1even 11802 
An integer is odd iff its successor is even. (Contributed by Mario
Carneiro, 5Sep2016.)



Theorem  oexpneg 11803 
The exponential of the negative of a number, when the exponent is odd.
(Contributed by Mario Carneiro, 25Apr2015.)



Theorem  mod2eq0even 11804 
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, 21Jul2021.)



Theorem  mod2eq1n2dvds 11805 
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, 24May2020.)



Theorem  oddnn02np1 11806* 
A nonnegative integer is odd iff it is one plus twice another
nonnegative integer. (Contributed by AV, 19Jun2021.)



Theorem  oddge22np1 11807* 
An integer greater than one is odd iff it is one plus twice a positive
integer. (Contributed by AV, 16Aug2021.)



Theorem  evennn02n 11808* 
A nonnegative integer is even iff it is twice another nonnegative
integer. (Contributed by AV, 12Aug2021.)



Theorem  evennn2n 11809* 
A positive integer is even iff it is twice another positive integer.
(Contributed by AV, 12Aug2021.)



Theorem  2tp1odd 11810 
A number which is twice an integer increased by 1 is odd. (Contributed
by AV, 16Jul2021.)



Theorem  mulsucdiv2z 11811 
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, 19Jul2021.)



Theorem  sqoddm1div8z 11812 
A squared odd number minus 1 divided by 8 is an integer. (Contributed
by AV, 19Jul2021.)



Theorem  2teven 11813 
A number which is twice an integer is even. (Contributed by AV,
16Jul2021.)



Theorem  zeo5 11814 
An integer is either even or odd, version of zeo3 11794
avoiding the negation
of the representation of an odd number. (Proposed by BJ, 21Jun2021.)
(Contributed by AV, 26Jun2020.)



Theorem  evend2 11815 
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 9288 and zeo2 9289. (Contributed by AV, 22Jun2021.)



Theorem  oddp1d2 11816 
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 9288 and zeo2 9289. (Contributed by AV, 22Jun2021.)



Theorem  zob 11817 
Alternate characterizations of an odd number. (Contributed by AV,
7Jun2020.)



Theorem  oddm1d2 11818 
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, 18Jun2021.) (Proof shortened by AV,
22Jun2021.)



Theorem  ltoddhalfle 11819 
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, 29Jun2021.)



Theorem  halfleoddlt 11820 
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,
1Jul2021.)



Theorem  opoe 11821 
The sum of two odds is even. (Contributed by Scott Fenton, 7Apr2014.)
(Revised by Mario Carneiro, 19Apr2014.)



Theorem  omoe 11822 
The difference of two odds is even. (Contributed by Scott Fenton,
7Apr2014.) (Revised by Mario Carneiro, 19Apr2014.)



Theorem  opeo 11823 
The sum of an odd and an even is odd. (Contributed by Scott Fenton,
7Apr2014.) (Revised by Mario Carneiro, 19Apr2014.)



Theorem  omeo 11824 
The difference of an odd and an even is odd. (Contributed by Scott
Fenton, 7Apr2014.) (Revised by Mario Carneiro, 19Apr2014.)



Theorem  m1expe 11825 
Exponentiation of 1 by an even power. Variant of m1expeven 10493.
(Contributed by AV, 25Jun2021.)



Theorem  m1expo 11826 
Exponentiation of 1 by an odd power. (Contributed by AV,
26Jun2021.)



Theorem  m1exp1 11827 
Exponentiation of negative one is one iff the exponent is even.
(Contributed by AV, 20Jun2021.)



Theorem  nn0enne 11828 
A positive integer is an even nonnegative integer iff it is an even
positive integer. (Contributed by AV, 30May2020.)



Theorem  nn0ehalf 11829 
The half of an even nonnegative integer is a nonnegative integer.
(Contributed by AV, 22Jun2020.) (Revised by AV, 28Jun2021.)



Theorem  nnehalf 11830 
The half of an even positive integer is a positive integer. (Contributed
by AV, 28Jun2021.)



Theorem  nn0o1gt2 11831 
An odd nonnegative integer is either 1 or greater than 2. (Contributed by
AV, 2Jun2020.)



Theorem  nno 11832 
An alternate characterization of an odd integer greater than 1.
(Contributed by AV, 2Jun2020.)



Theorem  nn0o 11833 
An alternate characterization of an odd nonnegative integer. (Contributed
by AV, 28May2020.) (Proof shortened by AV, 2Jun2020.)



Theorem  nn0ob 11834 
Alternate characterizations of an odd nonnegative integer. (Contributed
by AV, 4Jun2020.)



Theorem  nn0oddm1d2 11835 
A positive integer is odd iff its predecessor divided by 2 is a positive
integer. (Contributed by AV, 28Jun2021.)



Theorem  nnoddm1d2 11836 
A positive integer is odd iff its successor divided by 2 is a positive
integer. (Contributed by AV, 28Jun2021.)



Theorem  z0even 11837 
0 is even. (Contributed by AV, 11Feb2020.) (Revised by AV,
23Jun2021.)



Theorem  n2dvds1 11838 
2 does not divide 1 (common case). That means 1 is odd. (Contributed by
David A. Wheeler, 8Dec2018.)



Theorem  n2dvdsm1 11839 
2 does not divide 1. That means 1 is odd. (Contributed by AV,
15Aug2021.)



Theorem  z2even 11840 
2 is even. (Contributed by AV, 12Feb2020.) (Revised by AV,
23Jun2021.)



Theorem  n2dvds3 11841 
2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV,
28Feb2021.)



Theorem  z4even 11842 
4 is an even number. (Contributed by AV, 23Jul2020.) (Revised by AV,
4Jul2021.)



Theorem  4dvdseven 11843 
An integer which is divisible by 4 is an even integer. (Contributed by
AV, 4Jul2021.)



5.1.3 The division algorithm


Theorem  divalglemnn 11844* 
Lemma for divalg 11850. Existence for a positive denominator.
(Contributed by Jim Kingdon, 30Nov2021.)



Theorem  divalglemqt 11845 
Lemma for divalg 11850. The
case involved in
showing uniqueness.
(Contributed by Jim Kingdon, 5Dec2021.)



Theorem  divalglemnqt 11846 
Lemma for divalg 11850. The case
involved in showing uniqueness.
(Contributed by Jim Kingdon, 4Dec2021.)



Theorem  divalglemeunn 11847* 
Lemma for divalg 11850. Uniqueness for a positive denominator.
(Contributed by Jim Kingdon, 4Dec2021.)



Theorem  divalglemex 11848* 
Lemma for divalg 11850. The quotient and remainder exist.
(Contributed by
Jim Kingdon, 30Nov2021.)



Theorem  divalglemeuneg 11849* 
Lemma for divalg 11850. Uniqueness for a negative denominator.
(Contributed by Jim Kingdon, 4Dec2021.)



Theorem  divalg 11850* 
The division algorithm (theorem). Dividing an integer by a
nonzero integer produces a (unique) quotient and a unique
remainder . Theorem 1.14 in [ApostolNT]
p. 19. (Contributed by Paul Chapman, 21Mar2011.)



Theorem  divalgb 11851* 
Express the division algorithm as stated in divalg 11850 in terms of
.
(Contributed by Paul Chapman, 31Mar2011.)



Theorem  divalg2 11852* 
The division algorithm (theorem) for a positive divisor. (Contributed
by Paul Chapman, 21Mar2011.)



Theorem  divalgmod 11853 
The result of the operator satisfies the requirements for the
remainder in
the division algorithm for a positive divisor
(compare divalg2 11852 and divalgb 11851). This demonstration theorem
justifies the use of to yield an explicit remainder from this
point forward. (Contributed by Paul Chapman, 31Mar2011.) (Revised by
AV, 21Aug2021.)



Theorem  divalgmodcl 11854 
The result of the operator satisfies the requirements for the
remainder in the
division algorithm for a positive divisor. Variant
of divalgmod 11853. (Contributed by Stefan O'Rear,
17Oct2014.) (Proof
shortened by AV, 21Aug2021.)



Theorem  modremain 11855* 
The result of the modulo operation is the remainder of the division
algorithm. (Contributed by AV, 19Aug2021.)



Theorem  ndvdssub 11856 
Corollary of the division algorithm. If an integer greater than
divides , then it does not divide
any of ,
... . (Contributed by Paul
Chapman,
31Mar2011.)



Theorem  ndvdsadd 11857 
Corollary of the division algorithm. If an integer greater than
divides , then it does not divide
any of ,
... . (Contributed by Paul
Chapman,
31Mar2011.)



Theorem  ndvdsp1 11858 
Special case of ndvdsadd 11857. If an integer greater than
divides , it does
not divide . (Contributed by Paul
Chapman, 31Mar2011.)



Theorem  ndvdsi 11859 
A quick test for nondivisibility. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  flodddiv4 11860 
The floor of an odd integer divided by 4. (Contributed by AV,
17Jun2021.)



Theorem  fldivndvdslt 11861 
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, 4Jul2021.)



Theorem  flodddiv4lt 11862 
The floor of an odd number divided by 4 is less than the odd number
divided by 4. (Contributed by AV, 4Jul2021.)



Theorem  flodddiv4t2lthalf 11863 
The floor of an odd number divided by 4, multiplied by 2 is less than the
half of the odd number. (Contributed by AV, 4Jul2021.)



5.1.4 The greatest common divisor
operator


Syntax  cgcd 11864 
Extend the definition of a class to include the greatest common divisor
operator.



Definition  dfgcd 11865* 
Define the
operator. For example,
(exgcd 13475). (Contributed by Paul Chapman,
21Mar2011.)



Theorem  gcdmndc 11866 
Decidablity lemma used in various proofs related to .
(Contributed by Jim Kingdon, 12Dec2021.)

DECID 

Theorem  zsupcllemstep 11867* 
Lemma for zsupcl 11869. Induction step. (Contributed by Jim
Kingdon,
7Dec2021.)

DECID


Theorem  zsupcllemex 11868* 
Lemma for zsupcl 11869. Existence of the supremum. (Contributed
by Jim
Kingdon, 7Dec2021.)

DECID


Theorem  zsupcl 11869* 
Closure of supremum for decidable integer properties. The property
which defines the set we are taking the supremum of must (a) be true at
(which
corresponds to the nonempty condition of classical supremum
theorems), (b) decidable at each value after , and (c) be false
after (which
corresponds to the upper bound condition found in
classical supremum theorems). (Contributed by Jim Kingdon,
7Dec2021.)

DECID


Theorem  zssinfcl 11870* 
The infimum of a set of integers is an element of the set. (Contributed
by Jim Kingdon, 16Jan2022.)

inf inf 

Theorem  infssuzex 11871* 
Existence of the infimum of a subset of an upper set of integers.
(Contributed by Jim Kingdon, 13Jan2022.)

DECID


Theorem  infssuzledc 11872* 
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,
13Jan2022.)

DECID inf 

Theorem  infssuzcldc 11873* 
The infimum of a subset of an upper set of integers belongs to the
subset. (Contributed by Jim Kingdon, 20Jan2022.)

DECID inf 

Theorem  suprzubdc 11874* 
The supremum of a boundedabove decidable set of integers is greater
than any member of the set. (Contributed by Mario Carneiro,
21Apr2015.) (Revised by Jim Kingdon, 5Oct2024.)

DECID


Theorem  nninfdcex 11875* 
A decidable set of natural numbers has an infimum. (Contributed by Jim
Kingdon, 28Sep2024.)

DECID


Theorem  zsupssdc 11876* 
An inhabited decidable bounded subset of integers has a supremum in the
set. (The proof does not use axpresuploc 7866.) (Contributed by Mario
Carneiro, 21Apr2015.) (Revised by Jim Kingdon, 5Oct2024.)

DECID


Theorem  suprzcl2dc 11877* 
The supremum of a boundedabove decidable set of integers is a member of
the set. (This theorem avoids axpresuploc 7866.) (Contributed by Mario
Carneiro, 21Apr2015.) (Revised by Jim Kingdon, 6Oct2024.)

DECID


Theorem  dvdsbnd 11878* 
There is an upper bound to the divisors of a nonzero integer.
(Contributed by Jim Kingdon, 11Dec2021.)



Theorem  gcdsupex 11879* 
Existence of the supremum used in defining . (Contributed by
Jim Kingdon, 12Dec2021.)



Theorem  gcdsupcl 11880* 
Closure of the supremum used in defining . A lemma for gcdval 11881
and gcdn0cl 11884. (Contributed by Jim Kingdon, 11Dec2021.)



Theorem  gcdval 11881* 
The value of the
operator. is the greatest
common divisor of and . If
and are both ,
the result is defined conventionally as . (Contributed by Paul
Chapman, 21Mar2011.) (Revised by Mario Carneiro, 10Nov2013.)



Theorem  gcd0val 11882 
The value, by convention, of the operator when both operands are
0. (Contributed by Paul Chapman, 21Mar2011.)



Theorem  gcdn0val 11883* 
The value of the
operator when at least one operand is nonzero.
(Contributed by Paul Chapman, 21Mar2011.)



Theorem  gcdn0cl 11884 
Closure of the
operator. (Contributed by Paul Chapman,
21Mar2011.)



Theorem  gcddvds 11885 
The gcd of two integers divides each of them. (Contributed by Paul
Chapman, 21Mar2011.)



Theorem  dvdslegcd 11886 
An integer which divides both operands of the operator is
bounded by it. (Contributed by Paul Chapman, 21Mar2011.)



Theorem  nndvdslegcd 11887 
A positive integer which divides both positive operands of the
operator is bounded by it. (Contributed by AV, 9Aug2020.)



Theorem  gcdcl 11888 
Closure of the
operator. (Contributed by Paul Chapman,
21Mar2011.)



Theorem  gcdnncl 11889 
Closure of the
operator. (Contributed by Thierry Arnoux,
2Feb2020.)



Theorem  gcdcld 11890 
Closure of the
operator. (Contributed by Mario Carneiro,
29May2016.)



Theorem  gcd2n0cl 11891 
Closure of the
operator if the second operand is not 0.
(Contributed by AV, 10Jul2021.)



Theorem  zeqzmulgcd 11892* 
An integer is the product of an integer and the gcd of it and another
integer. (Contributed by AV, 11Jul2021.)



Theorem  divgcdz 11893 
An integer divided by the gcd of it and a nonzero integer is an integer.
(Contributed by AV, 11Jul2021.)



Theorem  gcdf 11894 
Domain and codomain of the operator. (Contributed by Paul
Chapman, 31Mar2011.) (Revised by Mario Carneiro, 16Nov2013.)



Theorem  gcdcom 11895 
The operator is
commutative. Theorem 1.4(a) in [ApostolNT]
p. 16. (Contributed by Paul Chapman, 21Mar2011.)



Theorem  gcdcomd 11896 
The operator is
commutative, deduction version. (Contributed by
SN, 24Aug2024.)



Theorem  divgcdnn 11897 
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10Jul2021.)



Theorem  divgcdnnr 11898 
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10Jul2021.)



Theorem  gcdeq0 11899 
The gcd of two integers is zero iff they are both zero. (Contributed by
Paul Chapman, 21Mar2011.)



Theorem  gcdn0gt0 11900 
The gcd of two integers is positive (nonzero) iff they are not both zero.
(Contributed by Paul Chapman, 22Jun2011.)

