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