Home | Metamath
Proof ExplorerTheorem List
(p. 86 of 322)
| < 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-21498) |
Hilbert Space Explorer
(21499-23021) |
Users' Mathboxes
(23022-32154) |

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

Statement | ||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | nqex 8547 | 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 8548 | 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 8549 | 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 8550 | 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 8551 | 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 8552 | The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

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

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

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

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

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

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

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

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

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

Theorem | ordpinq 8567 | 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 8568 | 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 8569 | 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 8570 | 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 8571 | 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 8572 | 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 8573 | 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 8574 | 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 8575 | 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 8576 | 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 8577 | 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 8578 | Lemma for adderpq 8580. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

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

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

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

Theorem | addassnq 8582 | 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 8583 | 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 8584 | 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 8585 | 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 8586 | 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 8587 | 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 8588 | 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 8589 | 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 8590 | 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 8591 | 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 8592 | 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 8593 | '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 8594 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |

Theorem | ltanq 8595 | 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 8596 | 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 8597 | 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 8598 | 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 8599* | 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 8600* | 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.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |