Theorem List for Intuitionistic Logic Explorer - 9101-9200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zltp1le 9101 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | zleltp1 9102 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
|
|
Theorem | zlem1lt 9103 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
|
|
Theorem | zltlem1 9104 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
|
|
Theorem | zgt0ge1 9105 |
An integer greater than
is greater than or equal to .
(Contributed by AV, 14-Oct-2018.)
|
|
|
Theorem | nnleltp1 9106 |
Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nnltp1le 9107 |
Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
|
|
|
Theorem | nnaddm1cl 9108 |
Closure of addition of positive integers minus one. (Contributed by NM,
6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nn0ltp1le 9109 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nn0leltp1 9110 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Apr-2004.)
|
|
|
Theorem | nn0ltlem1 9111 |
Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | znn0sub 9112 |
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 9113.) (Contributed by NM, 14-Jul-2005.)
|
|
|
Theorem | nn0sub 9113 |
Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | nn0n0n1ge2 9114 |
A nonnegative integer which is neither 0 nor 1 is greater than or equal to
2. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
|
|
|
Theorem | elz2 9115* |
Membership in the set of integers. Commonly used in constructions of
the integers as equivalence classes under subtraction of the positive
integers. (Contributed by Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | dfz2 9116 |
Alternate definition of the integers, based on elz2 9115.
(Contributed by
Mario Carneiro, 16-May-2014.)
|
|
|
Theorem | nn0sub2 9117 |
Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
|
|
|
Theorem | zapne 9118 |
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14-Mar-2020.)
|
# |
|
Theorem | zdceq 9119 |
Equality of integers is decidable. (Contributed by Jim Kingdon,
14-Mar-2020.)
|
DECID
|
|
Theorem | zdcle 9120 |
Integer is
decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
|
DECID |
|
Theorem | zdclt 9121 |
Integer is
decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|
DECID |
|
Theorem | zltlen 9122 |
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8387 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 14-Mar-2020.)
|
|
|
Theorem | nn0n0n1ge2b 9123 |
A nonnegative integer is neither 0 nor 1 if and only if it is greater than
or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
|
|
|
Theorem | nn0lt10b 9124 |
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22-Jun-2011.)
|
|
|
Theorem | nn0lt2 9125 |
A nonnegative integer less than 2 must be 0 or 1. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
|
|
Theorem | nn0le2is012 9126 |
A nonnegative integer which is less than or equal to 2 is either 0 or 1 or
2. (Contributed by AV, 16-Mar-2019.)
|
|
|
Theorem | nn0lem1lt 9127 |
Nonnegative integer ordering relation. (Contributed by NM,
21-Jun-2005.)
|
|
|
Theorem | nnlem1lt 9128 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
|
|
Theorem | nnltlem1 9129 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
|
|
Theorem | nnm1ge0 9130 |
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30-Oct-2018.)
|
|
|
Theorem | nn0ge0div 9131 |
Division of a nonnegative integer by a positive number is not negative.
(Contributed by Alexander van der Vekens, 14-Apr-2018.)
|
|
|
Theorem | zdiv 9132* |
Two ways to express " divides .
(Contributed by NM,
3-Oct-2008.)
|
|
|
Theorem | zdivadd 9133 |
Property of divisibility: if divides
and then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
|
Theorem | zdivmul 9134 |
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
|
Theorem | zextle 9135* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
|
|
Theorem | zextlt 9136* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
|
|
Theorem | recnz 9137 |
The reciprocal of a number greater than 1 is not an integer. (Contributed
by NM, 3-May-2005.)
|
|
|
Theorem | btwnnz 9138 |
A number between an integer and its successor is not an integer.
(Contributed by NM, 3-May-2005.)
|
|
|
Theorem | gtndiv 9139 |
A larger number does not divide a smaller positive integer. (Contributed
by NM, 3-May-2005.)
|
|
|
Theorem | halfnz 9140 |
One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
|
|
|
Theorem | 3halfnz 9141 |
Three halves is not an integer. (Contributed by AV, 2-Jun-2020.)
|
|
|
Theorem | suprzclex 9142* |
The supremum of a set of integers is an element of the set.
(Contributed by Jim Kingdon, 20-Dec-2021.)
|
|
|
Theorem | prime 9143* |
Two ways to express " is a prime number (or 1)." (Contributed by
NM, 4-May-2005.)
|
|
|
Theorem | msqznn 9144 |
The square of a nonzero integer is a positive integer. (Contributed by
NM, 2-Aug-2004.)
|
|
|
Theorem | zneo 9145 |
No even integer equals an odd integer (i.e. no integer can be both even
and odd). Exercise 10(a) of [Apostol] p.
28. (Contributed by NM,
31-Jul-2004.) (Proof shortened by Mario Carneiro, 18-May-2014.)
|
|
|
Theorem | nneoor 9146 |
A positive integer is even or odd. (Contributed by Jim Kingdon,
15-Mar-2020.)
|
|
|
Theorem | nneo 9147 |
A positive integer is even or odd but not both. (Contributed by NM,
1-Jan-2006.) (Proof shortened by Mario Carneiro, 18-May-2014.)
|
|
|
Theorem | nneoi 9148 |
A positive integer is even or odd but not both. (Contributed by NM,
20-Aug-2001.)
|
|
|
Theorem | zeo 9149 |
An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
|
|
|
Theorem | zeo2 9150 |
An integer is even or odd but not both. (Contributed by Mario Carneiro,
12-Sep-2015.)
|
|
|
Theorem | peano2uz2 9151* |
Second Peano postulate for upper integers. (Contributed by NM,
3-Oct-2004.)
|
|
|
Theorem | peano5uzti 9152* |
Peano's inductive postulate for upper integers. (Contributed by NM,
6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.)
|
|
|
Theorem | peano5uzi 9153* |
Peano's inductive postulate for upper integers. (Contributed by NM,
6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.)
|
|
|
Theorem | dfuzi 9154* |
An expression for the upper integers that start at that is
analogous to dfnn2 8715 for positive integers. (Contributed by NM,
6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
|
|
|
Theorem | uzind 9155* |
Induction on the upper integers that start at . The first four
hypotheses give us the substitution instances we need; the last two are
the basis and the induction step. (Contributed by NM, 5-Jul-2005.)
|
|
|
Theorem | uzind2 9156* |
Induction on the upper integers that start after an integer .
The first four hypotheses give us the substitution instances we need;
the last two are the basis and the induction step. (Contributed by NM,
25-Jul-2005.)
|
|
|
Theorem | uzind3 9157* |
Induction on the upper integers that start at an integer . The
first four hypotheses give us the substitution instances we need, and
the last two are the basis and the induction step. (Contributed by NM,
26-Jul-2005.)
|
|
|
Theorem | nn0ind 9158* |
Principle of Mathematical Induction (inference schema) on nonnegative
integers. The first four hypotheses give us the substitution instances
we need; the last two are the basis and the induction step.
(Contributed by NM, 13-May-2004.)
|
|
|
Theorem | fzind 9159* |
Induction on the integers from to
inclusive . The first
four hypotheses give us the substitution instances we need; the last two
are the basis and the induction step. (Contributed by Paul Chapman,
31-Mar-2011.)
|
|
|
Theorem | fnn0ind 9160* |
Induction on the integers from to
inclusive . The first
four hypotheses give us the substitution instances we need; the last two
are the basis and the induction step. (Contributed by Paul Chapman,
31-Mar-2011.)
|
|
|
Theorem | nn0ind-raph 9161* |
Principle of Mathematical Induction (inference schema) on nonnegative
integers. The first four hypotheses give us the substitution instances
we need; the last two are the basis and the induction step. Raph Levien
remarks: "This seems a bit painful. I wonder if an explicit
substitution version would be easier." (Contributed by Raph
Levien,
10-Apr-2004.)
|
|
|
Theorem | zindd 9162* |
Principle of Mathematical Induction on all integers, deduction version.
The first five hypotheses give the substitutions; the last three are the
basis, the induction, and the extension to negative numbers.
(Contributed by Paul Chapman, 17-Apr-2009.) (Proof shortened by Mario
Carneiro, 4-Jan-2017.)
|
|
|
Theorem | btwnz 9163* |
Any real number can be sandwiched between two integers. Exercise 2 of
[Apostol] p. 28. (Contributed by NM,
10-Nov-2004.)
|
|
|
Theorem | nn0zd 9164 |
A positive integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | nnzd 9165 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zred 9166 |
An integer is a real number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zcnd 9167 |
An integer is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | znegcld 9168 |
Closure law for negative integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | peano2zd 9169 |
Deduction from second Peano postulate generalized to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | zaddcld 9170 |
Closure of addition of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zsubcld 9171 |
Closure of subtraction of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zmulcld 9172 |
Closure of multiplication of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zadd2cl 9173 |
Increasing an integer by 2 results in an integer. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
|
|
Theorem | btwnapz 9174 |
A number between an integer and its successor is apart from any integer.
(Contributed by Jim Kingdon, 6-Jan-2023.)
|
# |
|
4.4.10 Decimal arithmetic
|
|
Syntax | cdc 9175 |
Constant used for decimal constructor.
|
; |
|
Definition | df-dec 9176 |
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base . For example,
;;; ;;; ;;; 1kp2ke3k 12925.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV,
1-Aug-2021.)
|
; |
|
Theorem | 9p1e10 9177 |
9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by
Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.)
|
; |
|
Theorem | dfdec10 9178 |
Version of the definition of the "decimal constructor" using ;
instead of the symbol 10. Of course, this statement cannot be used as
definition, because it uses the "decimal constructor".
(Contributed by
AV, 1-Aug-2021.)
|
; ;
|
|
Theorem | deceq1 9179 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | deceq2 9180 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | deceq1i 9181 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ; |
|
Theorem | deceq2i 9182 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ; |
|
Theorem | deceq12i 9183 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ; |
|
Theorem | numnncl 9184 |
Closure for a numeral (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | num0u 9185 |
Add a zero in the units place. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | num0h 9186 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | numcl 9187 |
Closure for a decimal integer (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numsuc 9188 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | deccl 9189 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 10nn 9190 |
10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by
AV, 6-Sep-2021.)
|
; |
|
Theorem | 10pos 9191 |
The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by
AV, 8-Sep-2021.)
|
; |
|
Theorem | 10nn0 9192 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 10re 9193 |
The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
8-Sep-2021.)
|
; |
|
Theorem | decnncl 9194 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | dec0u 9195 |
Add a zero in the units place. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | dec0h 9196 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | numnncl2 9197 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9-Mar-2015.)
|
|
|
Theorem | decnncl2 9198 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | numlt 9199 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numltc 9200 |
Comparing two decimal integers (unequal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|