Statement List for Metamath Proof Explorer - 3901-4000 - Page 40 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | genpss 3901 |
The result of an operation on positive reals is a subset of the
positive fractions.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ ((g ∈ Q ∧ h ∈ Q) → (gGh) ∈ Q)
⇒ ⊢ ((A ∈ P ∧ B ∈ P) → (AFB) ⊆ Q) |
| |
| Theorem | genpnnp 3902 |
The result of an operation on positive reals is different from
the set of positive fractions.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ ((w ∈ Q ∧ v ∈ Q) → (wGv) ∈ Q)
& ⊢ (z ∈ Q → (x <Q y ↔ (zGx) <Q (zGy))) & ⊢ (xGy) = (yGx) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → ¬ (AFB) =
Q) |
| |
| Theorem | genpcd 3903 |
Downward closure of an operation on positive reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ ((((A ∈ P ∧ g ∈ A)
∧ (B ∈ P ∧
h ∈ B)) ∧ x
∈ Q) → (x
<Q (gGh) →
x ∈ (AFB)))
⇒ ⊢ ((A ∈ P ∧ B ∈ P) → (f ∈ (AFB) → (x
<Q f →
x ∈ (AFB)))) |
| |
| Theorem | genpnmax 3904 |
An operation on positive reals has no largest member.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ (v ∈ Q → (z <Q w ↔ (vGz) <Q (vGw))) & ⊢ (zGw) = (wGz) ⇒ ⊢ ((A ∈
P ∧ B ∈
P) → (f ∈
(AFB) →
∃x(x ∈ (AFB) ∧ f
<Q x))) |
| |
| Theorem | genpcl 3905 |
Closure of an operation on reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ ((x ∈ Q ∧ y ∈ Q) → (xGy) ∈ Q)
& ⊢ (h ∈ Q → (f <Q g ↔ (hGf) <Q (hGg))) & ⊢ (xGy) = (yGx) & ⊢ ((((A
∈ P ∧ g ∈
A) ∧ (B ∈ P ∧ h ∈ B))
∧ x ∈ Q) →
(x <Q
(gGh) →
x ∈ (AFB)))
⇒ ⊢ ((A ∈ P ∧ B ∈ P) → (AFB) ∈ P) |
| |
| Theorem | genpass 3906 |
Associativity of an operation on reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ∧ v ∈ P) ∧ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ dom F = (P ×
P) & ⊢ ((f ∈
P ∧ g ∈
P) → (fFg) ∈
P) & ⊢ ((fGg)Gh) = (fG(gGh))
⇒ ⊢ ((AFB)FC) = (AF(BFC)) |
| |
| Theorem | plpv 3907 |
Value of addition on positive reals.
|
| ⊢
((A ∈ P ∧
B ∈ P) → (A +P B) = {x∣∃y∃z((y ∈
A ∧ z ∈ B)
∧ x = (y +Q z))}) |
| |
| Theorem | mpv 3908 |
Value of multiplication on positive reals.
|
| ⊢
((A ∈ P ∧
B ∈ P) → (A ·P B) = {x∣∃y∃z((y ∈
A ∧ z ∈ B)
∧ x = (y ·Q z))}) |
| |
| Theorem | dmplp 3909 |
Domain of addition on positive reals.
|
| ⊢
dom +P = (P ×
P) |
| |
| Theorem | dmmp 3910 |
Domain of multiplication on positive reals.
|
| ⊢
dom ·P = (P ×
P) |
| |
| Theorem | 1pr 3911 |
The positive real number 'one'.
|
| ⊢
1P ∈ P |
| |
| Theorem | addclprlem1 3912 |
Lemma to prove downward closure in positive real addition. Part of
proof of Proposition 9-3.5 of [Gleason]
p. 123.
|
| ⊢
(((A ∈ P ∧
g ∈ A) ∧ x
∈ Q) → (x
<Q (g
+Q h) →
((x ·Q
(*Q ‘(g
+Q h)))
·Q g)
∈ A)) |
| |
| Theorem | addclprlem2 3913 |
Lemma to prove downward closure in positive real addition. Part of
proof of Proposition 9-3.5 of [Gleason]
p. 123.
|
| ⊢
((((A ∈ P ∧
g ∈ A) ∧ (B
∈ P ∧ h ∈
B)) ∧ x ∈ Q) → (x <Q (g +Q h) → x
∈ (A +P
B))) |
| |
| Theorem | addclpr 3914 |
Closure of addition on positive reals. First statement of
Proposition 9-3.5 of [Gleason] p. 123.
|
| ⊢
((A ∈ P ∧
B ∈ P) → (A +P B) ∈ P) |
| |
| Theorem | mulclprlem 3915 |
Lemma to prove downward closure in positive real multiplication. Part
of proof of Proposition 9-3.7 of [Gleason] p. 124.
|
| ⊢
((((A ∈ P ∧
g ∈ A) ∧ (B
∈ P ∧ h ∈
B)) ∧ x ∈ Q) → (x <Q (g ·Q h) → x
∈ (A
·P B))) |
| |
| Theorem | mulclpr 3916 |
Closure of multiplication on positive reals. First statement of
Proposition 9-3.7 of [Gleason] p. 124.
|
| ⊢
((A ∈ P ∧
B ∈ P) → (A ·P B) ∈ P) |
| |
| Theorem | addcompr 3917 |
Addition of positive reals is commutative. Proposition 9-3.5(ii) of
[Gleason] p. 123.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A +P B) = (B
+P A) |
| |
| Theorem | addasspr 3918 |
Addition of positive reals is associative. Proposition 9-3.5(i) of
[Gleason] p. 123.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A +P B) +P C) = (A
+P (B
+P C)) |
| |
| Theorem | mulcompr 3919 |
Multiplication of positive reals is commutative. Proposition
9-3.7(ii) of [Gleason] p. 124.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ·P B) = (B
·P A) |
| |
| Theorem | mulasspr 3920 |
Multiplication of positive reals is associative. Proposition 9-3.7(i)
of [Gleason] p. 124.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ·P B) ·P C) = (A
·P (B
·P C)) |
| |
| Theorem | distrlem1pr 3921 |
Lemma for distributive law for positive reals.
|
| ⊢
((A ∈ P ∧
(B ∈ P ∧ C ∈ P)) → (A ·P (B +P C)) ⊆ ((A
·P B)
+P (A
·P C))) |
| |
| Theorem | distrlem2pr 3922 |
Lemma for distributive law for positive reals.
|
| ⊢
((A ∈ P ∧
(B ∈ P ∧ C ∈ P)) → ((x ∈ A
∧ (y ∈ B ∧ z
∈ C)) → ((x ·Q y) +Q (x ·Q z)) ∈ (A
·P (B
+P C)))) |
| |
| Theorem | distrlem3pr 3923 |
Lemma for distributive law for positive reals.
|
| ⊢
(((A ∈ P ∧
(B ∈ P ∧ C ∈ P)) ∧ (x ∈ A
∧ (y ∈ B ∧ z
∈ C))) → (x ∈ Q ∧ (y ∈ Q ∧ z ∈ Q))) |
| |
| Theorem | distrlem4pr 3924 |
Lemma for distributive law for positive reals.
|
| ⊢
(((A ∈ P ∧
(B ∈ P ∧ C ∈ P)) ∧ ((x ∈ A
∧ f ∈ A) ∧ (y
∈ B ∧ z ∈ C)))
→ ((x
·Q y)
+Q (f
·Q z))
∈ (A
·P (B
+P C))) |
| |
| Theorem | distrlem5pr 3925 |
Lemma for distributive law for positive reals.
|
| ⊢
((A ∈ P ∧
(B ∈ P ∧ C ∈ P)) → ((A ·P B) +P (A ·P C)) ⊆ (A
·P (B
+P C))) |
| |
| Theorem | distrpr 3926 |
Multiplication of positive reals is distributive. Proposition
9-3.7(iii) of [Gleason] p. 124.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ·P (B +P C)) = ((A
·P B)
+P (A
·P C)) |
| |
| Theorem | 1idpr 3927 |
1 is an identity element for positive real multiplication. Theorem
9-3.7(iv) of [Gleason] p. 124.
|
| ⊢
(A ∈ P →
(A ·P
1P) = A) |
| |
| Theorem | ltprord 3928 |
Positive real 'less than' in terms of proper subset.
|
| ⊢
((A ∈ P ∧
B ∈ P) → (A<P B ↔ A
⊂ B)) |
| |
| Theorem | psslinpr 3929 |
Proper subset is a linear ordering on positive reals. Part of
Proposition 9-3.3 of [Gleason] p. 122.
|
| ⊢
((A ∈ P ∧
B ∈ P) → (A ⊂ B ∨
A = B
∨ B ⊂ A)) |
| |
| Theorem | ltsopr 3930 |
Positive real 'less than' is a strict ordering. Part of Proposition
9-3.3 of [Gleason] p. 122.
|
| ⊢
<P Or P |
| |
| Theorem | prlem934a 3931 |
Sublemma for Lemma 9-3.4 of [Gleason] p. 122.
|
| ⊢
B ∈ V
⇒ ⊢ (C ∈ N → (((B ∈ Q ∧ ∀x(x ∈
A → (x +Q B) ∈ A))
∧ y ∈ A) → (y
+Q ([⟨C,
1o⟩] ~Q
·Q B))
∈ A)) |
| |
| Theorem | prlem934b 3932 |
Sublemma for Lemma 9-3.4 of [Gleason] p. 122.
|
| ⊢
(((u ∈ N ∧
w ∈ N) ∧ (v ∈ N ∧ z ∈ N)) →
(([⟨(w
·N v),
1o⟩] ~Q
·Q [⟨z, w⟩]
~Q ) = [⟨v,
u⟩] ~Q ∨
[⟨v, u⟩] ~Q
<Q ([⟨(w
·N v),
1o⟩] ~Q
·Q [⟨z, w⟩]
~Q ))) |
| |
| Theorem | prlem934 3933 |
Lemma 9-3.4 of [Gleason] p. 122.
|
| ⊢
((A ∈ P ∧
B ∈ Q) →
∃x(x ∈ A
∧ ¬ (x +Q
B) ∈ A)) |
| |
| Theorem | ltaddpr 3934 |
The sum of two positive reals is greater than one of them. Proposition
9-3.5(iii) of [Gleason] p. 123.
|
| ⊢
((A ∈ P ∧
B ∈ P) → A<P (A +P B)) |
| |
| Theorem | ltaddpr2 3935 |
The sum of two positive reals is greater than one of them.
|
| ⊢
B ∈ V
⇒ ⊢ (C ∈ P → ((A +P B) = C →
A<P C)) |
| |
| Theorem | ltexprlem1 3936 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ (B ∈ P → (A ⊂ B
→ ¬ C = ∅)) |
| |
| Theorem | ltexprlem2 3937 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ (B ∈ P → C ⊂ Q) |
| |
| Theorem | ltexprlem3 3938 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ (B ∈ P → (x ∈ C
→ ∀z(z <Q x → z
∈ C))) |
| |
| Theorem | ltexprlem4 3939 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ (B ∈ P → (x ∈ C
→ ∃z(z ∈ C
∧ x <Q
z))) |
| |
| Theorem | ltexprlem5 3940 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ ((B ∈ P ∧ A ⊂ B)
→ C ∈ P) |
| |
| Theorem | ltexprlem6 3941 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ (((A ∈ P ∧ B ∈ P) ∧ A ⊂ B)
→ (A +P
C) ⊆ B) |
| |
| Theorem | ltexprlem7 3942 |
Lemma for Proposition 9-3.5(iv) of [Gleason]
p. 123.
|
| ⊢
C = {x∣∃y(¬ y
∈ A ∧ (y +Q x) ∈ B)}
⇒ ⊢ (((A ∈ P ∧ B ∈ P) ∧ A ⊂ B)
→ B ⊆ (A +P C)) |
| |
| Theorem | ltexpri 3943 |
Proposition 9-3.5(iv) of [Gleason] p. 123.
|
| ⊢
B ∈ V
⇒ ⊢ (A<P B → ∃x(x ∈
P ∧ (A
+P x) = B)) |
| |
| Theorem | ltaprlem 3944 |
Lemma for Proposition 9-3.5(v) of [Gleason] p.
123.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (C ∈ P → (A<P B → (C
+P A)<P (C +P B))) |
| |
| Theorem | ltapr 3945 |
Ordering property of addition. Proposition 9-3.5(v) of [Gleason]
p. 123.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (C ∈ P → (A<P B ↔ (C
+P A)<P (C +P B))) |
| |
| Theorem | addcanpr 3946 |
Addition cancellation law for positive reals. Proposition 9-3.5(vi)
of [Gleason] p. 123.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ∈ P ∧ B ∈ P) → ((A +P B) = (A
+P C) →
B = C)) |
| |
| Theorem | prlem936a 3947 |
Sublemma for Lemma 9-3.6 of [Gleason] p. 124.
This is a property of
positive fractions.
|
| ⊢
((x ∈ Q ∧
(z ∈ Q ∧ y ∈ Q)) → ((y +Q z) <Q (x +Q z) ↔ (x
+Q z)
<Q ((x
·Q (*Q
‘y))
·Q (y
+Q z)))) |
| |
| Theorem | prlem936b 3948 |
Sublemma for Lemma 9-3.6 of [Gleason] p. 124.
|
| ⊢
(((y
·Q B)
∈ A ∧ φ) → (y +Q z) ∈ A) & ⊢ (((A ∈
P ∧ (y
+Q z) ∈
A) ∧ (x ∈ Q ∧ z ∈ Q)) → (ψ → χ))
& ⊢ ((x ∈ Q ∧ (z ∈ Q ∧ y ∈ Q)) → (χ ↔ θ))
& ⊢
((((1Q <Q B ∧ x
∈ Q) ∧ y ∈
Q) ∧ φ) →
(θ ↔ τ))
& ⊢ ((A ∈ P ∧ τ) → (ψ → ¬ (x ·Q B) ∈ A))
⇒ ⊢ (((A ∈ P ∧ z ∈ Q) ∧ ((φ ∧ y ∈ Q) ∧
(1Q <Q B ∧ (y
·Q B)
∈ A))) → ((x ∈ A
∧ ψ) → (x ∈ A
∧ ¬ (x
·Q B)
∈ A))) |
| |
| Theorem | prlem936 3949 |
Lemma 9-3.6 of [Gleason] p. 124.
|
| ⊢
B ∈ V
⇒ ⊢ ((A ∈ P ∧
1Q <Q B) → ∃x(x ∈
A ∧ ¬ (x ·Q B) ∈ A)) |
| |
| Theorem | reclem1pr 3950 |
Lemma for Proposition 9-3.7 of [Gleason] p.
124.
|
| ⊢
B = {x∣∃y(x
<Q y ∧
¬ (*Q ‘y) ∈ A)}
⇒ ⊢ (A ∈ P → ∅ ⊂
B) |
| |
| Theorem | reclem2pr 3951 |
Lemma for Proposition 9-3.7 of [Gleason] p.
124.
|
| ⊢
B = {x∣∃y(x
<Q y ∧
¬ (*Q ‘y) ∈ A)}
⇒ ⊢ (A ∈ P → B ∈ P) |
| |
| Theorem | reclem3pr 3952 |
Lemma for Proposition 9-3.7(v) of [Gleason] p.
124.
|
| ⊢
B = {x∣∃y(x
<Q y ∧
¬ (*Q ‘y) ∈ A)}
⇒ ⊢ (A ∈ P →
1P ⊆ (A
·P B)) |
| |
| Theorem | reclem4pr 3953 |
Lemma for Proposition 9-3.7(v) of [Gleason] p.
124.
|
| ⊢
B = {x∣∃y(x
<Q y ∧
¬ (*Q ‘y) ∈ A)}
⇒ ⊢ (A ∈ P → (A ·P B) = 1P) |
| |
| Theorem | recexpr 3954 |
The reciprocal of a positive real exists. Part of Proposition
9-3.7(v) of [Gleason] p. 124.
|
| ⊢
(A ∈ P →
∃x(x ∈ P ∧ (A ·P x) = 1P)) |
| |
| Theorem | suplem1pr 3955 |
The union of a non-empty, bounded set of positive reals is a positive
real. Part of Proposition 9-3.3 of [Gleason] p. 122.
|
| ⊢
(((A ⊆ P ∧
¬ A = ∅) ∧ ∃x(x ∈
P ∧ ∀y(y ∈ P → (y ∈ A
→ y<P
x)))) → ∪A ∈
P) |
| |
| Theorem | suplem2pr 3956 |
The union of a set of positive reals (if a positive real) is its
supremum (least upper bound). Part of Proposition 9-3.3 of [Gleason]
p. 122.
|
| ⊢
(A ⊆ P →
((y ∈ A → ¬ ∪A<P y) ∧ (y<P ∪A →
∃z(z ∈ P ∧ (z ∈ A
∧ y<P
z))))) |
| |
| Theorem | suppr 3957 |
The union of a non-empty, bounded set of positive reals has a supremum.
Part of Proposition 9-3.3 of [Gleason]
p. 122.
|
| ⊢
(((A ⊆ P ∧
¬ A = ∅) ∧ ∃x(x ∈
P ∧ ∀y(y ∈ P → (y ∈ A
→ y<P
x)))) → ∃x(x ∈
P ∧ ∀y(y ∈ P → ((y ∈ A
→ ¬ x<P y) ∧ (y<P x → ∃z(z ∈
P ∧ (z ∈ A ∧ y<P z))))))) |
| |
| Definition | df-plpr 3958 |
Define pre-addition on signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.1
of [Gleason] p. 126.
|
| ⊢
+pR = {⟨⟨x, y⟩,
z⟩∣((x ∈ (P × P)
∧ y ∈ (P ×
P)) ∧ ∃w∃v∃u∃f((x =
⟨w, v⟩ ∧ y
= ⟨u, f⟩) ∧ z = ⟨(w
+P u), (v +P f)⟩))} |
| |
| Definition | df-mpr 3959 |
Define pre-multiplication on signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.1
of [Gleason] p. 126.
|
| ⊢
·pR = {⟨⟨x, y⟩,
z⟩∣((x ∈ (P × P)
∧ y ∈ (P ×
P)) ∧ ∃w∃v∃u∃f((x =
⟨w, v⟩ ∧ y
= ⟨u, f⟩) ∧ z = ⟨((w
·P u)
+P (v
·P f)),
((w ·P
f) +P (v ·P u))⟩))} |
| |
| Definition | df-enr 3960 |
Define equivalence relation for signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition
9-4.1 of [Gleason] p. 126.
|
| ⊢
~R = {⟨x,
y⟩∣((x ∈ (P × P)
∧ y ∈ (P ×
P)) ∧ ∃z∃w∃v∃u((x =
⟨z, w⟩ ∧ y
= ⟨v, u⟩) ∧ (z +P u) = (w
+P v)))} |
| |
| Definition | df-nr 3961 |
Define class of signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.2 of
[Gleason] p. 126.
|
| ⊢
R = ((P × P) /
~R ) |
| |
| Definition | df-plr 3962 |
Define addition on signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.3
of [Gleason] p. 126.
|
| ⊢
+R = {⟨⟨x, y⟩,
z⟩∣((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃f((x =
[⟨w, v⟩] ~R ∧ y = [⟨u,
f⟩] ~R )
∧ z = [(⟨w, v⟩
+pR ⟨u,
f⟩)] ~R
))} |
| |
| Definition | df-mr 3963 |
Define multiplication on signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.3
of [Gleason] p. 126.
|
| ⊢
·R = {⟨⟨x, y⟩,
z⟩∣((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃f((x =
[⟨w, v⟩] ~R ∧ y = [⟨u,
f⟩] ~R )
∧ z = [(⟨w, v⟩
·pR ⟨u, f⟩)]
~R ))} |
| |
| Definition | df-ltr 3964 |
Define ordering relation on signed reals. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.4 of
[Gleason] p. 127.
|
| ⊢
<R = {⟨x,
y⟩∣((x ∈ R ∧ y ∈ R) ∧ ∃z∃w∃v∃u((x =
[⟨z, w⟩] ~R ∧ y = [⟨v,
u⟩] ~R )
∧ (z +P
u)<P (w +P v)))} |
| |
| Definition | df-0r 3965 |
Define signed real constant 0. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.2 of
[Gleason] p. 126.
|
| ⊢
0R = [⟨1P,
1P⟩] ~R |
| |
| Definition | df-1r 3966 |
Define signed real constant 1. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction. From Proposition 9-4.2 of
[Gleason] p. 126.
|
| ⊢
1R = [⟨(1P
+P 1P),
1P⟩] ~R |
| |
| Definition | df-m1r 3967 |
Define signed real constant -1. This is a "temporary"
set used in the construction of complex numbers df-c 4034,
and is intended
to be used only by the construction.
|
| ⊢
-1R = [⟨1P,
(1P +P
1P)⟩] ~R |
| |
| Theorem | enrbreq 3968 |
Equivalence relation for signed reals in terms of positive reals.
|
| ⊢
(((A ∈ P ∧
B ∈ P) ∧ (C ∈ P ∧ D ∈ P)) → (⟨A, B⟩
~R ⟨C,
D⟩ ↔ (A +P D) = (B
+P C))) |
| |
| Theorem | dmenr 3969 |
Domain of equivalence relation for signed reals.
|
| ⊢
dom ~R = (P ×
P) |
| |
| Theorem | enrer 3970 |
The equivalence relation for signed reals is an equivalence
relation. Proposition 9-4.1 of [Gleason] p. 126.
|
| ⊢
Er ~R |
| |
| Theorem | enreceq 3971 |
Equivalence class equality of positive fractions in terms of positive
integers.
|
| ⊢
(((A ∈ P ∧
B ∈ P) ∧ (C ∈ P ∧ D ∈ P)) → ([⟨A, B⟩]
~R = [⟨C,
D⟩] ~R
↔ (A +P
D) = (B +P C))) |
| |
| Theorem | enrex 3972 |
The equivalence relation for signed reals exists.
|
| ⊢
~R ∈ V |
| |
| Theorem | srex 3973 |
The class of signed reals is a set.
|
| ⊢
R ∈ V |
| |
| Theorem | ltrelsr 3974 |
Signed real 'less than' is a relation on signed reals.
|
| ⊢
<R ⊆ (R ×
R) |
| |
| Theorem | addcmpblnr 3975 |
Lemma showing compatibility of addition.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V
& ⊢ G ∈ V
& ⊢ R ∈ V
& ⊢ S ∈ V
⇒ ⊢ ((((A ∈ P ∧ B ∈ P) ∧ (C ∈ P ∧ D ∈ P)) ∧ ((F ∈ P ∧ G ∈ P) ∧ (R ∈ P ∧ S ∈ P))) → (((A +P D) = (B
+P C) ∧
(F +P S) = (G
+P R)) →
⟨(A +P
F), (B
+P G)⟩
~R ⟨(C
+P R), (D +P S)⟩)) |
| |
| Theorem | mulcmpblnrlem 3976 |
Lemma used in lemma showing compatibility of multiplication.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V
& ⊢ G ∈ V
& ⊢ R ∈ V
& ⊢ S ∈ V
⇒ ⊢ (((A +P D) = (B
+P C) ∧
(F +P S) = (G
+P R)) →
((D ·P
F) +P (((A ·P F) +P (B ·P G)) +P ((C ·P S) +P (D ·P R)))) = ((D
·P F)
+P (((A
·P G)
+P (B
·P F))
+P ((C
·P R)
+P (D
·P S))))) |
| |
| Theorem | mulcmpblnr 3977 |
Lemma showing compatibility of multiplication.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V
& ⊢ G ∈ V
& ⊢ R ∈ V
& ⊢ S ∈ V
⇒ ⊢ ((((A ∈ P ∧ B ∈ P) ∧ (C ∈ P ∧ D ∈ P)) ∧ ((F ∈ P ∧ G ∈ P) ∧ (R ∈ P ∧ S ∈ P))) → (((A +P D) = (B
+P C) ∧
(F +P S) = (G
+P R)) →
⟨((A
·P F)
+P (B
·P G)),
((A ·P
G) +P (B ·P F))⟩ ~R
⟨((C
·P R)
+P (D
·P S)),
((C ·P
S) +P (D ·P R))⟩)) |
| |
| Theorem | addsrpr 3978 |
Addition of signed reals in terms of positive reals.
|
| ⊢
(((A ∈ P ∧
B ∈ P) ∧ (C ∈ P ∧ D ∈ P)) → ([⟨A, B⟩]
~R +R [⟨C, D⟩]
~R ) = [⟨(A
+P C), (B +P D)⟩] ~R ) |
| |
| Theorem | mulsrpr 3979 |
Multiplication of signed reals in terms of positive reals.
|
| ⊢
(((A ∈ P ∧
B ∈ P) ∧ (C ∈ P ∧ D ∈ P)) → ([⟨A, B⟩]
~R ·R [⟨C, D⟩]
~R ) = [⟨((A
·P C)
+P (B
·P D)),
((A ·P
D) +P (B ·P C))⟩] ~R ) |
| |
| Theorem | ltsrpr 3980 |
Ordering of signed reals in terms of positive reals.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ ([⟨A, B⟩]
~R <R [⟨C, D⟩]
~R ↔ (A
+P D)<P (B +P C)) |
| |
| Theorem | gt0srpr 3981 |
Greater then zero in terms of positive reals.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢
(0R <R
[⟨A, B⟩] ~R ↔
B<P A) |
| |
| Theorem | 0nsr 3982 |
The empty set is not a signed real.
|
| ⊢
¬ ∅ ∈ R |
| |
| Theorem | 0r 3983 |
The constant 0R is a signed real.
|
| ⊢
0R ∈ R |
| |
| Theorem | 1r 3984 |
The constant 1R is a signed real.
|
| ⊢
1R ∈ R |
| |
| Theorem | m1r 3985 |
The constant -1R is a signed real.
|
| ⊢
-1R ∈ R |
| |
| Theorem | addclsr 3986 |
Closure of addition on signed reals.
|
| ⊢
((A ∈ R ∧
B ∈ R) → (A +R B) ∈ R) |
| |
| Theorem | mulclsr 3987 |
Closure of multiplication on signed reals.
|
| ⊢
((A ∈ R ∧
B ∈ R) → (A ·R B) ∈ R) |
| |
| Theorem | dmaddsr 3988 |
Domain of addition on signed reals.
|
| ⊢
dom +R = (R ×
R) |
| |
| Theorem | dmmulsr 3989 |
Domain of multiplication on signed reals.
|
| ⊢
dom ·R = (R ×
R) |
| |
| Theorem | addcomsr 3990 |
Addition of signed reals is commutative.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A +R B) = (B
+R A) |
| |
| Theorem | addasssr 3991 |
Addition of signed reals is associative.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A +R B) +R C) = (A
+R (B
+R C)) |
| |
| Theorem | mulcomsr 3992 |
Multiplication of signed reals is commutative.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ·R B) = (B
·R A) |
| |
| Theorem | mulasssr 3993 |
Multiplication of signed reals is associative.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ·R B) ·R C) = (A
·R (B
·R C)) |
| |
| Theorem | distrsr 3994 |
Multiplication of signed reals is distributive.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ·R (B +R C)) = ((A
·R B)
+R (A
·R C)) |
| |
| Theorem | m1p1sr 3995 |
Minus one plus one is zero for signed reals.
|
| ⊢
(-1R +R
1R) = 0R |
| |
| Theorem | m1m1sr 3996 |
Minus one times minus one is plus one for signed reals.
|
| ⊢
(-1R ·R
-1R) = 1R |
| |
| Theorem | ltsosr 3997 |
Signed real 'less than' is a strict ordering.
|
| ⊢
<R Or R |
| |
| Theorem | 0lt1sr 3998 |
0 is less than 1 for signed reals.
|
| ⊢
0R <R
1R |
| |
| Theorem | 1ne0sr 3999 |
1 and 0 are distinct for signed reals.
|
| ⊢
¬ 1R = 0R |
| |
| Theorem | 0idsr 4000 |
The signed real number 0 is an identity element for addition of
signed reals.
|
| ⊢
(A ∈ R →
(A +R
0R) = A) |
Home
Hilbert Space Explorer
(4958-5787)