![]() |
Metamath
Proof Explorer Theorem List (p. 110 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nlt1pi 10901 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
โข ยฌ ๐ด <N 1o | ||
Theorem | indpi 10902* | Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
โข (๐ฅ = 1o โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข (๐ฅ = (๐ฆ +N 1o) โ (๐ โ ๐)) & โข (๐ฅ = ๐ด โ (๐ โ ๐)) & โข ๐ & โข (๐ฆ โ N โ (๐ โ ๐)) โ โข (๐ด โ N โ ๐) | ||
Definition | df-plpq 10903* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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 +Q (df-plq 10909) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10906). (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.) |
โข +pQ = (๐ฅ โ (N ร N), ๐ฆ โ (N ร N) โฆ โจ(((1st โ๐ฅ) ยทN (2nd โ๐ฆ)) +N ((1st โ๐ฆ) ยทN (2nd โ๐ฅ))), ((2nd โ๐ฅ) ยทN (2nd โ๐ฆ))โฉ) | ||
Definition | df-mpq 10904* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข ยทpQ = (๐ฅ โ (N ร N), ๐ฆ โ (N ร N) โฆ โจ((1st โ๐ฅ) ยทN (1st โ๐ฆ)), ((2nd โ๐ฅ) ยทN (2nd โ๐ฆ))โฉ) | ||
Definition | df-ltpq 10905* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข <pQ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร N) โง ๐ฆ โ (N ร N)) โง ((1st โ๐ฅ) ยทN (2nd โ๐ฆ)) <N ((1st โ๐ฆ) ยทN (2nd โ๐ฅ)))} | ||
Definition | df-enq 10906* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข ~Q = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร N) โง ๐ฆ โ (N ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ)))} | ||
Definition | df-nq 10907* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข Q = {๐ฅ โ (N ร N) โฃ โ๐ฆ โ (N ร N)(๐ฅ ~Q ๐ฆ โ ยฌ (2nd โ๐ฆ) <N (2nd โ๐ฅ))} | ||
Definition | df-erq 10908 | 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 10925. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
โข [Q] = ( ~Q โฉ ((N ร N) ร Q)) | ||
Definition | df-plq 10909 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข +Q = (([Q] โ +pQ ) โพ (Q ร Q)) | ||
Definition | df-mq 10910 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข ยทQ = (([Q] โ ยทpQ ) โพ (Q ร Q)) | ||
Definition | df-1nq 10911 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข 1Q = โจ1o, 1oโฉ | ||
Definition | df-rq 10912 | 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 11116, 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.) |
โข *Q = (โก ยทQ โ {1Q}) | ||
Definition | df-ltnq 10913 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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.) |
โข <Q = ( <pQ โฉ (Q ร Q)) | ||
Theorem | enqbreq 10914 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
โข (((๐ด โ N โง ๐ต โ N) โง (๐ถ โ N โง ๐ท โ N)) โ (โจ๐ด, ๐ตโฉ ~Q โจ๐ถ, ๐ทโฉ โ (๐ด ยทN ๐ท) = (๐ต ยทN ๐ถ))) | ||
Theorem | enqbreq2 10915 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N)) โ (๐ด ~Q ๐ต โ ((1st โ๐ด) ยทN (2nd โ๐ต)) = ((1st โ๐ต) ยทN (2nd โ๐ด)))) | ||
Theorem | enqer 10916 | 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.) |
โข ~Q Er (N ร N) | ||
Theorem | enqex 10917 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
โข ~Q โ V | ||
Theorem | nqex 10918 | The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |
โข Q โ V | ||
Theorem | 0nnq 10919 | 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.) |
โข ยฌ โ โ Q | ||
Theorem | elpqn 10920 | 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.) |
โข (๐ด โ Q โ ๐ด โ (N ร N)) | ||
Theorem | ltrelnq 10921 | 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.) |
โข <Q โ (Q ร Q) | ||
Theorem | pinq 10922 | 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.) |
โข (๐ด โ N โ โจ๐ด, 1oโฉ โ Q) | ||
Theorem | 1nq 10923 | The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข 1Q โ Q | ||
Theorem | nqereu 10924* | There is a unique element of Q equivalent to each element of N ร N. (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
โข (๐ด โ (N ร N) โ โ!๐ฅ โ Q ๐ฅ ~Q ๐ด) | ||
Theorem | nqerf 10925 | Corollary of nqereu 10924: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข [Q]:(N ร N)โถQ | ||
Theorem | nqercl 10926 | Corollary of nqereu 10924: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข (๐ด โ (N ร N) โ ([Q]โ๐ด) โ Q) | ||
Theorem | nqerrel 10927 | 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 10928 | Corollary of nqereu 10924: 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 10929 | Corollary of nqereu 10924: 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 10930 | 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 10931 | 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 10932 | 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 10933 | 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 10934 | 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 10935 | 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 10936 | 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 10937 | 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 10938 | 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 10939 | 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 10940 | 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 10941 | 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 10942 | 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 10943 | 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 10944 | 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 10945 | 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 10946 | 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 10947 | 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 10948 | 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 10949 | Lemma for adderpq 10951. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N) โง ๐ถ โ (N ร N)) โ (๐ด ~Q ๐ต โ (๐ด +pQ ๐ถ) ~Q (๐ต +pQ ๐ถ))) | ||
Theorem | mulerpqlem 10950 | Lemma for mulerpq 10952. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N) โง ๐ถ โ (N ร N)) โ (๐ด ~Q ๐ต โ (๐ด ยทpQ ๐ถ) ~Q (๐ต ยทpQ ๐ถ))) | ||
Theorem | adderpq 10951 | 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 10952 | 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 10953 | 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 10954 | 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 10955 | 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 10956 | 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 10957 | 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 10958 | 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 10959 | 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 10960 | 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 10961 | 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 10962 | 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 10963 | 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 10964 | '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 10965 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |
โข (๐ด <pQ ๐ต โ ([Q]โ๐ด) <Q ([Q]โ๐ต)) | ||
Theorem | ltanq 10966 | 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 10967 | 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 10968 | 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 10969 | 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 10970* | 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 10971* | 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 10972* | 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 10973* | 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 10974 | 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 10975* | 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 10976* | 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 11116, 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 10977 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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 10978* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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 10979* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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 10980* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11116, 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 10981 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
โข P โ V | ||
Theorem | elnp 10982* | Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.) |
โข (๐ด โ P โ ((โ โ ๐ด โง ๐ด โ Q) โง โ๐ฅ โ ๐ด (โ๐ฆ(๐ฆ <Q ๐ฅ โ ๐ฆ โ ๐ด) โง โ๐ฆ โ ๐ด ๐ฅ <Q ๐ฆ))) | ||
Theorem | elnpi 10983* | Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
โข (๐ด โ P โ ((๐ด โ V โง โ โ ๐ด โง ๐ด โ Q) โง โ๐ฅ โ ๐ด (โ๐ฆ(๐ฆ <Q ๐ฅ โ ๐ฆ โ ๐ด) โง โ๐ฆ โ ๐ด ๐ฅ <Q ๐ฆ))) | ||
Theorem | prn0 10984 | 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 10985 | 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 10986 | 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 10987 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |
โข ยฌ โ โ P | ||
Theorem | prcdnq 10988 | 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 10989 | 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 10990* | 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 10991 | 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 10988 and nsmallnq 10972). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |
โข (๐ด โ P โ ฯ โ V) | ||
Theorem | prnmadd 10992* | 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 10993 | 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 10994* | 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 10995* | 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 10996* | 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 10997* | 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 10998* | 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 10999* | 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 11000* | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |