![]() |
Metamath
Proof Explorer Theorem List (p. 110 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ltexpi 10901* | Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |
โข ((๐ด โ N โง ๐ต โ N) โ (๐ด <N ๐ต โ โ๐ฅ โ N (๐ด +N ๐ฅ) = ๐ต)) | ||
Theorem | ltapi 10902 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |
โข (๐ถ โ N โ (๐ด <N ๐ต โ (๐ถ +N ๐ด) <N (๐ถ +N ๐ต))) | ||
Theorem | ltmpi 10903 | Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
โข (๐ถ โ N โ (๐ด <N ๐ต โ (๐ถ ยทN ๐ด) <N (๐ถ ยทN ๐ต))) | ||
Theorem | 1lt2pi 10904 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |
โข 1o <N (1o +N 1o) | ||
Theorem | nlt1pi 10905 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
โข ยฌ ๐ด <N 1o | ||
Theorem | indpi 10906* | 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 10907* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10913) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10910). (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 10908* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10909* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10910* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10911* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10912 | 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 10929. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
โข [Q] = ( ~Q โฉ ((N ร N) ร Q)) | ||
Definition | df-plq 10913 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10914 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10915 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10916 | 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 11120, 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 10917 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10918 | 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 10919 | 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 10920 | 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 10921 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
โข ~Q โ V | ||
Theorem | nqex 10922 | 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 10923 | 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 10924 | 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 10925 | 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 10926 | 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 10927 | 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 10928* | 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 10929 | Corollary of nqereu 10928: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข [Q]:(N ร N)โถQ | ||
Theorem | nqercl 10930 | Corollary of nqereu 10928: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
โข (๐ด โ (N ร N) โ ([Q]โ๐ด) โ Q) | ||
Theorem | nqerrel 10931 | 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 10932 | Corollary of nqereu 10928: 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 10933 | Corollary of nqereu 10928: 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 10934 | 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 10935 | 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 10936 | 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 10937 | 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 10938 | 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 10939 | 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 10940 | 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 10941 | 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 10942 | 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 10943 | 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 10944 | 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 10945 | 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 10946 | 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 10947 | 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 10948 | 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 10949 | 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 10950 | 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 10951 | 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 10952 | 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 10953 | Lemma for adderpq 10955. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N) โง ๐ถ โ (N ร N)) โ (๐ด ~Q ๐ต โ (๐ด +pQ ๐ถ) ~Q (๐ต +pQ ๐ถ))) | ||
Theorem | mulerpqlem 10954 | Lemma for mulerpq 10956. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
โข ((๐ด โ (N ร N) โง ๐ต โ (N ร N) โง ๐ถ โ (N ร N)) โ (๐ด ~Q ๐ต โ (๐ด ยทpQ ๐ถ) ~Q (๐ต ยทpQ ๐ถ))) | ||
Theorem | adderpq 10955 | 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 10956 | 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 10957 | 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 10958 | 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 10959 | 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 10960 | 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 10961 | 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 10962 | 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 10963 | 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 10964 | 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 10965 | 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 10966 | 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 10967 | 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 10968 | '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 10969 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |
โข (๐ด <pQ ๐ต โ ([Q]โ๐ด) <Q ([Q]โ๐ต)) | ||
Theorem | ltanq 10970 | 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 10971 | 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 10972 | 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 10973 | 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 10974* | 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 10975* | 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 10976* | 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 10977* | 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 10978 | 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 10979* | 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 10980* | 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 11120, 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 10981 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10982* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10983* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10984* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11120, 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 10985 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
โข P โ V | ||
Theorem | elnp 10986* | Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.) |
โข (๐ด โ P โ ((โ โ ๐ด โง ๐ด โ Q) โง โ๐ฅ โ ๐ด (โ๐ฆ(๐ฆ <Q ๐ฅ โ ๐ฆ โ ๐ด) โง โ๐ฆ โ ๐ด ๐ฅ <Q ๐ฆ))) | ||
Theorem | elnpi 10987* | Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
โข (๐ด โ P โ ((๐ด โ V โง โ โ ๐ด โง ๐ด โ Q) โง โ๐ฅ โ ๐ด (โ๐ฆ(๐ฆ <Q ๐ฅ โ ๐ฆ โ ๐ด) โง โ๐ฆ โ ๐ด ๐ฅ <Q ๐ฆ))) | ||
Theorem | prn0 10988 | 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 10989 | 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 10990 | 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 10991 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |
โข ยฌ โ โ P | ||
Theorem | prcdnq 10992 | 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 10993 | 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 10994* | 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 10995 | 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 10992 and nsmallnq 10976). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |
โข (๐ด โ P โ ฯ โ V) | ||
Theorem | prnmadd 10996* | 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 10997 | 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 10998* | 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 10999* | 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 11000* | 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) โ ((๐ถ โ ๐ด โง ๐ท โ ๐ต) โ (๐ถ๐บ๐ท) โ (๐ด๐น๐ต))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |