Home | Metamath
Proof ExplorerTheorem List
(p. 85 of 311)
| < 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-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-31058) |

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

Statement | ||

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

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

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

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

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

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

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

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

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

Definition | df-plpq 8412* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8418) works with the equivalence classes of these ordered pairs determined by the equivalence relation (df-enq 8415). (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 8413* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8414* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8415* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8416* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8417 | 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 8434. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

Definition | df-plq 8418 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8419 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8420 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8421 | 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 8623, 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 8422 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8423 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |

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

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

Theorem | nqex 8427 | 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 8428 | 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 8429 | 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 8430 | 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 8431 | 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 8432 | The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |

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

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

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

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

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

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

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

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

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

Theorem | ordpinq 8447 | 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 8448 | 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 8449 | 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 8450 | 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 8451 | 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 8452 | 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 8453 | 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 8454 | 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 8455 | 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 8456 | 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 8457 | 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 8458 | Lemma for adderpq 8460. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |

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

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

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

Theorem | addassnq 8462 | 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 8463 | 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 8464 | 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 8465 | 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 8466 | 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 8467 | 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 8468 | 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 8469 | 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 8470 | 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 8471 | 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 8472 | 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 8473 | '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 8474 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |

Theorem | ltanq 8475 | 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 8476 | 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 8477 | 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 8478 | 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 8479* | 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 8480* | 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 8481* | 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 8482* | 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 8483 | 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 8484* | 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 8485* | 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 8623, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |

Definition | df-1p 8486 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8623, and is intended to be used only by the construction. Definition of [Gleason] p. 122. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Definition | df-plp 8487* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8623, and is intended to be used only by the construction. From Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |

Definition | df-mp 8488* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8623, and is intended to be used only by the construction. From Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |

Definition | df-ltp 8489* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8623, and is intended to be used only by the construction. From Proposition 9-3.2 of [Gleason] p. 122. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |

Theorem | npex 8490 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |

Theorem | elnp 8491* | Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.) |

Theorem | elnpi 8492* | Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | prn0 8493 | A positive real is not empty. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | prpssnq 8494 | A positive real is a subset of the positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | elprnq 8495 | A positive real is a set of positive fractions. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | 0npr 8496 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |

Theorem | prcdnq 8497 | A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of [Gleason] p. 121. (Contributed by NM, 25-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | prub 8498 | A positive fraction not in a positive real is an upper bound. Remark (1) of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.) |

Theorem | prnmax 8499* | A positive real has no largest member. Definition 9-3.1(iii) of [Gleason] p. 121. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | npomex 8500 | A simplifying observation, and an indication of why any attempt to develop a theory of the real numbers without the Axiom of Infinity is doomed to failure: since every member of is an infinite set, the negation of Infinity implies that , and hence , is empty. (Note that this proof, which used the fact that Dedekind cuts have no maximum, could just as well have used that they have no minimum, since they are downward-closed by prcdnq 8497 and nsmallnq 8481). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |