Home | Metamath
Proof ExplorerTheorem List
(p. 89 of 321)
| < 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-22283) |
Hilbert Space Explorer
(22284-23806) |
Users' Mathboxes
(23807-32095) |

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

Statement | ||

Theorem | nsmallnq 8801* | 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 8802* | 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 8803 | 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 8804* | 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 8805* | 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 8943, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |

Definition | df-1p 8806 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8807* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8808* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8809* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8810 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |

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

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

Theorem | prn0 8813 | 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 8814 | 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 8815 | 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 8816 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |

Theorem | prcdnq 8817 | 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 8818 | 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 8819* | 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 8820 | 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 8817 and nsmallnq 8801). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |

Theorem | prnmadd 8821* | 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 8822 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |

Theorem | genpv 8823* | 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 8824* | 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 8825* | 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 8826* | 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 8827* | 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 8828* | 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 8829* | 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 8830* | 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 8831* | 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 8832* | 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 8833* | 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 8834* | Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |

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

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

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

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

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

Theorem | addclprlem1 8840 | 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 8841* | 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 8842 | 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 8843* | 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 8844 | 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 8845 | 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 8846 | 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 8847 | 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 8848 | 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 8849 | 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 8850* | 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 8851 | 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 8852 | 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 8853 | 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 8854 | Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.) |

Theorem | psslinpr 8855 | 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 8856 | 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 8857* | 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 8858 | 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 8859 | The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |

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

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

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

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

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

Theorem | ltexprlem6 8865* | 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 8866* | 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 8867* | 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 8868 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.) |

Theorem | ltapr 8869 | 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 8870 | 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 8871* | 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 8872* | 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 8873* | 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 8874* | Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.) |

Theorem | recexpr 8875* | 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 8876* | 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 8877* | The union of a set of positive reals (if a positive real) is its supremum (the 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 8878* | 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 8879* | Define pre-addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8880* | Define pre-multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8881* | Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8882 | Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8883* | Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8884* | Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8885* | Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8886 | Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8887 | Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8943, 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 8888 | Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 8943, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |

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

Theorem | enrer 8890 | 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 8891 | Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.) |

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

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

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

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

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

Theorem | addsrpr 8897 | 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 8898 | 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 8899 | 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 8900 | Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |