![]() |
Metamath
Proof Explorer Theorem List (p. 111 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 | genpcd 11001* | 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 11002* | 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 11003* | 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 11004* | 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 11005* | Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด +P ๐ต) = {๐ฅ โฃ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ๐ฅ = (๐ฆ +Q ๐ง)}) | ||
Theorem | mpv 11006* | Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด ยทP ๐ต) = {๐ฅ โฃ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ๐ฅ = (๐ฆ ยทQ ๐ง)}) | ||
Theorem | dmplp 11007 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
โข dom +P = (P ร P) | ||
Theorem | dmmp 11008 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
โข dom ยทP = (P ร P) | ||
Theorem | nqpr 11009* | 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 11010 | 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 11011 | 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 11012* | 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 11013 | 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 11014* | 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 11015 | 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 11016 | 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 11017 | 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 11018 | 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 11019 | 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 11020 | 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 11021* | 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 11022 | 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 11023 | 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 11024 | 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 11025 | Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด<P ๐ต โ ๐ด โ ๐ต)) | ||
Theorem | psslinpr 11026 | 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.) |
โข ((๐ด โ P โง ๐ต โ P) โ (๐ด โ ๐ต โจ ๐ด = ๐ต โจ ๐ต โ ๐ด)) | ||
Theorem | ltsopr 11027 | 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.) |
โข <P Or P | ||
Theorem | prlem934 11028* | 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.) |
โข ๐ต โ V โ โข (๐ด โ P โ โ๐ฅ โ ๐ด ยฌ (๐ฅ +Q ๐ต) โ ๐ด) | ||
Theorem | ltaddpr 11029 | 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.) |
โข ((๐ด โ P โง ๐ต โ P) โ ๐ด<P (๐ด +P ๐ต)) | ||
Theorem | ltaddpr2 11030 | The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
โข (๐ถ โ P โ ((๐ด +P ๐ต) = ๐ถ โ ๐ด<P ๐ถ)) | ||
Theorem | ltexprlem1 11031* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข (๐ต โ P โ (๐ด โ ๐ต โ ๐ถ โ โ )) | ||
Theorem | ltexprlem2 11032* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข (๐ต โ P โ ๐ถ โ Q) | ||
Theorem | ltexprlem3 11033* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข (๐ต โ P โ (๐ฅ โ ๐ถ โ โ๐ง(๐ง <Q ๐ฅ โ ๐ง โ ๐ถ))) | ||
Theorem | ltexprlem4 11034* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข (๐ต โ P โ (๐ฅ โ ๐ถ โ โ๐ง(๐ง โ ๐ถ โง ๐ฅ <Q ๐ง))) | ||
Theorem | ltexprlem5 11035* | Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข ((๐ต โ P โง ๐ด โ ๐ต) โ ๐ถ โ P) | ||
Theorem | ltexprlem6 11036* | 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.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข (((๐ด โ P โง ๐ต โ P) โง ๐ด โ ๐ต) โ (๐ด +P ๐ถ) โ ๐ต) | ||
Theorem | ltexprlem7 11037* | 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.) |
โข ๐ถ = {๐ฅ โฃ โ๐ฆ(ยฌ ๐ฆ โ ๐ด โง (๐ฆ +Q ๐ฅ) โ ๐ต)} โ โข (((๐ด โ P โง ๐ต โ P) โง ๐ด โ ๐ต) โ ๐ต โ (๐ด +P ๐ถ)) | ||
Theorem | ltexpri 11038* | 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.) |
โข (๐ด<P ๐ต โ โ๐ฅ โ P (๐ด +P ๐ฅ) = ๐ต) | ||
Theorem | ltaprlem 11039 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.) |
โข (๐ถ โ P โ (๐ด<P ๐ต โ (๐ถ +P ๐ด)<P (๐ถ +P ๐ต))) | ||
Theorem | ltapr 11040 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.) |
โข (๐ถ โ P โ (๐ด<P ๐ต โ (๐ถ +P ๐ด)<P (๐ถ +P ๐ต))) | ||
Theorem | addcanpr 11041 | 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.) |
โข ((๐ด โ P โง ๐ต โ P) โ ((๐ด +P ๐ต) = (๐ด +P ๐ถ) โ ๐ต = ๐ถ)) | ||
Theorem | prlem936 11042* | 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.) |
โข ((๐ด โ P โง 1Q <Q ๐ต) โ โ๐ฅ โ ๐ด ยฌ (๐ฅ ยทQ ๐ต) โ ๐ด) | ||
Theorem | reclem2pr 11043* | 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.) |
โข ๐ต = {๐ฅ โฃ โ๐ฆ(๐ฅ <Q ๐ฆ โง ยฌ (*Qโ๐ฆ) โ ๐ด)} โ โข (๐ด โ P โ ๐ต โ P) | ||
Theorem | reclem3pr 11044* | 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.) |
โข ๐ต = {๐ฅ โฃ โ๐ฆ(๐ฅ <Q ๐ฆ โง ยฌ (*Qโ๐ฆ) โ ๐ด)} โ โข (๐ด โ P โ 1P โ (๐ด ยทP ๐ต)) | ||
Theorem | reclem4pr 11045* | Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.) |
โข ๐ต = {๐ฅ โฃ โ๐ฆ(๐ฅ <Q ๐ฆ โง ยฌ (*Qโ๐ฆ) โ ๐ด)} โ โข (๐ด โ P โ (๐ด ยทP ๐ต) = 1P) | ||
Theorem | recexpr 11046* | 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.) |
โข (๐ด โ P โ โ๐ฅ โ P (๐ด ยทP ๐ฅ) = 1P) | ||
Theorem | suplem1pr 11047* | The union of a nonempty, 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.) |
โข ((๐ด โ โ โง โ๐ฅ โ P โ๐ฆ โ ๐ด ๐ฆ<P ๐ฅ) โ โช ๐ด โ P) | ||
Theorem | suplem2pr 11048* | 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.) |
โข (๐ด โ P โ ((๐ฆ โ ๐ด โ ยฌ โช ๐ด<P ๐ฆ) โง (๐ฆ<P โช ๐ด โ โ๐ง โ ๐ด ๐ฆ<P ๐ง))) | ||
Theorem | supexpr 11049* | The union of a nonempty, 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.) |
โข ((๐ด โ โ โง โ๐ฅ โ P โ๐ฆ โ ๐ด ๐ฆ<P ๐ฅ) โ โ๐ฅ โ P (โ๐ฆ โ ๐ด ยฌ ๐ฅ<P ๐ฆ โง โ๐ฆ โ P (๐ฆ<P ๐ฅ โ โ๐ง โ ๐ด ๐ฆ<P ๐ง))) | ||
Definition | df-enr 11050* | Define equivalence relation for signed 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-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
โข ~R = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (P ร P) โง ๐ฆ โ (P ร P)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง +P ๐ข) = (๐ค +P ๐ฃ)))} | ||
Definition | df-nr 11051 | Define class of signed 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-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
โข R = ((P ร P) / ~R ) | ||
Definition | df-plr 11052* | Define addition on signed 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-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
โข +R = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ R โง ๐ฆ โ R) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~R โง ๐ฆ = [โจ๐ข, ๐โฉ] ~R ) โง ๐ง = [โจ(๐ค +P ๐ข), (๐ฃ +P ๐)โฉ] ~R ))} | ||
Definition | df-mr 11053* | Define multiplication on signed 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-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
โข ยทR = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ R โง ๐ฆ โ R) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = [โจ๐ค, ๐ฃโฉ] ~R โง ๐ฆ = [โจ๐ข, ๐โฉ] ~R ) โง ๐ง = [โจ((๐ค ยทP ๐ข) +P (๐ฃ ยทP ๐)), ((๐ค ยทP ๐) +P (๐ฃ ยทP ๐ข))โฉ] ~R ))} | ||
Definition | df-ltr 11054* | Define ordering relation on signed 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-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |
โข <R = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ R โง ๐ฆ โ R) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~R โง ๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~R ) โง (๐ง +P ๐ข)<P (๐ค +P ๐ฃ)))} | ||
Definition | df-0r 11055 | Define signed real constant 0. 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-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
โข 0R = [โจ1P, 1Pโฉ] ~R | ||
Definition | df-1r 11056 | Define signed 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. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
โข 1R = [โจ(1P +P 1P), 1Pโฉ] ~R | ||
Definition | df-m1r 11057 | Define signed 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. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
โข -1R = [โจ1P, (1P +P 1P)โฉ] ~R | ||
Theorem | enrer 11058 | 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.) |
โข ~R Er (P ร P) | ||
Theorem | nrex1 11059 | The class of signed reals is a set. Note that a shorter proof is possible using qsex 8770 (and not requiring enrer 11058), but it would add a dependency on ax-rep 5286. (Contributed by Mario Carneiro, 17-Nov-2014.) Extract proof from that of axcnex 11142. (Revised by BJ, 4-Feb-2023.) (New usage is discouraged.) |
โข R โ V | ||
Theorem | enrbreq 11060 | Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
โข (((๐ด โ P โง ๐ต โ P) โง (๐ถ โ P โง ๐ท โ P)) โ (โจ๐ด, ๐ตโฉ ~R โจ๐ถ, ๐ทโฉ โ (๐ด +P ๐ท) = (๐ต +P ๐ถ))) | ||
Theorem | enreceq 11061 | Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.) |
โข (((๐ด โ P โง ๐ต โ P) โง (๐ถ โ P โง ๐ท โ P)) โ ([โจ๐ด, ๐ตโฉ] ~R = [โจ๐ถ, ๐ทโฉ] ~R โ (๐ด +P ๐ท) = (๐ต +P ๐ถ))) | ||
Theorem | enrex 11062 | The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
โข ~R โ V | ||
Theorem | ltrelsr 11063 | Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |
โข <R โ (R ร R) | ||
Theorem | addcmpblnr 11064 | Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
โข ((((๐ด โ P โง ๐ต โ P) โง (๐ถ โ P โง ๐ท โ P)) โง ((๐น โ P โง ๐บ โ P) โง (๐ โ P โง ๐ โ P))) โ (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐ )) โ โจ(๐ด +P ๐น), (๐ต +P ๐บ)โฉ ~R โจ(๐ถ +P ๐ ), (๐ท +P ๐)โฉ)) | ||
Theorem | mulcmpblnrlem 11065 | Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.) |
โข (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐ )) โ ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)) +P ((๐ถ ยทP ๐) +P (๐ท ยทP ๐ )))) = ((๐ท ยทP ๐น) +P (((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น)) +P ((๐ถ ยทP ๐ ) +P (๐ท ยทP ๐))))) | ||
Theorem | mulcmpblnr 11066 | Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.) |
โข ((((๐ด โ P โง ๐ต โ P) โง (๐ถ โ P โง ๐ท โ P)) โง ((๐น โ P โง ๐บ โ P) โง (๐ โ P โง ๐ โ P))) โ (((๐ด +P ๐ท) = (๐ต +P ๐ถ) โง (๐น +P ๐) = (๐บ +P ๐ )) โ โจ((๐ด ยทP ๐น) +P (๐ต ยทP ๐บ)), ((๐ด ยทP ๐บ) +P (๐ต ยทP ๐น))โฉ ~R โจ((๐ถ ยทP ๐ ) +P (๐ท ยทP ๐)), ((๐ถ ยทP ๐) +P (๐ท ยทP ๐ ))โฉ)) | ||
Theorem | prsrlem1 11067* | Decomposing signed reals into positive reals. Lemma for addsrpr 11070 and mulsrpr 11071. (Contributed by Jim Kingdon, 30-Dec-2019.) |
โข (((๐ด โ ((P ร P) / ~R ) โง ๐ต โ ((P ร P) / ~R )) โง ((๐ด = [โจ๐ค, ๐ฃโฉ] ~R โง ๐ต = [โจ๐ข, ๐กโฉ] ~R ) โง (๐ด = [โจ๐ , ๐โฉ] ~R โง ๐ต = [โจ๐, โโฉ] ~R ))) โ ((((๐ค โ P โง ๐ฃ โ P) โง (๐ โ P โง ๐ โ P)) โง ((๐ข โ P โง ๐ก โ P) โง (๐ โ P โง โ โ P))) โง ((๐ค +P ๐) = (๐ฃ +P ๐ ) โง (๐ข +P โ) = (๐ก +P ๐)))) | ||
Theorem | addsrmo 11068* | There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) |
โข ((๐ด โ ((P ร P) / ~R ) โง ๐ต โ ((P ร P) / ~R )) โ โ*๐งโ๐คโ๐ฃโ๐ขโ๐ก((๐ด = [โจ๐ค, ๐ฃโฉ] ~R โง ๐ต = [โจ๐ข, ๐กโฉ] ~R ) โง ๐ง = [โจ(๐ค +P ๐ข), (๐ฃ +P ๐ก)โฉ] ~R )) | ||
Theorem | mulsrmo 11069* | There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) |
โข ((๐ด โ ((P ร P) / ~R ) โง ๐ต โ ((P ร P) / ~R )) โ โ*๐งโ๐คโ๐ฃโ๐ขโ๐ก((๐ด = [โจ๐ค, ๐ฃโฉ] ~R โง ๐ต = [โจ๐ข, ๐กโฉ] ~R ) โง ๐ง = [โจ((๐ค ยทP ๐ข) +P (๐ฃ ยทP ๐ก)), ((๐ค ยทP ๐ก) +P (๐ฃ ยทP ๐ข))โฉ] ~R )) | ||
Theorem | addsrpr 11070 | 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.) |
โข (((๐ด โ P โง ๐ต โ P) โง (๐ถ โ P โง ๐ท โ P)) โ ([โจ๐ด, ๐ตโฉ] ~R +R [โจ๐ถ, ๐ทโฉ] ~R ) = [โจ(๐ด +P ๐ถ), (๐ต +P ๐ท)โฉ] ~R ) | ||
Theorem | mulsrpr 11071 | 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.) |
โข (((๐ด โ P โง ๐ต โ P) โง (๐ถ โ P โง ๐ท โ P)) โ ([โจ๐ด, ๐ตโฉ] ~R ยทR [โจ๐ถ, ๐ทโฉ] ~R ) = [โจ((๐ด ยทP ๐ถ) +P (๐ต ยทP ๐ท)), ((๐ด ยทP ๐ท) +P (๐ต ยทP ๐ถ))โฉ] ~R ) | ||
Theorem | ltsrpr 11072 | 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.) |
โข ([โจ๐ด, ๐ตโฉ] ~R <R [โจ๐ถ, ๐ทโฉ] ~R โ (๐ด +P ๐ท)<P (๐ต +P ๐ถ)) | ||
Theorem | gt0srpr 11073 | Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
โข (0R <R [โจ๐ด, ๐ตโฉ] ~R โ ๐ต<P ๐ด) | ||
Theorem | 0nsr 11074 | The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
โข ยฌ โ โ R | ||
Theorem | 0r 11075 | The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
โข 0R โ R | ||
Theorem | 1sr 11076 | The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
โข 1R โ R | ||
Theorem | m1r 11077 | The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
โข -1R โ R | ||
Theorem | addclsr 11078 | Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
โข ((๐ด โ R โง ๐ต โ R) โ (๐ด +R ๐ต) โ R) | ||
Theorem | mulclsr 11079 | Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
โข ((๐ด โ R โง ๐ต โ R) โ (๐ด ยทR ๐ต) โ R) | ||
Theorem | dmaddsr 11080 | Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
โข dom +R = (R ร R) | ||
Theorem | dmmulsr 11081 | Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
โข dom ยทR = (R ร R) | ||
Theorem | addcomsr 11082 | Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
โข (๐ด +R ๐ต) = (๐ต +R ๐ด) | ||
Theorem | addasssr 11083 | Addition of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
โข ((๐ด +R ๐ต) +R ๐ถ) = (๐ด +R (๐ต +R ๐ถ)) | ||
Theorem | mulcomsr 11084 | Multiplication of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
โข (๐ด ยทR ๐ต) = (๐ต ยทR ๐ด) | ||
Theorem | mulasssr 11085 | Multiplication of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
โข ((๐ด ยทR ๐ต) ยทR ๐ถ) = (๐ด ยทR (๐ต ยทR ๐ถ)) | ||
Theorem | distrsr 11086 | Multiplication of signed reals is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
โข (๐ด ยทR (๐ต +R ๐ถ)) = ((๐ด ยทR ๐ต) +R (๐ด ยทR ๐ถ)) | ||
Theorem | m1p1sr 11087 | Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
โข (-1R +R 1R) = 0R | ||
Theorem | m1m1sr 11088 | Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
โข (-1R ยทR -1R) = 1R | ||
Theorem | ltsosr 11089 | Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.) (New usage is discouraged.) |
โข <R Or R | ||
Theorem | 0lt1sr 11090 | 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.) |
โข 0R <R 1R | ||
Theorem | 1ne0sr 11091 | 1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.) |
โข ยฌ 1R = 0R | ||
Theorem | 0idsr 11092 | The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.) |
โข (๐ด โ R โ (๐ด +R 0R) = ๐ด) | ||
Theorem | 1idsr 11093 | 1 is an identity element for multiplication. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
โข (๐ด โ R โ (๐ด ยทR 1R) = ๐ด) | ||
Theorem | 00sr 11094 | A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.) |
โข (๐ด โ R โ (๐ด ยทR 0R) = 0R) | ||
Theorem | ltasr 11095 | Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
โข (๐ถ โ R โ (๐ด <R ๐ต โ (๐ถ +R ๐ด) <R (๐ถ +R ๐ต))) | ||
Theorem | pn0sr 11096 | A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
โข (๐ด โ R โ (๐ด +R (๐ด ยทR -1R)) = 0R) | ||
Theorem | negexsr 11097* | Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
โข (๐ด โ R โ โ๐ฅ โ R (๐ด +R ๐ฅ) = 0R) | ||
Theorem | recexsrlem 11098* | The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
โข (0R <R ๐ด โ โ๐ฅ โ R (๐ด ยทR ๐ฅ) = 1R) | ||
Theorem | addgt0sr 11099 | The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
โข ((0R <R ๐ด โง 0R <R ๐ต) โ 0R <R (๐ด +R ๐ต)) | ||
Theorem | mulgt0sr 11100 | The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
โข ((0R <R ๐ด โง 0R <R ๐ต) โ 0R <R (๐ด ยทR ๐ต)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |