Home | Metamath
Proof Explorer Theorem List (p. 109 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nqercl 10801 | Corollary of nqereu 10799: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข (๐ด โ (N ร N) โ ([Q]โ๐ด) โ Q) | ||
Theorem | nqerrel 10802 | Any member of (N ร N) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข (๐ด โ (N ร N) โ ๐ด ~Q ([Q]โ๐ด)) | ||
Theorem | nqerid 10803 | Corollary of nqereu 10799: the function [Q] acts as the identity on members of Q. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข (๐ด โ Q โ ([Q]โ๐ด) = ๐ด) | ||
Theorem | enqeq 10804 | Corollary of nqereu 10799: if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ Q โง ๐ต โ Q โง ๐ด ~Q ๐ต) โ ๐ด = ๐ต) | ||
Theorem | nqereq 10805 | The function [Q] 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.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N)) โ (๐ด ~Q ๐ต โ ([Q]โ๐ด) = ([Q]โ๐ต))) | ||
Theorem | addpipq2 10806 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N)) โ (๐ด +pQ ๐ต) = โจ(((1st โ๐ด) ยทN (2nd โ๐ต)) +N ((1st โ๐ต) ยทN (2nd โ๐ด))), ((2nd โ๐ด) ยทN (2nd โ๐ต))โฉ) | ||
Theorem | addpipq 10807 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข (((๐ด โ N โง ๐ต โ N) โง (๐ถ โ N โง ๐ท โ N)) โ (โจ๐ด, ๐ตโฉ +pQ โจ๐ถ, ๐ทโฉ) = โจ((๐ด ยทN ๐ท) +N (๐ถ ยทN ๐ต)), (๐ต ยทN ๐ท)โฉ) | ||
Theorem | addpqnq 10808 | 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.) |
โข ((๐ด โ Q โง ๐ต โ Q) โ (๐ด +Q ๐ต) = ([Q]โ(๐ด +pQ ๐ต))) | ||
Theorem | mulpipq2 10809 | Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N)) โ (๐ด ยทpQ ๐ต) = โจ((1st โ๐ด) ยทN (1st โ๐ต)), ((2nd โ๐ด) ยทN (2nd โ๐ต))โฉ) | ||
Theorem | mulpipq 10810 | 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.) |
โข (((๐ด โ N โง ๐ต โ N) โง (๐ถ โ N โง ๐ท โ N)) โ (โจ๐ด, ๐ตโฉ ยทpQ โจ๐ถ, ๐ทโฉ) = โจ(๐ด ยทN ๐ถ), (๐ต ยทN ๐ท)โฉ) | ||
Theorem | mulpqnq 10811 | 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.) |
โข ((๐ด โ Q โง ๐ต โ Q) โ (๐ด ยทQ ๐ต) = ([Q]โ(๐ด ยทpQ ๐ต))) | ||
Theorem | ordpipq 10812 | Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข (โจ๐ด, ๐ตโฉ <pQ โจ๐ถ, ๐ทโฉ โ (๐ด ยทN ๐ท) <N (๐ถ ยทN ๐ต)) | ||
Theorem | ordpinq 10813 | 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.) |
โข ((๐ด โ Q โง ๐ต โ Q) โ (๐ด <Q ๐ต โ ((1st โ๐ด) ยทN (2nd โ๐ต)) <N ((1st โ๐ต) ยทN (2nd โ๐ด)))) | ||
Theorem | addpqf 10814 | Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข +pQ :((N ร N) ร (N ร N))โถ(N ร N) | ||
Theorem | addclnq 10815 | Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ Q โง ๐ต โ Q) โ (๐ด +Q ๐ต) โ Q) | ||
Theorem | mulpqf 10816 | Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ยทpQ :((N ร N) ร (N ร N))โถ(N ร N) | ||
Theorem | mulclnq 10817 | Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ Q โง ๐ต โ Q) โ (๐ด ยทQ ๐ต) โ Q) | ||
Theorem | addnqf 10818 | Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
โข +Q :(Q ร Q)โถQ | ||
Theorem | mulnqf 10819 | Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
โข ยทQ :(Q ร Q)โถQ | ||
Theorem | addcompq 10820 | Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด +pQ ๐ต) = (๐ต +pQ ๐ด) | ||
Theorem | addcomnq 10821 | Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด +Q ๐ต) = (๐ต +Q ๐ด) | ||
Theorem | mulcompq 10822 | Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด ยทpQ ๐ต) = (๐ต ยทpQ ๐ด) | ||
Theorem | mulcomnq 10823 | Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด ยทQ ๐ต) = (๐ต ยทQ ๐ด) | ||
Theorem | adderpqlem 10824 | Lemma for adderpq 10826. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N) โง ๐ถ โ (N ร N)) โ (๐ด ~Q ๐ต โ (๐ด +pQ ๐ถ) ~Q (๐ต +pQ ๐ถ))) | ||
Theorem | mulerpqlem 10825 | Lemma for mulerpq 10827. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N) โง ๐ถ โ (N ร N)) โ (๐ด ~Q ๐ต โ (๐ด ยทpQ ๐ถ) ~Q (๐ต ยทpQ ๐ถ))) | ||
Theorem | adderpq 10826 | Addition is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข (([Q]โ๐ด) +Q ([Q]โ๐ต)) = ([Q]โ(๐ด +pQ ๐ต)) | ||
Theorem | mulerpq 10827 | Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข (([Q]โ๐ด) ยทQ ([Q]โ๐ต)) = ([Q]โ(๐ด ยทpQ ๐ต)) | ||
Theorem | addassnq 10828 | Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข ((๐ด +Q ๐ต) +Q ๐ถ) = (๐ด +Q (๐ต +Q ๐ถ)) | ||
Theorem | mulassnq 10829 | Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด ยทQ ๐ต) ยทQ ๐ถ) = (๐ด ยทQ (๐ต ยทQ ๐ถ)) | ||
Theorem | mulcanenq 10830 | 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.) |
โข ((๐ด โ N โง ๐ต โ N โง ๐ถ โ N) โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ ~Q โจ๐ต, ๐ถโฉ) | ||
Theorem | distrnq 10831 | Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด ยทQ (๐ต +Q ๐ถ)) = ((๐ด ยทQ ๐ต) +Q (๐ด ยทQ ๐ถ)) | ||
Theorem | 1nqenq 10832 | The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด โ N โ 1Q ~Q โจ๐ด, ๐ดโฉ) | ||
Theorem | mulidnq 10833 | Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด โ Q โ (๐ด ยทQ 1Q) = ๐ด) | ||
Theorem | recmulnq 10834 | 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.) |
โข (๐ด โ Q โ ((*Qโ๐ด) = ๐ต โ (๐ด ยทQ ๐ต) = 1Q)) | ||
Theorem | recidnq 10835 | 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.) |
โข (๐ด โ Q โ (๐ด ยทQ (*Qโ๐ด)) = 1Q) | ||
Theorem | recclnq 10836 | Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข (๐ด โ Q โ (*Qโ๐ด) โ Q) | ||
Theorem | recrecnq 10837 | Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.) |
โข (๐ด โ Q โ (*Qโ(*Qโ๐ด)) = ๐ด) | ||
Theorem | dmrecnq 10838 | Domain of reciprocal on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
โข dom *Q = Q | ||
Theorem | ltsonq 10839 | '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.) |
โข <Q Or Q | ||
Theorem | lterpq 10840 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |
โข (๐ด <pQ ๐ต โ ([Q]โ๐ด) <Q ([Q]โ๐ต)) | ||
Theorem | ltanq 10841 | 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.) |
โข (๐ถ โ Q โ (๐ด <Q ๐ต โ (๐ถ +Q ๐ด) <Q (๐ถ +Q ๐ต))) | ||
Theorem | ltmnq 10842 | 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.) |
โข (๐ถ โ Q โ (๐ด <Q ๐ต โ (๐ถ ยทQ ๐ด) <Q (๐ถ ยทQ ๐ต))) | ||
Theorem | 1lt2nq 10843 | 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.) |
โข 1Q <Q (1Q +Q 1Q) | ||
Theorem | ltaddnq 10844 | 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.) |
โข ((๐ด โ Q โง ๐ต โ Q) โ ๐ด <Q (๐ด +Q ๐ต)) | ||
Theorem | ltexnq 10845* | 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.) |
โข (๐ต โ Q โ (๐ด <Q ๐ต โ โ๐ฅ(๐ด +Q ๐ฅ) = ๐ต)) | ||
Theorem | halfnq 10846* | 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.) |
โข (๐ด โ Q โ โ๐ฅ(๐ฅ +Q ๐ฅ) = ๐ด) | ||
Theorem | nsmallnq 10847* | The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
โข (๐ด โ Q โ โ๐ฅ ๐ฅ <Q ๐ด) | ||
Theorem | ltbtwnnq 10848* | 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.) |
โข (๐ด <Q ๐ต โ โ๐ฅ(๐ด <Q ๐ฅ โง ๐ฅ <Q ๐ต)) | ||
Theorem | ltrnq 10849 | 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.) |
โข (๐ด <Q ๐ต โ (*Qโ๐ต) <Q (*Qโ๐ด)) | ||
Theorem | archnq 10850* | 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.) |
โข (๐ด โ Q โ โ๐ฅ โ N ๐ด <Q โจ๐ฅ, 1oโฉ) | ||
Definition | df-np 10851* | 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 10991, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
โข P = {๐ฅ โฃ ((โ โ ๐ฅ โง ๐ฅ โ Q) โง โ๐ฆ โ ๐ฅ (โ๐ง(๐ง <Q ๐ฆ โ ๐ง โ ๐ฅ) โง โ๐ง โ ๐ฅ ๐ฆ <Q ๐ง))} | ||
Definition | df-1p 10852 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10991, 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.) |
โข 1P = {๐ฅ โฃ ๐ฅ <Q 1Q} | ||
Definition | df-plp 10853* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10991, 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.) |
โข +P = (๐ฅ โ P, ๐ฆ โ P โฆ {๐ค โฃ โ๐ฃ โ ๐ฅ โ๐ข โ ๐ฆ ๐ค = (๐ฃ +Q ๐ข)}) | ||
Definition | df-mp 10854* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10991, 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.) |
โข ยทP = (๐ฅ โ P, ๐ฆ โ P โฆ {๐ค โฃ โ๐ฃ โ ๐ฅ โ๐ข โ ๐ฆ ๐ค = (๐ฃ ยทQ ๐ข)}) | ||
Definition | df-ltp 10855* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10991, 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.) |
โข <P = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ P โง ๐ฆ โ P) โง ๐ฅ โ ๐ฆ)} | ||
Theorem | npex 10856 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
โข P โ V | ||
Theorem | elnp 10857* | Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.) |
โข (๐ด โ P โ ((โ โ ๐ด โง ๐ด โ Q) โง โ๐ฅ โ ๐ด (โ๐ฆ(๐ฆ <Q ๐ฅ โ ๐ฆ โ ๐ด) โง โ๐ฆ โ ๐ด ๐ฅ <Q ๐ฆ))) | ||
Theorem | elnpi 10858* | Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
โข (๐ด โ P โ ((๐ด โ V โง โ โ ๐ด โง ๐ด โ Q) โง โ๐ฅ โ ๐ด (โ๐ฆ(๐ฆ <Q ๐ฅ โ ๐ฆ โ ๐ด) โง โ๐ฆ โ ๐ด ๐ฅ <Q ๐ฆ))) | ||
Theorem | prn0 10859 | A positive real is not empty. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
โข (๐ด โ P โ ๐ด โ โ ) | ||
Theorem | prpssnq 10860 | 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.) |
โข (๐ด โ P โ ๐ด โ Q) | ||
Theorem | elprnq 10861 | 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.) |
โข ((๐ด โ P โง ๐ต โ ๐ด) โ ๐ต โ Q) | ||
Theorem | 0npr 10862 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |
โข ยฌ โ โ P | ||
Theorem | prcdnq 10863 | 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.) |
โข ((๐ด โ P โง ๐ต โ ๐ด) โ (๐ถ <Q ๐ต โ ๐ถ โ ๐ด)) | ||
Theorem | prub 10864 | 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.) |
โข (((๐ด โ P โง ๐ต โ ๐ด) โง ๐ถ โ Q) โ (ยฌ ๐ถ โ ๐ด โ ๐ต <Q ๐ถ)) | ||
Theorem | prnmax 10865* | 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.) |
โข ((๐ด โ P โง ๐ต โ ๐ด) โ โ๐ฅ โ ๐ด ๐ต <Q ๐ฅ) | ||
Theorem | npomex 10866 | 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 P is an infinite set, the negation of Infinity implies that P, 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 10863 and nsmallnq 10847). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |
โข (๐ด โ P โ ฯ โ V) | ||
Theorem | prnmadd 10867* | 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.) |
โข ((๐ด โ P โง ๐ต โ ๐ด) โ โ๐ฅ(๐ต +Q ๐ฅ) โ ๐ด) | ||
Theorem | ltrelpr 10868 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |
โข <P โ (P ร P) | ||
Theorem | genpv 10869* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) โ โข ((๐ด โ P โง ๐ต โ P) โ (๐ด๐น๐ต) = {๐ โฃ โ๐ โ ๐ด โโ โ ๐ต ๐ = (๐๐บโ)}) | ||
Theorem | genpelv 10870* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) โ โข ((๐ด โ P โง ๐ต โ P) โ (๐ถ โ (๐ด๐น๐ต) โ โ๐ โ ๐ด โโ โ ๐ต ๐ถ = (๐๐บโ))) | ||
Theorem | genpprecl 10871* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) โ โข ((๐ด โ P โง ๐ต โ P) โ ((๐ถ โ ๐ด โง ๐ท โ ๐ต) โ (๐ถ๐บ๐ท) โ (๐ด๐น๐ต))) | ||
Theorem | genpdm 10872* | Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) โ โข dom ๐น = (P ร P) | ||
Theorem | genpn0 10873* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) โ โข ((๐ด โ P โง ๐ต โ P) โ โ โ (๐ด๐น๐ต)) | ||
Theorem | genpss 10874* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) โ โข ((๐ด โ P โง ๐ต โ P) โ (๐ด๐น๐ต) โ Q) | ||
Theorem | genpnnp 10875* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) & โข (๐ง โ Q โ (๐ฅ <Q ๐ฆ โ (๐ง๐บ๐ฅ) <Q (๐ง๐บ๐ฆ))) & โข (๐ฅ๐บ๐ฆ) = (๐ฆ๐บ๐ฅ) โ โข ((๐ด โ P โง ๐ต โ P) โ ยฌ (๐ด๐น๐ต) = Q) | ||
Theorem | genpcd 10876* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) & โข ((((๐ด โ P โง ๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q (๐๐บโ) โ ๐ฅ โ (๐ด๐น๐ต))) โ โข ((๐ด โ P โง ๐ต โ P) โ (๐ โ (๐ด๐น๐ต) โ (๐ฅ <Q ๐ โ ๐ฅ โ (๐ด๐น๐ต)))) | ||
Theorem | genpnmax 10877* | 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.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) & โข (๐ฃ โ Q โ (๐ง <Q ๐ค โ (๐ฃ๐บ๐ง) <Q (๐ฃ๐บ๐ค))) & โข (๐ง๐บ๐ค) = (๐ค๐บ๐ง) โ โข ((๐ด โ P โง ๐ต โ P) โ (๐ โ (๐ด๐น๐ต) โ โ๐ฅ โ (๐ด๐น๐ต)๐ <Q ๐ฅ)) | ||
Theorem | genpcl 10878* | Closure of an operation on reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) & โข (โ โ Q โ (๐ <Q ๐ โ (โ๐บ๐) <Q (โ๐บ๐))) & โข (๐ฅ๐บ๐ฆ) = (๐ฆ๐บ๐ฅ) & โข ((((๐ด โ P โง ๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q (๐๐บโ) โ ๐ฅ โ (๐ด๐น๐ต))) โ โข ((๐ด โ P โง ๐ต โ P) โ (๐ด๐น๐ต) โ P) | ||
Theorem | genpass 10879* | Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |
โข ๐น = (๐ค โ P, ๐ฃ โ P โฆ {๐ฅ โฃ โ๐ฆ โ ๐ค โ๐ง โ ๐ฃ ๐ฅ = (๐ฆ๐บ๐ง)}) & โข ((๐ฆ โ Q โง ๐ง โ Q) โ (๐ฆ๐บ๐ง) โ Q) & โข dom ๐น = (P ร P) & โข ((๐ โ P โง ๐ โ P) โ (๐๐น๐) โ P) & โข ((๐๐บ๐)๐บโ) = (๐๐บ(๐๐บโ)) โ โข ((๐ด๐น๐ต)๐น๐ถ) = (๐ด๐น(๐ต๐น๐ถ)) | ||
Theorem | plpv 10880* | Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด +P ๐ต) = {๐ฅ โฃ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ๐ฅ = (๐ฆ +Q ๐ง)}) | ||
Theorem | mpv 10881* | Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด ยทP ๐ต) = {๐ฅ โฃ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ๐ฅ = (๐ฆ ยทQ ๐ง)}) | ||
Theorem | dmplp 10882 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
โข dom +P = (P ร P) | ||
Theorem | dmmp 10883 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
โข dom ยทP = (P ร P) | ||
Theorem | nqpr 10884* | The canonical embedding of the rationals into the reals. (Contributed by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |
โข (๐ด โ Q โ {๐ฅ โฃ ๐ฅ <Q ๐ด} โ P) | ||
Theorem | 1pr 10885 | The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.) |
โข 1P โ P | ||
Theorem | addclprlem1 10886 | 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.) |
โข (((๐ด โ P โง ๐ โ ๐ด) โง ๐ฅ โ Q) โ (๐ฅ <Q (๐ +Q โ) โ ((๐ฅ ยทQ (*Qโ(๐ +Q โ))) ยทQ ๐) โ ๐ด)) | ||
Theorem | addclprlem2 10887* | 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.) |
โข ((((๐ด โ P โง ๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q (๐ +Q โ) โ ๐ฅ โ (๐ด +P ๐ต))) | ||
Theorem | addclpr 10888 | 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.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด +P ๐ต) โ P) | ||
Theorem | mulclprlem 10889* | 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.) |
โข ((((๐ด โ P โง ๐ โ ๐ด) โง (๐ต โ P โง โ โ ๐ต)) โง ๐ฅ โ Q) โ (๐ฅ <Q (๐ ยทQ โ) โ ๐ฅ โ (๐ด ยทP ๐ต))) | ||
Theorem | mulclpr 10890 | 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.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด ยทP ๐ต) โ P) | ||
Theorem | addcompr 10891 | 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.) |
โข (๐ด +P ๐ต) = (๐ต +P ๐ด) | ||
Theorem | addasspr 10892 | 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.) |
โข ((๐ด +P ๐ต) +P ๐ถ) = (๐ด +P (๐ต +P ๐ถ)) | ||
Theorem | mulcompr 10893 | 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.) |
โข (๐ด ยทP ๐ต) = (๐ต ยทP ๐ด) | ||
Theorem | mulasspr 10894 | 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.) |
โข ((๐ด ยทP ๐ต) ยทP ๐ถ) = (๐ด ยทP (๐ต ยทP ๐ถ)) | ||
Theorem | distrlem1pr 10895 | Lemma for distributive law for positive reals. (Contributed by NM, 1-May-1996.) (Revised by Mario Carneiro, 13-Jun-2013.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P โง ๐ถ โ P) โ (๐ด ยทP (๐ต +P ๐ถ)) โ ((๐ด ยทP ๐ต) +P (๐ด ยทP ๐ถ))) | ||
Theorem | distrlem4pr 10896* | Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |
โข (((๐ด โ P โง ๐ต โ P โง ๐ถ โ P) โง ((๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โง (๐ โ ๐ด โง ๐ง โ ๐ถ))) โ ((๐ฅ ยทQ ๐ฆ) +Q (๐ ยทQ ๐ง)) โ (๐ด ยทP (๐ต +P ๐ถ))) | ||
Theorem | distrlem5pr 10897 | Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P โง ๐ถ โ P) โ ((๐ด ยทP ๐ต) +P (๐ด ยทP ๐ถ)) โ (๐ด ยทP (๐ต +P ๐ถ))) | ||
Theorem | distrpr 10898 | 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.) |
โข (๐ด ยทP (๐ต +P ๐ถ)) = ((๐ด ยทP ๐ต) +P (๐ด ยทP ๐ถ)) | ||
Theorem | 1idpr 10899 | 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.) |
โข (๐ด โ P โ (๐ด ยทP 1P) = ๐ด) | ||
Theorem | ltprord 10900 | Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด<P ๐ต โ ๐ด โ ๐ต)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |