Theorem List for Intuitionistic Logic Explorer - 8901-9000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zmulcl 8901 |
Closure of multiplication of integers. (Contributed by NM,
30-Jul-2004.)
|
    
  |
|
Theorem | zltp1le 8902 |
Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof
shortened by Mario Carneiro, 16-May-2014.)
|
     
   |
|
Theorem | zleltp1 8903 |
Integer ordering relation. (Contributed by NM, 10-May-2004.)
|
         |
|
Theorem | zlem1lt 8904 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
     
   |
|
Theorem | zltlem1 8905 |
Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
|
         |
|
Theorem | zgt0ge1 8906 |
An integer greater than
is greater than or equal to .
(Contributed by AV, 14-Oct-2018.)
|
     |
|
Theorem | nnleltp1 8907 |
Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
         |
|
Theorem | nnltp1le 8908 |
Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
|
     
   |
|
Theorem | nnaddm1cl 8909 |
Closure of addition of positive integers minus one. (Contributed by NM,
6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
      
  |
|
Theorem | nn0ltp1le 8910 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
|
         |
|
Theorem | nn0leltp1 8911 |
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10-Apr-2004.)
|
         |
|
Theorem | nn0ltlem1 8912 |
Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.)
(Proof shortened by Mario Carneiro, 16-May-2014.)
|
         |
|
Theorem | znn0sub 8913 |
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 8914.) (Contributed by NM, 14-Jul-2005.)
|
     
   |
|
Theorem | nn0sub 8914 |
Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
|
         |
|
Theorem | nn0n0n1ge2 8915 |
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 8916* |
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 8917 |
Alternate definition of the integers, based on elz2 8916.
(Contributed by
Mario Carneiro, 16-May-2014.)
|
     |
|
Theorem | nn0sub2 8918 |
Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
|
       |
|
Theorem | zapne 8919 |
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14-Mar-2020.)
|
    #    |
|
Theorem | zdceq 8920 |
Equality of integers is decidable. (Contributed by Jim Kingdon,
14-Mar-2020.)
|
   DECID
  |
|
Theorem | zdcle 8921 |
Integer is
decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
|
   DECID   |
|
Theorem | zdclt 8922 |
Integer is
decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|
   DECID   |
|
Theorem | zltlen 8923 |
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8204 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 14-Mar-2020.)
|
         |
|
Theorem | nn0n0n1ge2b 8924 |
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 8925 |
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22-Jun-2011.)
|
 
   |
|
Theorem | nn0lt2 8926 |
A nonnegative integer less than 2 must be 0 or 1. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
       |
|
Theorem | nn0le2is012 8927 |
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 8928 |
Nonnegative integer ordering relation. (Contributed by NM,
21-Jun-2005.)
|
         |
|
Theorem | nnlem1lt 8929 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
     
   |
|
Theorem | nnltlem1 8930 |
Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|
         |
|
Theorem | nnm1ge0 8931 |
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30-Oct-2018.)
|

    |
|
Theorem | nn0ge0div 8932 |
Division of a nonnegative integer by a positive number is not negative.
(Contributed by Alexander van der Vekens, 14-Apr-2018.)
|
  
    |
|
Theorem | zdiv 8933* |
Two ways to express " divides .
(Contributed by NM,
3-Oct-2008.)
|
      
     |
|
Theorem | zdivadd 8934 |
Property of divisibility: if divides
and then it divides
. (Contributed by NM, 3-Oct-2008.)
|
   
         
   |
|
Theorem | zdivmul 8935 |
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3-Oct-2008.)
|
   
         |
|
Theorem | zextle 8936* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
   
 
  |
|
Theorem | zextlt 8937* |
An extensionality-like property for integer ordering. (Contributed by
NM, 29-Oct-2005.)
|
   
 
  |
|
Theorem | recnz 8938 |
The reciprocal of a number greater than 1 is not an integer. (Contributed
by NM, 3-May-2005.)
|
  
    |
|
Theorem | btwnnz 8939 |
A number between an integer and its successor is not an integer.
(Contributed by NM, 3-May-2005.)
|
       |
|
Theorem | gtndiv 8940 |
A larger number does not divide a smaller positive integer. (Contributed
by NM, 3-May-2005.)
|
    
  |
|
Theorem | halfnz 8941 |
One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
|
   |
|
Theorem | 3halfnz 8942 |
Three halves is not an integer. (Contributed by AV, 2-Jun-2020.)
|
   |
|
Theorem | suprzclex 8943* |
The supremum of a set of integers is an element of the set.
(Contributed by Jim Kingdon, 20-Dec-2021.)
|
   
 
         
   |
|
Theorem | prime 8944* |
Two ways to express " is a prime number (or 1)." (Contributed by
NM, 4-May-2005.)
|
           
 
     |
|
Theorem | msqznn 8945 |
The square of a nonzero integer is a positive integer. (Contributed by
NM, 2-Aug-2004.)
|
  
    |
|
Theorem | zneo 8946 |
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 8947 |
A positive integer is even or odd. (Contributed by Jim Kingdon,
15-Mar-2020.)
|
      
    |
|
Theorem | nneo 8948 |
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 8949 |
A positive integer is even or odd but not both. (Contributed by NM,
20-Aug-2001.)
|
         |
|
Theorem | zeo 8950 |
An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
|
      
    |
|
Theorem | zeo2 8951 |
An integer is even or odd but not both. (Contributed by Mario Carneiro,
12-Sep-2015.)
|
      
    |
|
Theorem | peano2uz2 8952* |
Second Peano postulate for upper integers. (Contributed by NM,
3-Oct-2004.)
|
  
  
     |
|
Theorem | peano5uzti 8953* |
Peano's inductive postulate for upper integers. (Contributed by NM,
6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.)
|
     
  
   |
|
Theorem | peano5uzi 8954* |
Peano's inductive postulate for upper integers. (Contributed by NM,
6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.)
|
  

   
  |
|
Theorem | dfuzi 8955* |
An expression for the upper integers that start at that is
analogous to dfnn2 8522 for positive integers. (Contributed by NM,
6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
|
      
    |
|
Theorem | uzind 8956* |
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 8957* |
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 8958* |
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 8959* |
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 8960* |
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 8961* |
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 8962* |
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 8963* |
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 8964* |
Any real number can be sandwiched between two integers. Exercise 2 of
[Apostol] p. 28. (Contributed by NM,
10-Nov-2004.)
|
       |
|
Theorem | nn0zd 8965 |
A positive integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | nnzd 8966 |
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | zred 8967 |
An integer is a real number. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | zcnd 8968 |
An integer is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | znegcld 8969 |
Closure law for negative integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
      |
|
Theorem | peano2zd 8970 |
Deduction from second Peano postulate generalized to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | zaddcld 8971 |
Closure of addition of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | zsubcld 8972 |
Closure of subtraction of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | zmulcld 8973 |
Closure of multiplication of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
         |
|
Theorem | zadd2cl 8974 |
Increasing an integer by 2 results in an integer. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
     |
|
Theorem | btwnapz 8975 |
A number between an integer and its successor is apart from any integer.
(Contributed by Jim Kingdon, 6-Jan-2023.)
|
             #   |
|
3.4.10 Decimal arithmetic
|
|
Syntax | cdc 8976 |
Constant used for decimal constructor.
|
;  |
|
Definition | df-dec 8977 |
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base  . For example,
;;;   ;;;    ;;;   1kp2ke3k 12363.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV,
1-Aug-2021.)
|
;        |
|
Theorem | 9p1e10 8978 |
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 8979 |
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 8980 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
 ;
;   |
|
Theorem | deceq2 8981 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
 ;
;   |
|
Theorem | deceq1i 8982 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ;  |
|
Theorem | deceq2i 8983 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ;  |
|
Theorem | deceq12i 8984 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
; ;  |
|
Theorem | numnncl 8985 |
Closure for a numeral (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
   
 |
|
Theorem | num0u 8986 |
Add a zero in the units place. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
 
     |
|
Theorem | num0h 8987 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
     |
|
Theorem | numcl 8988 |
Closure for a decimal integer (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
  

 |
|
Theorem | numsuc 8989 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
    
        |
|
Theorem | deccl 8990 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | 10nn 8991 |
10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by
AV, 6-Sep-2021.)
|
;  |
|
Theorem | 10pos 8992 |
The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by
AV, 8-Sep-2021.)
|
;  |
|
Theorem | 10nn0 8993 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | 10re 8994 |
The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
8-Sep-2021.)
|
;  |
|
Theorem | decnncl 8995 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | dec0u 8996 |
Add a zero in the units place. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
; 
;  |
|
Theorem | dec0h 8997 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | numnncl2 8998 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9-Mar-2015.)
|
  
  |
|
Theorem | decnncl2 8999 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;  |
|
Theorem | numlt 9000 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
  
      |