Home | Metamath
Proof Explorer Theorem List (p. 105 of 449) | < 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: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elprnq 10401 | 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 10402 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ P | ||
Theorem | prcdnq 10403 | 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 10404 | 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 10405* | 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 10406 | 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 10403 and nsmallnq 10387). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P → ω ∈ V) | ||
Theorem | prnmadd 10407* | 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 10408 | 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 10409* | 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 10410* | 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 10411* | 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 10412* | 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 10413* | 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 10414* | 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 10415* | 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 10416* | 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 10417* | 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 10418* | 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 10419* | 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 10420* | Value of addition on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +P 𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦 +Q 𝑧)}) | ||
Theorem | mpv 10421* | Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·P 𝐵) = {𝑥 ∣ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝑥 = (𝑦 ·Q 𝑧)}) | ||
Theorem | dmplp 10422 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
⊢ dom +P = (P × P) | ||
Theorem | dmmp 10423 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
⊢ dom ·P = (P × P) | ||
Theorem | nqpr 10424* | 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 10425 | 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 10426 | 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 10427* | 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 10428 | 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 10429* | 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 10430 | 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 10431 | 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 10432 | 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 10433 | 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 10434 | 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 10435 | 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 10436* | 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 10437 | 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 10438 | 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 10439 | 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 10440 | Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<P 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | psslinpr 10441 | 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 10442 | 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 10443* | 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 10444 | 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 10445 | 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 10446* | 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 10447* | 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 10448* | 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 10449* | 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 10450* | 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 10451* | 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 10452* | 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 10453* | 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 10454 | 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 10455 | 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 10456 | 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 10457* | 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 10458* | 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 10459* | 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 10460* | 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 10461* | 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 10462* | 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 10463* | 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 10464* | 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 10465* | Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10466 | Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10467* | Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10468* | Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10469* | Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10470 | Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10471 | Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10472 | Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10473 | 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 10474 | The class of signed reals is a set. Note that a shorter proof is possible using qsex 8345 (and not requiring enrer 10473), but it would add a dependency on ax-rep 5181. (Contributed by Mario Carneiro, 17-Nov-2014.) Extract proof from that of axcnex 10557. (Revised by BJ, 4-Feb-2023.) (New usage is discouraged.) |
⊢ R ∈ V | ||
Theorem | enrbreq 10475 | 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 10476 | 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 10477 | The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
⊢ ~R ∈ V | ||
Theorem | ltrelsr 10478 | 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 10479 | 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 10480 | 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 10481 | 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 10482* | Decomposing signed reals into positive reals. Lemma for addsrpr 10485 and mulsrpr 10486. (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 10483* | 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 10484* | 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 10485 | 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 10486 | 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 10487 | 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 10488 | Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (0R <R [〈𝐴, 𝐵〉] ~R ↔ 𝐵<P 𝐴) | ||
Theorem | 0nsr 10489 | 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 10490 | The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
⊢ 0R ∈ R | ||
Theorem | 1sr 10491 | The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
⊢ 1R ∈ R | ||
Theorem | m1r 10492 | The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
⊢ -1R ∈ R | ||
Theorem | addclsr 10493 | Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) ∈ R) | ||
Theorem | mulclsr 10494 | Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R) | ||
Theorem | dmaddsr 10495 | Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
⊢ dom +R = (R × R) | ||
Theorem | dmmulsr 10496 | Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
⊢ dom ·R = (R × R) | ||
Theorem | addcomsr 10497 | 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 10498 | 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 10499 | 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 10500 | 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 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |