Home | Metamath
Proof ExplorerTheorem List
(p. 87 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 | nsmallnq 8601* | 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 8602* | 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 8603 | 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 8604* | 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 8605* | 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 8743, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |

Definition | df-1p 8606 | Define the positive real 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. Definition of [Gleason] p. 122. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Definition | df-plp 8607* | Define addition on positive reals. 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-3.5 of [Gleason] p. 123. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |

Definition | df-mp 8608* | Define multiplication on positive reals. 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-3.7 of [Gleason] p. 124. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |

Definition | df-ltp 8609* | Define ordering on positive reals. 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-3.2 of [Gleason] p. 122. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |

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

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

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

Theorem | prn0 8613 | 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 8614 | 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 8615 | 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 8616 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |

Theorem | prcdnq 8617 | 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 8618 | 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 8619* | 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 8620 | 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 8617 and nsmallnq 8601). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |

Theorem | prnmadd 8621* | A positive real has no largest member. Addition version. (Contributed by NM, 7-Apr-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | ltrelpr 8622 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |

Theorem | genpv 8623* | Value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |

Theorem | genpelv 8624* | Membership in value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpprecl 8625* | Pre-closure law for general operation on positive reals. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpdm 8626* | Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |

Theorem | genpn0 8627* | The result of an operation on positive reals is not empty. (Contributed by NM, 28-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpss 8628* | The result of an operation on positive reals is a subset of the positive fractions. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpnnp 8629* | The result of an operation on positive reals is different from the set of positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpcd 8630* | Downward closure of an operation on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpnmax 8631* | An operation on positive reals has no largest member. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | genpcl 8632* | Closure of an operation on reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |

Theorem | genpass 8633* | Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | plpv 8634* | Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |

Theorem | mpv 8635* | Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |

Theorem | dmplp 8636 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |

Theorem | dmmp 8637 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |

Theorem | nqpr 8638* | The canonical embedding of the rationals into the reals. (Contributed by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | 1pr 8639 | The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | addclprlem1 8640 | Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Theorem | addclprlem2 8641* | Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Theorem | addclpr 8642 | Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Theorem | mulclprlem 8643* | Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 14-Mar-1996.) (New usage is discouraged.) |

Theorem | mulclpr 8644 | Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |

Theorem | addcompr 8645 | Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.) |

Theorem | addasspr 8646 | Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.) |

Theorem | mulcompr 8647 | Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.) |

Theorem | mulasspr 8648 | Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.) |

Theorem | distrlem1pr 8649 | Lemma for distributive law for positive reals. (Contributed by NM, 1-May-1996.) (Revised by Mario Carneiro, 13-Jun-2013.) (New usage is discouraged.) |

Theorem | distrlem4pr 8650* | Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |

Theorem | distrlem5pr 8651 | Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |

Theorem | distrpr 8652 | Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |

Theorem | 1idpr 8653 | 1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.) (New usage is discouraged.) |

Theorem | ltprord 8654 | Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.) |

Theorem | psslinpr 8655 | Proper subset is a linear ordering on positive reals. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.) |

Theorem | ltsopr 8656 | Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.) |

Theorem | prlem934 8657* | Lemma 9-3.4 of [Gleason] p. 122. (Contributed by NM, 25-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |

Theorem | ltaddpr 8658 | The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | ltaddpr2 8659 | The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |

Theorem | ltexprlem1 8660* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.) |

Theorem | ltexprlem2 8661* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.) |

Theorem | ltexprlem3 8662* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.) |

Theorem | ltexprlem4 8663* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.) |

Theorem | ltexprlem5 8664* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.) |

Theorem | ltexprlem6 8665* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | ltexprlem7 8666* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | ltexpri 8667* | Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |

Theorem | ltaprlem 8668 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.) |

Theorem | ltapr 8669 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.) |

Theorem | addcanpr 8670 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by NM, 9-Apr-1996.) (New usage is discouraged.) |

Theorem | prlem936 8671* | Lemma 9-3.6 of [Gleason] p. 124. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | reclem2pr 8672* | Lemma for Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | reclem3pr 8673* | Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | reclem4pr 8674* | Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.) |

Theorem | recexpr 8675* | The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | suplem1pr 8676* | The union of a non-empty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | suplem2pr 8677* | The union of a set of positive reals (if a positive real) is its supremum (least upper bound). Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |

Theorem | supexpr 8678* | The union of a non-empty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (New usage is discouraged.) |

Definition | df-plpr 8679* | Define pre-addition on signed reals. 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-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |

Definition | df-mpr 8680* | Define pre-multiplication on signed reals. 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-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |

Definition | df-enr 8681* | Define equivalence relation for signed reals. 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-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |

Definition | df-nr 8682 | Define class of signed reals. 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-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |

Definition | df-plr 8683* | Define addition on signed reals. 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-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |

Definition | df-mr 8684* | Define multiplication on signed reals. 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-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |

Definition | df-ltr 8685* | Define ordering relation on signed reals. 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-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |

Definition | df-0r 8686 | Define signed real constant 0. 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-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |

Definition | df-1r 8687 | Define signed real 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-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |

Definition | df-m1r 8688 | Define signed real 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. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |

Theorem | enrbreq 8689 | Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |

Theorem | enrer 8690 | The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (New usage is discouraged.) |

Theorem | enreceq 8691 | Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.) |

Theorem | enrex 8692 | The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |

Theorem | ltrelsr 8693 | Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |

Theorem | addcmpblnr 8694 | Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |

Theorem | mulcmpblnrlem 8695 | Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.) |

Theorem | mulcmpblnr 8696 | Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.) |

Theorem | addsrpr 8697 | Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |

Theorem | mulsrpr 8698 | Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |

Theorem | ltsrpr 8699 | Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |

Theorem | gt0srpr 8700 | Greater then zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |