Home | Metamath
Proof ExplorerTheorem List
(p. 86 of 315)
| < 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-21490) |
Hilbert Space Explorer
(21491-23013) |
Users' Mathboxes
(23014-31421) |

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

Statement | ||

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

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

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

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

Theorem | mulidpi 8505 | 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 8506 | 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 8507 | 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 8508 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |

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

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

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

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

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

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

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

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

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

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

Theorem | mulcanpi 8519 | 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 8520 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.) |

Theorem | ltexpi 8521* | 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 8522 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |

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

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

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

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

Definition | df-plpq 8527* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8533) works with the equivalence classes of these ordered pairs determined by the equivalence relation (df-enq 8530). (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 8528* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8529* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8530* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8531* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8532 | 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 8549. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Definition | df-plq 8533 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8534 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8535 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8536 | 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 8738, 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 8537 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8738, 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 8538 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

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

Theorem | enqer 8540 | 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 8541 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |

Theorem | nqex 8542 | 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 8543 | 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 8544 | 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 8545 | 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 8546 | 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 8547 | The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

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

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

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

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

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

Theorem | enqeq 8553 | Corollary of nqereu 8548: 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 8554 | 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 8555 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

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

Theorem | addpqnq 8557 | 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 8558 | Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | mulpipq 8559 | 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 8560 | 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 8561 | Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

Theorem | ordpinq 8562 | 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 8563 | 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 8564 | 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 8565 | 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 8566 | 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 8567 | 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 8568 | 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 8569 | 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 8570 | 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 8571 | 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 8572 | 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 8573 | Lemma for adderpq 8575. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

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

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

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

Theorem | addassnq 8577 | 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 8578 | 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 8579 | 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 8580 | 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 8581 | 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 8582 | 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 8583 | 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 8584 | 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 8585 | 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 8586 | Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.) |

Theorem | dmrecnq 8587 | Domain of reciprocal on positive fractions. (Contributed by Mario Carneiro, 6-Mar-1996.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |

Theorem | ltsonq 8588 | 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.) (New usage is discouraged.) |

Theorem | lterpq 8589 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |

Theorem | ltanq 8590 | Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | ltmnq 8591 | Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | 1lt2nq 8592 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | ltaddnq 8593 | The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | ltexnq 8594* | Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by NM, 24-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | halfnq 8595* | One-half of any positive fraction exists. Lemma for Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 16-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | nsmallnq 8596* | The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | ltbtwnnq 8597* | There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | ltrnq 8598 | Ordering property of reciprocal for positive fractions. Proposition 9-2.6(iv) of [Gleason] p. 120. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Theorem | archnq 8599* | For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |

Definition | df-np 8600* | Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. A positive real is defined as the lower class of a Dedekind cut. Definition 9-3.1 of [Gleason] p. 121. (Note: This is a "temporary" definition used in the construction of complex numbers df-c 8738, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |