Theorem List for Intuitionistic Logic Explorer - 6401-6500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | cltr 6401 |
Signed real ordering relation.
|
 |
|
Definition | df-ni 6402 |
Define the class of positive integers. This is a "temporary" set
used in
the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 15-Aug-1995.)
|
     |
|
Definition | df-pli 6403 |
Define addition on positive integers. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 26-Aug-1995.)
|
    |
|
Definition | df-mi 6404 |
Define multiplication on positive integers. This is a "temporary"
set
used in the construction of complex numbers and is intended to be used
only by the construction. (Contributed by NM, 26-Aug-1995.)
|
    |
|
Definition | df-lti 6405 |
Define 'less than' on positive integers. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 6-Feb-1996.)
|
    |
|
Theorem | elni 6406 |
Membership in the class of positive integers. (Contributed by NM,
15-Aug-1995.)
|
 
   |
|
Theorem | pinn 6407 |
A positive integer is a natural number. (Contributed by NM,
15-Aug-1995.)
|
   |
|
Theorem | pion 6408 |
A positive integer is an ordinal number. (Contributed by NM,
23-Mar-1996.)
|
   |
|
Theorem | piord 6409 |
A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|
   |
|
Theorem | niex 6410 |
The class of positive integers is a set. (Contributed by NM,
15-Aug-1995.)
|
 |
|
Theorem | 0npi 6411 |
The empty set is not a positive integer. (Contributed by NM,
26-Aug-1995.)
|
 |
|
Theorem | elni2 6412 |
Membership in the class of positive integers. (Contributed by NM,
27-Nov-1995.)
|
 
   |
|
Theorem | 1pi 6413 |
Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|
 |
|
Theorem | addpiord 6414 |
Positive integer addition in terms of ordinal addition. (Contributed by
NM, 27-Aug-1995.)
|
    
    |
|
Theorem | mulpiord 6415 |
Positive integer multiplication in terms of ordinal multiplication.
(Contributed by NM, 27-Aug-1995.)
|
    
    |
|
Theorem | mulidpi 6416 |
1 is an identity element for multiplication on positive integers.
(Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro,
17-Nov-2014.)
|
  
  |
|
Theorem | ltpiord 6417 |
Positive integer 'less than' in terms of ordinal membership. (Contributed
by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
   
   |
|
Theorem | ltsopi 6418 |
Positive integer 'less than' is a strict ordering. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
|
 |
|
Theorem | pitric 6419 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
    
    |
|
Theorem | pitri3or 6420 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
   
   |
|
Theorem | ltdcpi 6421 |
Less-than for positive integers is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
   DECID   |
|
Theorem | ltrelpi 6422 |
Positive integer 'less than' is a relation on positive integers.
(Contributed by NM, 8-Feb-1996.)
|
   |
|
Theorem | dmaddpi 6423 |
Domain of addition on positive integers. (Contributed by NM,
26-Aug-1995.)
|
   |
|
Theorem | dmmulpi 6424 |
Domain of multiplication on positive integers. (Contributed by NM,
26-Aug-1995.)
|
   |
|
Theorem | addclpi 6425 |
Closure of addition of positive integers. (Contributed by NM,
18-Oct-1995.)
|
    
  |
|
Theorem | mulclpi 6426 |
Closure of multiplication of positive integers. (Contributed by NM,
18-Oct-1995.)
|
    
  |
|
Theorem | addcompig 6427 |
Addition of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
    
    |
|
Theorem | addasspig 6428 |
Addition of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
     
  
    |
|
Theorem | mulcompig 6429 |
Multiplication of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
    
    |
|
Theorem | mulasspig 6430 |
Multiplication of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
     
  
    |
|
Theorem | distrpig 6431 |
Multiplication of positive integers is distributive. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
          
    |
|
Theorem | addcanpig 6432 |
Addition cancellation law for positive integers. (Contributed by Jim
Kingdon, 27-Aug-2019.)
|
     
 
   |
|
Theorem | mulcanpig 6433 |
Multiplication cancellation law for positive integers. (Contributed by
Jim Kingdon, 29-Aug-2019.)
|
     
 
   |
|
Theorem | addnidpig 6434 |
There is no identity element for addition on positive integers.
(Contributed by NM, 28-Nov-1995.)
|
  
    |
|
Theorem | ltexpi 6435* |
Ordering on positive integers in terms of existence of sum.
(Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro,
14-Jun-2013.)
|
    


   |
|
Theorem | ltapig 6436 |
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31-Aug-2019.)
|
     
     |
|
Theorem | ltmpig 6437 |
Ordering property of multiplication for positive integers. (Contributed
by Jim Kingdon, 31-Aug-2019.)
|
     
     |
|
Theorem | 1lt2pi 6438 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|
   |
|
Theorem | nlt1pig 6439 |
No positive integer is less than one. (Contributed by Jim Kingdon,
31-Aug-2019.)
|
   |
|
Theorem | indpi 6440* |
Principle of Finite Induction on positive integers. (Contributed by NM,
23-Mar-1996.)
|
    
   
     
    
     |
|
Theorem | nnppipi 6441 |
A natural number plus a positive integer is a positive integer.
(Contributed by Jim Kingdon, 10-Nov-2019.)
|
    
  |
|
Definition | df-plpq 6442* |
Define pre-addition on positive fractions. This is a "temporary" set
used in the construction of complex numbers, and is intended to be used
only by the construction. This "pre-addition" operation works
directly
with ordered pairs of integers. The actual positive fraction addition
(df-plqqs 6447) works with the equivalence classes of these
ordered pairs determined by the equivalence relation
(df-enq 6445). (Analogous remarks apply to the other
"pre-" operations
in the complex number construction that follows.) From Proposition
9-2.3 of [Gleason] p. 117. (Contributed
by NM, 28-Aug-1995.)
|
   
                                       |
|
Definition | df-mpq 6443* |
Define pre-multiplication on positive fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. From Proposition 9-2.4 of [Gleason]
p. 119. (Contributed by NM, 28-Aug-1995.)
|
   
                           |
|
Definition | df-ltpq 6444* |
Define pre-ordering relation on positive fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. Similar to Definition 5
of [Suppes] p. 162. (Contributed by NM,
28-Aug-1995.)
|
          
                       |
|
Definition | df-enq 6445* |
Define equivalence relation for positive fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. From Proposition 9-2.1 of
[Gleason] p. 117. (Contributed by NM,
27-Aug-1995.)
|
       
               
     
      |
|
Definition | df-nqqs 6446 |
Define class of positive fractions. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. From Proposition 9-2.2 of [Gleason] p. 117.
(Contributed by NM, 16-Aug-1995.)
|
     |
|
Definition | df-plqqs 6447* |
Define addition on positive fractions. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. From Proposition 9-2.3 of [Gleason] p. 117.
(Contributed by NM, 24-Aug-1995.)
|
   
  
                 
    
             |
|
Definition | df-mqqs 6448* |
Define multiplication on positive fractions. This is a "temporary"
set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 9-2.4 of [Gleason] p. 119.
(Contributed by NM, 24-Aug-1995.)
|
   
  
                 
    
             |
|
Definition | df-1nqqs 6449 |
Define positive fraction constant 1. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. From Proposition 9-2.2 of [Gleason] p. 117.
(Contributed by NM, 29-Oct-1995.)
|
      |
|
Definition | df-rq 6450* |
Define reciprocal on positive fractions. It means the same thing as one
divided by the argument (although we don't define full division since we
will never need it). This is a "temporary" set used in the
construction
of complex numbers, and is intended to be used only by the construction.
From Proposition 9-2.5 of [Gleason] p.
119, who uses an asterisk to
denote this unary operation. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
    
     |
|
Definition | df-ltnqqs 6451* |
Define ordering relation on positive fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. Similar to Definition 5 of [Suppes]
p. 162. (Contributed by NM, 13-Feb-1996.)
|
     
               
     
       |
|
Theorem | dfplpq2 6452* |
Alternative definition of pre-addition on positive fractions.
(Contributed by Jim Kingdon, 12-Sep-2019.)
|
                                  

          |
|
Theorem | dfmpq2 6453* |
Alternative definition of pre-multiplication on positive fractions.
(Contributed by Jim Kingdon, 13-Sep-2019.)
|
                                  
       |
|
Theorem | enqbreq 6454 |
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by NM, 27-Aug-1995.)
|
    
          
     |
|
Theorem | enqbreq2 6455 |
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by Mario Carneiro, 8-May-2013.)
|
       
                       |
|
Theorem | enqer 6456 |
The equivalence relation for positive fractions is an equivalence
relation. Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM,
27-Aug-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|
   |
|
Theorem | enqeceq 6457 |
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29-Nov-1995.)
|
    
              
     |
|
Theorem | enqex 6458 |
The equivalence relation for positive fractions exists. (Contributed by
NM, 3-Sep-1995.)
|
 |
|
Theorem | enqdc 6459 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
    
  DECID   
     |
|
Theorem | enqdc1 6460 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
      
DECID      |
|
Theorem | nqex 6461 |
The class of positive fractions exists. (Contributed by NM,
16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
 |
|
Theorem | 0nnq 6462 |
The empty set is not a positive fraction. (Contributed by NM,
24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
 |
|
Theorem | ltrelnq 6463 |
Positive fraction 'less than' is a relation on positive fractions.
(Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro,
27-Apr-2013.)
|
   |
|
Theorem | 1nq 6464 |
The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|
 |
|
Theorem | addcmpblnq 6465 |
Lemma showing compatibility of addition. (Contributed by NM,
27-Aug-1995.)
|
   
   
 
 
          
       
         
          |
|
Theorem | mulcmpblnq 6466 |
Lemma showing compatibility of multiplication. (Contributed by NM,
27-Aug-1995.)
|
   
   
 
 
          
             
      |
|
Theorem | addpipqqslem 6467 |
Lemma for addpipqqs 6468. (Contributed by Jim Kingdon, 11-Sep-2019.)
|
    
     
           |
|
Theorem | addpipqqs 6468 |
Addition of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
    
                 
         |
|
Theorem | mulpipq2 6469 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8-May-2013.)
|
       
                          |
|
Theorem | mulpipq 6470 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro,
8-May-2013.)
|
    
                   |
|
Theorem | mulpipqqs 6471 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
    
                 
     |
|
Theorem | ordpipqqs 6472 |
Ordering of positive fractions in terms of positive integers.
(Contributed by Jim Kingdon, 14-Sep-2019.)
|
    
                    |
|
Theorem | addclnq 6473 |
Closure of addition on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
    
  |
|
Theorem | mulclnq 6474 |
Closure of multiplication on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
    
  |
|
Theorem | dmaddpqlem 6475* |
Decomposition of a positive fraction into numerator and denominator.
Lemma for dmaddpq 6477. (Contributed by Jim Kingdon, 15-Sep-2019.)
|
   
      |
|
Theorem | nqpi 6476* |
Decomposition of a positive fraction into numerator and denominator.
Similar to dmaddpqlem 6475 but also shows that the numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
      
        |
|
Theorem | dmaddpq 6477 |
Domain of addition on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
   |
|
Theorem | dmmulpq 6478 |
Domain of multiplication on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
   |
|
Theorem | addcomnqg 6479 |
Addition of positive fractions is commutative. (Contributed by Jim
Kingdon, 15-Sep-2019.)
|
    
    |
|
Theorem | addassnqg 6480 |
Addition of positive fractions is associative. (Contributed by Jim
Kingdon, 16-Sep-2019.)
|
     
  
    |
|
Theorem | mulcomnqg 6481 |
Multiplication of positive fractions is commutative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
    
    |
|
Theorem | mulassnqg 6482 |
Multiplication of positive fractions is associative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
     
  
    |
|
Theorem | mulcanenq 6483 |
Lemma for distributive law: cancellation of common factor. (Contributed
by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
|
      
        |
|
Theorem | mulcanenqec 6484 |
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17-Sep-2019.)
|
                  |
|
Theorem | distrnqg 6485 |
Multiplication of positive fractions is distributive. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
          
    |
|
Theorem | 1qec 6486 |
The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|
       |
|
Theorem | mulidnq 6487 |
Multiplication identity element for positive fractions. (Contributed by
NM, 3-Mar-1996.)
|
  
  |
|
Theorem | recexnq 6488* |
Existence of positive fraction reciprocal. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
         |
|
Theorem | recmulnqg 6489 |
Relationship between reciprocal and multiplication on positive
fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
|
             |
|
Theorem | recclnq 6490 |
Closure law for positive fraction reciprocal. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
    
  |
|
Theorem | recidnq 6491 |
A positive fraction times its reciprocal is 1. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
         |
|
Theorem | recrecnq 6492 |
Reciprocal of reciprocal of positive fraction. (Contributed by NM,
26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
|
           |
|
Theorem | rec1nq 6493 |
Reciprocal of positive fraction one. (Contributed by Jim Kingdon,
29-Dec-2019.)
|
   
 |
|
Theorem | nqtri3or 6494 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
   
   |
|
Theorem | ltdcnq 6495 |
Less-than for positive fractions is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
   DECID   |
|
Theorem | ltsonq 6496 |
'Less than' is a strict ordering on positive fractions. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
|
 |
|
Theorem | nqtric 6497 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
    
    |
|
Theorem | ltanqg 6498 |
Ordering property of addition for positive fractions. Proposition
9-2.6(ii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22-Sep-2019.)
|
     
     |
|
Theorem | ltmnqg 6499 |
Ordering property of multiplication for positive fractions. Proposition
9-2.6(iii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22-Sep-2019.)
|
     
     |
|
Theorem | ltanqi 6500 |
Ordering property of addition for positive fractions. One direction of
ltanqg 6498. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
    
    |