Theorem List for Intuitionistic Logic Explorer - 11801-11900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | oddm1even 11801 |
An integer is odd iff its predecessor is even. (Contributed by Mario
Carneiro, 5-Sep-2016.)
|
|
|
Theorem | oddp1even 11802 |
An integer is odd iff its successor is even. (Contributed by Mario
Carneiro, 5-Sep-2016.)
|
|
|
Theorem | oexpneg 11803 |
The exponential of the negative of a number, when the exponent is odd.
(Contributed by Mario Carneiro, 25-Apr-2015.)
|
|
|
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, 21-Jul-2021.)
|
|
|
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, 24-May-2020.)
|
|
|
Theorem | oddnn02np1 11806* |
A nonnegative integer is odd iff it is one plus twice another
nonnegative integer. (Contributed by AV, 19-Jun-2021.)
|
|
|
Theorem | oddge22np1 11807* |
An integer greater than one is odd iff it is one plus twice a positive
integer. (Contributed by AV, 16-Aug-2021.)
|
|
|
Theorem | evennn02n 11808* |
A nonnegative integer is even iff it is twice another nonnegative
integer. (Contributed by AV, 12-Aug-2021.)
|
|
|
Theorem | evennn2n 11809* |
A positive integer is even iff it is twice another positive integer.
(Contributed by AV, 12-Aug-2021.)
|
|
|
Theorem | 2tp1odd 11810 |
A number which is twice an integer increased by 1 is odd. (Contributed
by AV, 16-Jul-2021.)
|
|
|
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, 19-Jul-2021.)
|
|
|
Theorem | sqoddm1div8z 11812 |
A squared odd number minus 1 divided by 8 is an integer. (Contributed
by AV, 19-Jul-2021.)
|
|
|
Theorem | 2teven 11813 |
A number which is twice an integer is even. (Contributed by AV,
16-Jul-2021.)
|
|
|
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, 21-Jun-2021.)
(Contributed by AV, 26-Jun-2020.)
|
|
|
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, 22-Jun-2021.)
|
|
|
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, 22-Jun-2021.)
|
|
|
Theorem | zob 11817 |
Alternate characterizations of an odd number. (Contributed by AV,
7-Jun-2020.)
|
|
|
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, 18-Jun-2021.) (Proof shortened by AV,
22-Jun-2021.)
|
|
|
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, 29-Jun-2021.)
|
|
|
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,
1-Jul-2021.)
|
|
|
Theorem | opoe 11821 |
The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | omoe 11822 |
The difference of two odds is even. (Contributed by Scott Fenton,
7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | opeo 11823 |
The sum of an odd and an even is odd. (Contributed by Scott Fenton,
7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | omeo 11824 |
The difference of an odd and an even is odd. (Contributed by Scott
Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | m1expe 11825 |
Exponentiation of -1 by an even power. Variant of m1expeven 10493.
(Contributed by AV, 25-Jun-2021.)
|
|
|
Theorem | m1expo 11826 |
Exponentiation of -1 by an odd power. (Contributed by AV,
26-Jun-2021.)
|
|
|
Theorem | m1exp1 11827 |
Exponentiation of negative one is one iff the exponent is even.
(Contributed by AV, 20-Jun-2021.)
|
|
|
Theorem | nn0enne 11828 |
A positive integer is an even nonnegative integer iff it is an even
positive integer. (Contributed by AV, 30-May-2020.)
|
|
|
Theorem | nn0ehalf 11829 |
The half of an even nonnegative integer is a nonnegative integer.
(Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.)
|
|
|
Theorem | nnehalf 11830 |
The half of an even positive integer is a positive integer. (Contributed
by AV, 28-Jun-2021.)
|
|
|
Theorem | nn0o1gt2 11831 |
An odd nonnegative integer is either 1 or greater than 2. (Contributed by
AV, 2-Jun-2020.)
|
|
|
Theorem | nno 11832 |
An alternate characterization of an odd integer greater than 1.
(Contributed by AV, 2-Jun-2020.)
|
|
|
Theorem | nn0o 11833 |
An alternate characterization of an odd nonnegative integer. (Contributed
by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
|
|
|
Theorem | nn0ob 11834 |
Alternate characterizations of an odd nonnegative integer. (Contributed
by AV, 4-Jun-2020.)
|
|
|
Theorem | nn0oddm1d2 11835 |
A positive integer is odd iff its predecessor divided by 2 is a positive
integer. (Contributed by AV, 28-Jun-2021.)
|
|
|
Theorem | nnoddm1d2 11836 |
A positive integer is odd iff its successor divided by 2 is a positive
integer. (Contributed by AV, 28-Jun-2021.)
|
|
|
Theorem | z0even 11837 |
0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
|
|
Theorem | n2dvds1 11838 |
2 does not divide 1 (common case). That means 1 is odd. (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
|
|
Theorem | n2dvdsm1 11839 |
2 does not divide -1. That means -1 is odd. (Contributed by AV,
15-Aug-2021.)
|
|
|
Theorem | z2even 11840 |
2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
|
|
Theorem | n2dvds3 11841 |
2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV,
28-Feb-2021.)
|
|
|
Theorem | z4even 11842 |
4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV,
4-Jul-2021.)
|
|
|
Theorem | 4dvdseven 11843 |
An integer which is divisible by 4 is an even integer. (Contributed by
AV, 4-Jul-2021.)
|
|
|
5.1.3 The division algorithm
|
|
Theorem | divalglemnn 11844* |
Lemma for divalg 11850. Existence for a positive denominator.
(Contributed by Jim Kingdon, 30-Nov-2021.)
|
|
|
Theorem | divalglemqt 11845 |
Lemma for divalg 11850. The
case involved in
showing uniqueness.
(Contributed by Jim Kingdon, 5-Dec-2021.)
|
|
|
Theorem | divalglemnqt 11846 |
Lemma for divalg 11850. The case
involved in showing uniqueness.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
|
|
Theorem | divalglemeunn 11847* |
Lemma for divalg 11850. Uniqueness for a positive denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
|
|
Theorem | divalglemex 11848* |
Lemma for divalg 11850. The quotient and remainder exist.
(Contributed by
Jim Kingdon, 30-Nov-2021.)
|
|
|
Theorem | divalglemeuneg 11849* |
Lemma for divalg 11850. Uniqueness for a negative denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
|
|
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, 21-Mar-2011.)
|
|
|
Theorem | divalgb 11851* |
Express the division algorithm as stated in divalg 11850 in terms of
.
(Contributed by Paul Chapman, 31-Mar-2011.)
|
|
|
Theorem | divalg2 11852* |
The division algorithm (theorem) for a positive divisor. (Contributed
by Paul Chapman, 21-Mar-2011.)
|
|
|
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, 31-Mar-2011.) (Revised by
AV, 21-Aug-2021.)
|
|
|
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,
17-Oct-2014.) (Proof
shortened by AV, 21-Aug-2021.)
|
|
|
Theorem | modremain 11855* |
The result of the modulo operation is the remainder of the division
algorithm. (Contributed by AV, 19-Aug-2021.)
|
|
|
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,
31-Mar-2011.)
|
|
|
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,
31-Mar-2011.)
|
|
|
Theorem | ndvdsp1 11858 |
Special case of ndvdsadd 11857. If an integer greater than
divides , it does
not divide . (Contributed by Paul
Chapman, 31-Mar-2011.)
|
|
|
Theorem | ndvdsi 11859 |
A quick test for non-divisibility. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | flodddiv4 11860 |
The floor of an odd integer divided by 4. (Contributed by AV,
17-Jun-2021.)
|
|
|
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, 4-Jul-2021.)
|
|
|
Theorem | flodddiv4lt 11862 |
The floor of an odd number divided by 4 is less than the odd number
divided by 4. (Contributed by AV, 4-Jul-2021.)
|
|
|
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, 4-Jul-2021.)
|
|
|
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 | df-gcd 11865* |
Define the
operator. For example,
(ex-gcd 13475). (Contributed by Paul Chapman,
21-Mar-2011.)
|
|
|
Theorem | gcdmndc 11866 |
Decidablity lemma used in various proofs related to .
(Contributed by Jim Kingdon, 12-Dec-2021.)
|
DECID |
|
Theorem | zsupcllemstep 11867* |
Lemma for zsupcl 11869. Induction step. (Contributed by Jim
Kingdon,
7-Dec-2021.)
|
DECID
|
|
Theorem | zsupcllemex 11868* |
Lemma for zsupcl 11869. Existence of the supremum. (Contributed
by Jim
Kingdon, 7-Dec-2021.)
|
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,
7-Dec-2021.)
|
DECID
|
|
Theorem | zssinfcl 11870* |
The infimum of a set of integers is an element of the set. (Contributed
by Jim Kingdon, 16-Jan-2022.)
|
inf inf |
|
Theorem | infssuzex 11871* |
Existence of the infimum of a subset of an upper set of integers.
(Contributed by Jim Kingdon, 13-Jan-2022.)
|
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,
13-Jan-2022.)
|
DECID inf |
|
Theorem | infssuzcldc 11873* |
The infimum of a subset of an upper set of integers belongs to the
subset. (Contributed by Jim Kingdon, 20-Jan-2022.)
|
DECID inf |
|
Theorem | suprzubdc 11874* |
The supremum of a bounded-above decidable set of integers is greater
than any member of the set. (Contributed by Mario Carneiro,
21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|
DECID
|
|
Theorem | nninfdcex 11875* |
A decidable set of natural numbers has an infimum. (Contributed by Jim
Kingdon, 28-Sep-2024.)
|
DECID
|
|
Theorem | zsupssdc 11876* |
An inhabited decidable bounded subset of integers has a supremum in the
set. (The proof does not use ax-pre-suploc 7866.) (Contributed by Mario
Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|
DECID
|
|
Theorem | suprzcl2dc 11877* |
The supremum of a bounded-above decidable set of integers is a member of
the set. (This theorem avoids ax-pre-suploc 7866.) (Contributed by Mario
Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
|
DECID
|
|
Theorem | dvdsbnd 11878* |
There is an upper bound to the divisors of a nonzero integer.
(Contributed by Jim Kingdon, 11-Dec-2021.)
|
|
|
Theorem | gcdsupex 11879* |
Existence of the supremum used in defining . (Contributed by
Jim Kingdon, 12-Dec-2021.)
|
|
|
Theorem | gcdsupcl 11880* |
Closure of the supremum used in defining . A lemma for gcdval 11881
and gcdn0cl 11884. (Contributed by Jim Kingdon, 11-Dec-2021.)
|
|
|
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, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
|
|
Theorem | gcd0val 11882 |
The value, by convention, of the operator when both operands are
0. (Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | gcdn0val 11883* |
The value of the
operator when at least one operand is nonzero.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | gcdn0cl 11884 |
Closure of the
operator. (Contributed by Paul Chapman,
21-Mar-2011.)
|
|
|
Theorem | gcddvds 11885 |
The gcd of two integers divides each of them. (Contributed by Paul
Chapman, 21-Mar-2011.)
|
|
|
Theorem | dvdslegcd 11886 |
An integer which divides both operands of the operator is
bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | nndvdslegcd 11887 |
A positive integer which divides both positive operands of the
operator is bounded by it. (Contributed by AV, 9-Aug-2020.)
|
|
|
Theorem | gcdcl 11888 |
Closure of the
operator. (Contributed by Paul Chapman,
21-Mar-2011.)
|
|
|
Theorem | gcdnncl 11889 |
Closure of the
operator. (Contributed by Thierry Arnoux,
2-Feb-2020.)
|
|
|
Theorem | gcdcld 11890 |
Closure of the
operator. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | gcd2n0cl 11891 |
Closure of the
operator if the second operand is not 0.
(Contributed by AV, 10-Jul-2021.)
|
|
|
Theorem | zeqzmulgcd 11892* |
An integer is the product of an integer and the gcd of it and another
integer. (Contributed by AV, 11-Jul-2021.)
|
|
|
Theorem | divgcdz 11893 |
An integer divided by the gcd of it and a nonzero integer is an integer.
(Contributed by AV, 11-Jul-2021.)
|
|
|
Theorem | gcdf 11894 |
Domain and codomain of the operator. (Contributed by Paul
Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
|
|
Theorem | gcdcom 11895 |
The operator is
commutative. Theorem 1.4(a) in [ApostolNT]
p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | gcdcomd 11896 |
The operator is
commutative, deduction version. (Contributed by
SN, 24-Aug-2024.)
|
|
|
Theorem | divgcdnn 11897 |
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10-Jul-2021.)
|
|
|
Theorem | divgcdnnr 11898 |
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10-Jul-2021.)
|
|
|
Theorem | gcdeq0 11899 |
The gcd of two integers is zero iff they are both zero. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | gcdn0gt0 11900 |
The gcd of two integers is positive (nonzero) iff they are not both zero.
(Contributed by Paul Chapman, 22-Jun-2011.)
|
|