Theorem List for Intuitionistic Logic Explorer - 9101-9200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nn0le2is012 9101 |
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 9102 |
Nonnegative integer ordering relation. (Contributed by NM,
21-Jun-2005.)
|
|
|
Theorem | nnlem1lt 9103 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
|
|
Theorem | nnltlem1 9104 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
|
|
Theorem | nnm1ge0 9105 |
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30-Oct-2018.)
|
|
|
Theorem | nn0ge0div 9106 |
Division of a nonnegative integer by a positive number is not negative.
(Contributed by Alexander van der Vekens, 14-Apr-2018.)
|
|
|
Theorem | zdiv 9107* |
Two ways to express " divides .
(Contributed by NM,
3-Oct-2008.)
|
|
|
Theorem | zdivadd 9108 |
Property of divisibility: if divides
and then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
|
Theorem | zdivmul 9109 |
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3-Oct-2008.)
|
|
|
Theorem | zextle 9110* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
|
|
Theorem | zextlt 9111* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
|
|
Theorem | recnz 9112 |
The reciprocal of a number greater than 1 is not an integer. (Contributed
by NM, 3-May-2005.)
|
|
|
Theorem | btwnnz 9113 |
A number between an integer and its successor is not an integer.
(Contributed by NM, 3-May-2005.)
|
|
|
Theorem | gtndiv 9114 |
A larger number does not divide a smaller positive integer. (Contributed
by NM, 3-May-2005.)
|
|
|
Theorem | halfnz 9115 |
One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
|
|
|
Theorem | 3halfnz 9116 |
Three halves is not an integer. (Contributed by AV, 2-Jun-2020.)
|
|
|
Theorem | suprzclex 9117* |
The supremum of a set of integers is an element of the set.
(Contributed by Jim Kingdon, 20-Dec-2021.)
|
|
|
Theorem | prime 9118* |
Two ways to express " is a prime number (or 1)." (Contributed by
NM, 4-May-2005.)
|
|
|
Theorem | msqznn 9119 |
The square of a nonzero integer is a positive integer. (Contributed by
NM, 2-Aug-2004.)
|
|
|
Theorem | zneo 9120 |
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 9121 |
A positive integer is even or odd. (Contributed by Jim Kingdon,
15-Mar-2020.)
|
|
|
Theorem | nneo 9122 |
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 9123 |
A positive integer is even or odd but not both. (Contributed by NM,
20-Aug-2001.)
|
|
|
Theorem | zeo 9124 |
An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
|
|
|
Theorem | zeo2 9125 |
An integer is even or odd but not both. (Contributed by Mario Carneiro,
12-Sep-2015.)
|
|
|
Theorem | peano2uz2 9126* |
Second Peano postulate for upper integers. (Contributed by NM,
3-Oct-2004.)
|
|
|
Theorem | peano5uzti 9127* |
Peano's inductive postulate for upper integers. (Contributed by NM,
6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.)
|
|
|
Theorem | peano5uzi 9128* |
Peano's inductive postulate for upper integers. (Contributed by NM,
6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.)
|
|
|
Theorem | dfuzi 9129* |
An expression for the upper integers that start at that is
analogous to dfnn2 8690 for positive integers. (Contributed by NM,
6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
|
|
|
Theorem | uzind 9130* |
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 9131* |
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 9132* |
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 9133* |
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 9134* |
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 9135* |
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 9136* |
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 9137* |
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 9138* |
Any real number can be sandwiched between two integers. Exercise 2 of
[Apostol] p. 28. (Contributed by NM,
10-Nov-2004.)
|
|
|
Theorem | nn0zd 9139 |
A positive integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | nnzd 9140 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zred 9141 |
An integer is a real number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zcnd 9142 |
An integer is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | znegcld 9143 |
Closure law for negative integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | peano2zd 9144 |
Deduction from second Peano postulate generalized to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | zaddcld 9145 |
Closure of addition of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zsubcld 9146 |
Closure of subtraction of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zmulcld 9147 |
Closure of multiplication of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | zadd2cl 9148 |
Increasing an integer by 2 results in an integer. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
|
|
Theorem | btwnapz 9149 |
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 9150 |
Constant used for decimal constructor.
|
; |
|
Definition | df-dec 9151 |
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base . For example,
;;; ;;; ;;; 1kp2ke3k 12863.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV,
1-Aug-2021.)
|
; |
|
Theorem | 9p1e10 9152 |
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 9153 |
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 9154 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | deceq2 9155 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | deceq1i 9156 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ; |
|
Theorem | deceq2i 9157 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ; |
|
Theorem | deceq12i 9158 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ; |
|
Theorem | numnncl 9159 |
Closure for a numeral (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | num0u 9160 |
Add a zero in the units place. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | num0h 9161 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | numcl 9162 |
Closure for a decimal integer (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numsuc 9163 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | deccl 9164 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 10nn 9165 |
10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by
AV, 6-Sep-2021.)
|
; |
|
Theorem | 10pos 9166 |
The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by
AV, 8-Sep-2021.)
|
; |
|
Theorem | 10nn0 9167 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 10re 9168 |
The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
8-Sep-2021.)
|
; |
|
Theorem | decnncl 9169 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | dec0u 9170 |
Add a zero in the units place. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | dec0h 9171 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | numnncl2 9172 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9-Mar-2015.)
|
|
|
Theorem | decnncl2 9173 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | numlt 9174 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numltc 9175 |
Comparing two decimal integers (unequal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | le9lt10 9176 |
A "decimal digit" (i.e. a nonnegative integer less than or equal to
9)
is less then 10. (Contributed by AV, 8-Sep-2021.)
|
; |
|
Theorem | declt 9177 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; ; |
|
Theorem | decltc 9178 |
Comparing two decimal integers (unequal higher places). (Contributed
by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ; ; |
|
Theorem | declth 9179 |
Comparing two decimal integers (unequal higher places). (Contributed
by AV, 8-Sep-2021.)
|
; ; |
|
Theorem | decsuc 9180 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; ; |
|
Theorem | 3declth 9181 |
Comparing two decimal integers with three "digits" (unequal higher
places). (Contributed by AV, 8-Sep-2021.)
|
;;
;; |
|
Theorem | 3decltc 9182 |
Comparing two decimal integers with three "digits" (unequal higher
places). (Contributed by AV, 15-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
;
; ;; ;; |
|
Theorem | decle 9183 |
Comparing two decimal integers (equal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
; ; |
|
Theorem | decleh 9184 |
Comparing two decimal integers (unequal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
; ; |
|
Theorem | declei 9185 |
Comparing a digit to a decimal integer. (Contributed by AV,
17-Aug-2021.)
|
; |
|
Theorem | numlti 9186 |
Comparing a digit to a decimal integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | declti 9187 |
Comparing a digit to a decimal integer. (Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | decltdi 9188 |
Comparing a digit to a decimal integer. (Contributed by AV,
8-Sep-2021.)
|
; |
|
Theorem | numsucc 9189 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | decsucc 9190 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ; |
|
Theorem | 1e0p1 9191 |
The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | dec10p 9192 |
Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;
; |
|
Theorem | numma 9193 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | nummac 9194 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numma2c 9195 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numadd 9196 |
Add two decimal integers and (no
carry). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numaddc 9197 |
Add two decimal integers and (with
carry). (Contributed
by Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | nummul1c 9198 |
The product of a decimal integer with a number. (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | nummul2c 9199 |
The product of a decimal integer with a number (with carry).
(Contributed by Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | decma 9200 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(no carry). (Contributed by Mario Carneiro,
18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
; ;
; |