Home | Metamath
Proof ExplorerTheorem List
(p. 88 of 325)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |

Type | Label | Description |
---|---|---|

Statement | ||

Syntax | cm1r 8701 | The signed real constant -1. |

Syntax | cplr 8702 | Signed real addition. |

Syntax | cmr 8703 | Signed real multiplication. |

Syntax | cltr 8704 | Signed real ordering relation. |

Definition | df-ni 8705 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |

Definition | df-pli 8706 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |

Definition | df-mi 8707 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |

Definition | df-lti 8708 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) (New usage is discouraged.) |

Theorem | elni 8709 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |

Theorem | elni2 8710 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.) |

Theorem | pinn 8711 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |

Theorem | pion 8712 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |

Theorem | piord 8713 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.) |

Theorem | niex 8714 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |

Theorem | 0npi 8715 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |

Theorem | 1pi 8716 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) |

Theorem | addpiord 8717 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Theorem | mulpiord 8718 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Theorem | mulidpi 8719 | 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |

Theorem | ltpiord 8720 | Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |

Theorem | ltsopi 8721 | Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |

Theorem | ltrelpi 8722 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |

Theorem | dmaddpi 8723 | Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |

Theorem | dmmulpi 8724 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |

Theorem | addclpi 8725 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |

Theorem | mulclpi 8726 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |

Theorem | addcompi 8727 | Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Theorem | addasspi 8728 | Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Theorem | mulcompi 8729 | Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |

Theorem | mulasspi 8730 | Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |

Theorem | distrpi 8731 | Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |

Theorem | addcanpi 8732 | Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulcanpi 8733 | Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | addnidpi 8734 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.) |

Theorem | ltexpi 8735* | Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |

Theorem | ltapi 8736 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |

Theorem | ltmpi 8737 | Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |

Theorem | 1lt2pi 8738 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Theorem | nlt1pi 8739 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |

Theorem | indpi 8740* | Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |

Definition | df-plpq 8741* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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-plq 8747) works with the equivalence classes of these ordered pairs determined by the equivalence relation (df-enq 8744). (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.) (New usage is discouraged.) |

Definition | df-mpq 8742* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.) |

Definition | df-ltpq 8743* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.) (New usage is discouraged.) |

Definition | df-enq 8744* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.) |

Definition | df-nq 8745* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.) |

Definition | df-erq 8746 | Define a convenience function that "reduces" a fraction to lowest terms. Note that in this form, it is not obviously a function; we prove this in nqerf 8763. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Definition | df-plq 8747 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.) |

Definition | df-mq 8748 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.) |

Definition | df-1nq 8749 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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.) (New usage is discouraged.) |

Definition | df-rq 8750 | 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 df-c 8952, 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 NM, 6-Mar-1996.) (New usage is discouraged.) |

Definition | df-ltnq 8751 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.) (New usage is discouraged.) |

Theorem | enqbreq 8752 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Theorem | enqbreq2 8753 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | enqer 8754 | 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.) (New usage is discouraged.) |

Theorem | enqex 8755 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |

Theorem | nqex 8756 | The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |

Theorem | 0nnq 8757 | The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |

Theorem | elpqn 8758 | Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | ltrelnq 8759 | Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |

Theorem | pinq 8760 | The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |

Theorem | 1nq 8761 | The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | nqereu 8762* | There is a unique element of equivalent to each element of . (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | nqerf 8763 | Corollary of nqereu 8762: the function is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |

Theorem | nqercl 8764 | Corollary of nqereu 8762: closure of . (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |

Theorem | nqerrel 8765 | Any member of relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |

Theorem | nqerid 8766 | Corollary of nqereu 8762: the function acts as the identity on members of . (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |

Theorem | enqeq 8767 | Corollary of nqereu 8762: if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |

Theorem | nqereq 8768 | The function acts as a substitute for equivalence classes, and it satisfies the fundamental requirement for equivalence representatives: the representatives are equal iff the members are equivalent. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |

Theorem | addpipq2 8769 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | addpipq 8770 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | addpqnq 8771 | Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 26-Dec-2014.) (New usage is discouraged.) |

Theorem | mulpipq2 8772 | Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulpipq 8773 | Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulpqnq 8774 | Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 26-Dec-2014.) (New usage is discouraged.) |

Theorem | ordpipq 8775 | Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | ordpinq 8776 | Ordering of positive fractions in terms of positive integers. (Contributed by NM, 13-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | addpqf 8777 | Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | addclnq 8778 | Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulpqf 8779 | Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulclnq 8780 | Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | addnqf 8781 | Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |

Theorem | mulnqf 8782 | Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |

Theorem | addcompq 8783 | Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | addcomnq 8784 | Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | mulcompq 8785 | Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | mulcomnq 8786 | Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | adderpqlem 8787 | Lemma for adderpq 8789. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulerpqlem 8788 | Lemma for mulerpq 8790. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | adderpq 8789 | Addition is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulerpq 8790 | Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | addassnq 8791 | Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | mulassnq 8792 | Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulcanenq 8793 | Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | distrnq 8794 | Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | 1nqenq 8795 | The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | mulidnq 8796 | Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | recmulnq 8797 | Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |

Theorem | recidnq 8798 | A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | recclnq 8799 | Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | recrecnq 8800 | Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |