![]() |
Metamath
Proof Explorer Theorem List (p. 111 of 489) | < 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-30950) |
![]() (30951-32473) |
![]() (32474-48899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nqerrel 11001 | 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 11002 | Corollary of nqereu 10998: 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 11003 | Corollary of nqereu 10998: 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 11004 | 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 11005 | 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 11006 | 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 11007 | 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 11008 | 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 11009 | 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 11010 | 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 11011 | 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 11012 | 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 11013 | 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 11014 | 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 11015 | 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 11016 | 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 11017 | 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 11018 | 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 11019 | 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 11020 | 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 11021 | 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 11022 | 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 11023 | Lemma for adderpq 11025. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 +pQ 𝐶) ~Q (𝐵 +pQ 𝐶))) | ||
Theorem | mulerpqlem 11024 | Lemma for mulerpq 11026. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 ·pQ 𝐶) ~Q (𝐵 ·pQ 𝐶))) | ||
Theorem | adderpq 11025 | 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 11026 | 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 11027 | 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 11028 | 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 11029 | 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 11030 | 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 11031 | 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 11032 | 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 11033 | 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 11034 | 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 11035 | 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 11036 | 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 11037 | 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 11038 | '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 11039 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 <pQ 𝐵 ↔ ([Q]‘𝐴) <Q ([Q]‘𝐵)) | ||
Theorem | ltanq 11040 | 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 11041 | 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 11042 | 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 11043 | 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 11044* | 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 11045* | 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 11046* | 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 11047* | 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 11048 | 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 11049* | 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 11050* | 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 11190, 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 11051 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11190, 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 11052* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11190, 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 11053* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11190, 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 11054* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 11190, 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 11055 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
⊢ P ∈ V | ||
Theorem | elnp 11056* | Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P ↔ ((∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) | ||
Theorem | elnpi 11057* | Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P ↔ ((𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) | ||
Theorem | prn0 11058 | 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 11059 | 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 11060 | 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 11061 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ P | ||
Theorem | prcdnq 11062 | 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 11063 | 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 11064* | 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 11065 | 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 11062 and nsmallnq 11046). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P → ω ∈ V) | ||
Theorem | prnmadd 11066* | 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 11067 | 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 11068* | 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 11069* | 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 11070* | 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 11071* | 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 11072* | 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 11073* | 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 11074* | 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 11075* | 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 11076* | 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 11077* | 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 11078* | 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 11079* | Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦 +Q 𝑧)}) | ||
Theorem | mpv 11080* | Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦 ·Q 𝑧)}) | ||
Theorem | dmplp 11081 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
⊢ dom +P = (P × P) | ||
Theorem | dmmp 11082 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
⊢ dom ·P = (P × P) | ||
Theorem | nqpr 11083* | 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 11084 | 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 11085 | 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 11086* | 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 11087 | 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 11088* | 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 11089 | 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 11090 | 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 11091 | 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 11092 | 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 11093 | 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 11094 | 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 11095* | 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 11096 | 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 11097 | 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 11098 | 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 11099 | Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<P 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | psslinpr 11100 | 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) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |