Theorem List for Intuitionistic Logic Explorer - 9001-9100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | divfnzn 9001 |
Division restricted to is a function. Given
excluded
middle, it would be easy to prove this for     .
The key difference is that an element of is apart from zero,
whereas being an element of
  implies being not equal to
zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|
      |
|
Theorem | elq 9002* |
Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.)
(Revised by Mario Carneiro, 28-Jan-2014.)
|
 
     |
|
Theorem | qmulz 9003* |
If is rational, then
some integer multiple of it is an integer.
(Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro,
22-Jul-2014.)
|
  

  |
|
Theorem | znq 9004 |
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12-Jan-2002.)
|
    
  |
|
Theorem | qre 9005 |
A rational number is a real number. (Contributed by NM,
14-Nov-2002.)
|
   |
|
Theorem | zq 9006 |
An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
|
   |
|
Theorem | zssq 9007 |
The integers are a subset of the rationals. (Contributed by NM,
9-Jan-2002.)
|
 |
|
Theorem | nn0ssq 9008 |
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31-Jul-2004.)
|
 |
|
Theorem | nnssq 9009 |
The positive integers are a subset of the rationals. (Contributed by NM,
31-Jul-2004.)
|
 |
|
Theorem | qssre 9010 |
The rationals are a subset of the reals. (Contributed by NM,
9-Jan-2002.)
|
 |
|
Theorem | qsscn 9011 |
The rationals are a subset of the complex numbers. (Contributed by NM,
2-Aug-2004.)
|
 |
|
Theorem | qex 9012 |
The set of rational numbers exists. (Contributed by NM, 30-Jul-2004.)
(Revised by Mario Carneiro, 17-Nov-2014.)
|
 |
|
Theorem | nnq 9013 |
A positive integer is rational. (Contributed by NM, 17-Nov-2004.)
|
   |
|
Theorem | qcn 9014 |
A rational number is a complex number. (Contributed by NM,
2-Aug-2004.)
|
   |
|
Theorem | qaddcl 9015 |
Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.)
|
    
  |
|
Theorem | qnegcl 9016 |
Closure law for the negative of a rational. (Contributed by NM,
2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.)
|
    |
|
Theorem | qmulcl 9017 |
Closure of multiplication of rationals. (Contributed by NM,
1-Aug-2004.)
|
    
  |
|
Theorem | qsubcl 9018 |
Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.)
|
    
  |
|
Theorem | qapne 9019 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 20-Mar-2020.)
|
    #    |
|
Theorem | qltlen 9020 |
Rational 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 8007 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 11-Oct-2021.)
|
         |
|
Theorem | qlttri2 9021 |
Apartness is equivalent to not equal for rationals. (Contributed by Jim
Kingdon, 9-Nov-2021.)
|
         |
|
Theorem | qreccl 9022 |
Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.)
|
  
    |
|
Theorem | qdivcl 9023 |
Closure of division of rationals. (Contributed by NM, 3-Aug-2004.)
|
    
  |
|
Theorem | qrevaddcl 9024 |
Reverse closure law for addition of rationals. (Contributed by NM,
2-Aug-2004.)
|
    
    |
|
Theorem | nnrecq 9025 |
The reciprocal of a positive integer is rational. (Contributed by NM,
17-Nov-2004.)
|
  
  |
|
Theorem | irradd 9026 |
The sum of an irrational number and a rational number is irrational.
(Contributed by NM, 7-Nov-2008.)
|
  
   
    |
|
Theorem | irrmul 9027 |
The product of a real which is not rational with a nonzero rational is not
rational. Note that by "not rational" we mean the negation of
"is
rational" (whereas "irrational" is often defined to mean
apart from any
rational number - given excluded middle these two definitions would be
equivalent). (Contributed by NM, 7-Nov-2008.)
|
  
  

    |
|
3.4.13 Complex numbers as pairs of
reals
|
|
Theorem | cnref1o 9028* |
There is a natural one-to-one mapping from 
 to ,
where we map    to     . In our
construction of the complex numbers, this is in fact our
definition of
(see df-c 7259), but in the axiomatic treatment we can only
show
that there is the expected mapping between these two sets. (Contributed
by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro,
17-Feb-2014.)
|
   
          |
|
3.5 Order sets
|
|
3.5.1 Positive reals (as a subset of complex
numbers)
|
|
Syntax | crp 9029 |
Extend class notation to include the class of positive reals.
|
 |
|
Definition | df-rp 9030 |
Define the set of positive reals. Definition of positive numbers in
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
   |
|
Theorem | elrp 9031 |
Membership in the set of positive reals. (Contributed by NM,
27-Oct-2007.)
|
 
   |
|
Theorem | elrpii 9032 |
Membership in the set of positive reals. (Contributed by NM,
23-Feb-2008.)
|
 |
|
Theorem | 1rp 9033 |
1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
|
 |
|
Theorem | 2rp 9034 |
2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|
 |
|
Theorem | rpre 9035 |
A positive real is a real. (Contributed by NM, 27-Oct-2007.)
|

  |
|
Theorem | rpxr 9036 |
A positive real is an extended real. (Contributed by Mario Carneiro,
21-Aug-2015.)
|

  |
|
Theorem | rpcn 9037 |
A positive real is a complex number. (Contributed by NM, 11-Nov-2008.)
|

  |
|
Theorem | nnrp 9038 |
A positive integer is a positive real. (Contributed by NM,
28-Nov-2008.)
|
   |
|
Theorem | rpssre 9039 |
The positive reals are a subset of the reals. (Contributed by NM,
24-Feb-2008.)
|
 |
|
Theorem | rpgt0 9040 |
A positive real is greater than zero. (Contributed by FL,
27-Dec-2007.)
|

  |
|
Theorem | rpge0 9041 |
A positive real is greater than or equal to zero. (Contributed by NM,
22-Feb-2008.)
|

  |
|
Theorem | rpregt0 9042 |
A positive real is a positive real number. (Contributed by NM,
11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|
 
   |
|
Theorem | rprege0 9043 |
A positive real is a nonnegative real number. (Contributed by Mario
Carneiro, 31-Jan-2014.)
|
 
   |
|
Theorem | rpne0 9044 |
A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|
   |
|
Theorem | rpap0 9045 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
22-Mar-2020.)
|
 #   |
|
Theorem | rprene0 9046 |
A positive real is a nonzero real number. (Contributed by NM,
11-Nov-2008.)
|
 
   |
|
Theorem | rpreap0 9047 |
A positive real is a real number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
 
#    |
|
Theorem | rpcnne0 9048 |
A positive real is a nonzero complex number. (Contributed by NM,
11-Nov-2008.)
|
 
   |
|
Theorem | rpcnap0 9049 |
A positive real is a complex number apart from zero. (Contributed by Jim
Kingdon, 22-Mar-2020.)
|
 
#    |
|
Theorem | ralrp 9050 |
Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|
       |
|
Theorem | rexrp 9051 |
Quantification over positive reals. (Contributed by Mario Carneiro,
21-May-2014.)
|
       |
|
Theorem | rpaddcl 9052 |
Closure law for addition of positive reals. Part of Axiom 7 of [Apostol]
p. 20. (Contributed by NM, 27-Oct-2007.)
|
    
  |
|
Theorem | rpmulcl 9053 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by NM,
27-Oct-2007.)
|
    
  |
|
Theorem | rpdivcl 9054 |
Closure law for division of positive reals. (Contributed by FL,
27-Dec-2007.)
|
    
  |
|
Theorem | rpreccl 9055 |
Closure law for reciprocation of positive reals. (Contributed by Jeff
Hankins, 23-Nov-2008.)
|
  
  |
|
Theorem | rphalfcl 9056 |
Closure law for half of a positive real. (Contributed by Mario Carneiro,
31-Jan-2014.)
|
 
   |
|
Theorem | rpgecl 9057 |
A number greater or equal to a positive real is positive real.
(Contributed by Mario Carneiro, 28-May-2016.)
|
  
  |
|
Theorem | rphalflt 9058 |
Half of a positive real is less than the original number. (Contributed by
Mario Carneiro, 21-May-2014.)
|
 

  |
|
Theorem | rerpdivcl 9059 |
Closure law for division of a real by a positive real. (Contributed by
NM, 10-Nov-2008.)
|
    
  |
|
Theorem | ge0p1rp 9060 |
A nonnegative number plus one is a positive number. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
    
  |
|
Theorem | rpnegap 9061 |
Either a real apart from zero or its negation is a positive real, but not
both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|
  #   
   |
|
Theorem | 0nrp 9062 |
Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by
NM, 27-Oct-2007.)
|
 |
|
Theorem | ltsubrp 9063 |
Subtracting a positive real from another number decreases it.
(Contributed by FL, 27-Dec-2007.)
|
    
  |
|
Theorem | ltaddrp 9064 |
Adding a positive number to another number increases it. (Contributed by
FL, 27-Dec-2007.)
|
   
   |
|
Theorem | difrp 9065 |
Two ways to say one number is less than another. (Contributed by Mario
Carneiro, 21-May-2014.)
|
     
   |
|
Theorem | elrpd 9066 |
Membership in the set of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
       |
|
Theorem | nnrpd 9067 |
A positive integer is a positive real. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpred 9068 |
A positive real is a real. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpxrd 9069 |
A positive real is an extended real. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpcnd 9070 |
A positive real is a complex number. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpgt0d 9071 |
A positive real is greater than zero. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpge0d 9072 |
A positive real is greater than or equal to zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
     |
|
Theorem | rpne0d 9073 |
A positive real is nonzero. (Contributed by Mario Carneiro,
28-May-2016.)
|
     |
|
Theorem | rpap0d 9074 |
A positive real is apart from zero. (Contributed by Jim Kingdon,
28-Jul-2021.)
|
   #   |
|
Theorem | rpregt0d 9075 |
A positive real is real and greater than zero. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rprege0d 9076 |
A positive real is real and greater or equal to zero. (Contributed by
Mario Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rprene0d 9077 |
A positive real is a nonzero real number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rpcnne0d 9078 |
A positive real is a nonzero complex number. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rpreccld 9079 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rprecred 9080 |
Closure law for reciprocation of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
   
   |
|
Theorem | rphalfcld 9081 |
Closure law for half of a positive real. (Contributed by Mario
Carneiro, 28-May-2016.)
|
       |
|
Theorem | reclt1d 9082 |
The reciprocal of a positive number less than 1 is greater than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
    
    |
|
Theorem | recgt1d 9083 |
The reciprocal of a positive number greater than 1 is less than 1.
(Contributed by Mario Carneiro, 28-May-2016.)
|
   
 
   |
|
Theorem | rpaddcld 9084 |
Closure law for addition of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
     
   |
|
Theorem | rpmulcld 9085 |
Closure law for multiplication of positive reals. Part of Axiom 7 of
[Apostol] p. 20. (Contributed by Mario
Carneiro, 28-May-2016.)
|
         |
|
Theorem | rpdivcld 9086 |
Closure law for division of positive reals. (Contributed by Mario
Carneiro, 28-May-2016.)
|
         |
|
Theorem | ltrecd 9087 |
The reciprocal of both sides of 'less than'. (Contributed by Mario
Carneiro, 28-May-2016.)
|
       
     |
|
Theorem | lerecd 9088 |
The reciprocal of both sides of 'less than or equal to'. (Contributed
by Mario Carneiro, 28-May-2016.)
|
       
     |
|
Theorem | ltrec1d 9089 |
Reciprocal swap in a 'less than' relation. (Contributed by Mario
Carneiro, 28-May-2016.)
|
             |
|
Theorem | lerec2d 9090 |
Reciprocal swap in a 'less than or equal to' relation. (Contributed
by Mario Carneiro, 28-May-2016.)
|
             |
|
Theorem | lediv2ad 9091 |
Division of both sides of 'less than or equal to' into a nonnegative
number. (Contributed by Mario Carneiro, 28-May-2016.)
|
             
   |
|
Theorem | ltdiv2d 9092 |
Division of a positive number by both sides of 'less than'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | lediv2d 9093 |
Division of a positive number by both sides of 'less than or equal to'.
(Contributed by Mario Carneiro, 28-May-2016.)
|
         
     |
|
Theorem | ledivdivd 9094 |
Invert ratios of positive numbers and swap their ordering.
(Contributed by Mario Carneiro, 28-May-2016.)
|
                 
   |
|
Theorem | divge1 9095 |
The ratio of a number over a smaller positive number is larger than 1.
(Contributed by Glauco Siliprandi, 5-Apr-2020.)
|
  
    |
|
Theorem | divlt1lt 9096 |
A real number divided by a positive real number is less than 1 iff the
real number is less than the positive real number. (Contributed by AV,
25-May-2020.)
|
         |
|
Theorem | divle1le 9097 |
A real number divided by a positive real number is less than or equal to 1
iff the real number is less than or equal to the positive real number.
(Contributed by AV, 29-Jun-2021.)
|
     
   |
|
Theorem | ledivge1le 9098 |
If a number is less than or equal to another number, the number divided by
a positive number greater than or equal to one is less than or equal to
the other number. (Contributed by AV, 29-Jun-2021.)
|
  
 

     |
|
Theorem | ge0p1rpd 9099 |
A nonnegative number plus one is a positive number. (Contributed by
Mario Carneiro, 28-May-2016.)
|
     
   |
|
Theorem | rerpdivcld 9100 |
Closure law for division of a real by a positive real. (Contributed by
Mario Carneiro, 28-May-2016.)
|
         |