Statement List for Metamath Proof Explorer - 5001-5100 - Page 51 of 107
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | 0npi 5001 |
The empty set is not a positive integer.
|
| ⊢
¬ ∅ ∈ N |
| |
| Theorem | 1pi 5002 |
Ordinal 'one' is a positive integer.
|
| ⊢
1o ∈ N |
| |
| Theorem | addpiord 5003 |
Positive integer addition in terms of ordinal addition.
|
| ⊢
((A ∈ N ⋀
B ∈ N) → (A +N B) = (A
+o B)) |
| |
| Theorem | mulpiord 5004 |
Positive integer multiplication in terms of ordinal multiplication.
|
| ⊢
((A ∈ N ⋀
B ∈ N) → (A ·N B) = (A
·o B)) |
| |
| Theorem | mulidpi 5005 |
1 is an identity element for multiplication on positive integers.
|
| ⊢
(A ∈ N →
(A ·N
1o) = A) |
| |
| Theorem | ltpiord 5006 |
Positive integer 'less than' in terms of ordinal membership.
|
| ⊢
((A ∈ N ⋀
B ∈ N) → (A <N B ↔ A
∈ B)) |
| |
| Theorem | ltsopi 5007 |
Positive integer 'less than' is a strict ordering.
|
| ⊢
<N Or N |
| |
| Theorem | ltrelpi 5008 |
Positive integer 'less than' is a relation on positive integers.
|
| ⊢
<N ⊆ (N ×
N) |
| |
| Theorem | dmaddpi 5009 |
Domain of addition on positive integers.
|
| ⊢
dom +N = (N ×
N) |
| |
| Theorem | dmmulpi 5010 |
Domain of multiplication on positive integers.
|
| ⊢
dom ·N = (N ×
N) |
| |
| Theorem | addclpi 5011 |
Closure of addition of positive integers.
|
| ⊢
((A ∈ N ⋀
B ∈ N) → (A +N B) ∈ N) |
| |
| Theorem | mulclpi 5012 |
Closure of multiplication of positive integers.
|
| ⊢
((A ∈ N ⋀
B ∈ N) → (A ·N B) ∈ N) |
| |
| Theorem | addcompi 5013 |
Addition of positive integers is commutative.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A +N B) = (B
+N A) |
| |
| Theorem | addasspi 5014 |
Addition of positive integers is associative.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A +N B) +N C) = (A
+N (B
+N C)) |
| |
| Theorem | mulcompi 5015 |
Multiplication of positive integers is commutative.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ·N B) = (B
·N A) |
| |
| Theorem | mulasspi 5016 |
Multiplication of positive integers is associative.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ·N B) ·N C) = (A
·N (B
·N C)) |
| |
| Theorem | distrpi 5017 |
Multiplication of positive integers is distributive.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ·N (B +N C)) = ((A
·N B)
+N (A
·N C)) |
| |
| Theorem | mulcanpi 5018 |
Multiplication cancellation law for positive integers.
|
| ⊢
C ∈ V
⇒ ⊢ ((A ∈ N ⋀ B ∈ N) → ((A ·N B) = (A
·N C)
→ B = C)) |
| |
| Theorem | addnidpi 5019 |
There is no identity element for addition on positive integers.
|
| ⊢
B ∈ V
⇒ ⊢ (A ∈ N → ¬ (A +N B) = A) |
| |
| Theorem | ltexpi 5020 |
Ordering on positive integers in terms of existence of sum.
|
| ⊢
((A ∈ N ⋀
B ∈ N) → (A <N B ↔ ∃x(x ∈
N ⋀ (A
+N x) = B))) |
| |
| Theorem | ltapi 5021 |
Ordering property of addition for positive integers.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (C ∈ N → (A <N B ↔ (C
+N A)
<N (C
+N B))) |
| |
| Theorem | ltmpi 5022 |
Ordering property of multiplication for positive integers.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (C ∈ N → (A <N B ↔ (C
·N A)
<N (C
·N B))) |
| |
| Theorem | 1lt2pi 5023 |
One is less than two (one plus one).
|
| ⊢
1o <N
(1o +N
1o) |
| |
| Theorem | nlt1pi 5024 |
No positive integer is less than one.
|
| ⊢
¬ A <N
1o |
| |
| Theorem | indpi 5025 |
Principle of Finite Induction on positive integers.
|
| ⊢
(x = 1o →
(φ ↔ ψ))
& ⊢ (x = y →
(φ ↔ χ))
& ⊢ (x = (y
+N 1o) → (φ ↔ θ))
& ⊢ (x = A →
(φ ↔ τ))
& ⊢ ψ
& ⊢ (y ∈ N → (χ → θ))
⇒ ⊢ (A ∈ N → τ) |
| |
| Definition | df-plpq 5026 |
Define pre-addition on positive fractions. This is a "temporary" set
used in the construction of complex numbers df-c 5231,
and is intended to
be used only by the construction. This "pre-addition"
operation works
works directly with ordered pairs of integers. The actual positive
fraction addition +Q (df-plq 5030) works with the equivalence classes
of these ordered pairs determined by the equivalence relation
~Q
(df-enq 5028). (Analogous remarks apply to the other
"pre-" operations
in the complex number construction that follows.) From Proposition
9-2.3 of [Gleason] p. 117.
|
| ⊢
+pQ = {⟨⟨x, y⟩,
z⟩∣((x ∈ (N × N)
⋀ y ∈ (N ×
N)) ⋀ ∃w∃v∃u∃f((x =
⟨w, v⟩ ⋀ y = ⟨u,
f⟩) ⋀ z = ⟨((w
·N f)
+N (v
·N u)),
(v ·N
f)⟩))} |
| |
| Definition | df-mpq 5027 |
Define pre-multiplication on positive fractions. This is a
"temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-2.4 of
[Gleason] p. 119.
|
| ⊢
·pQ = {⟨⟨x, y⟩,
z⟩∣((x ∈ (N × N)
⋀ y ∈ (N ×
N)) ⋀ ∃w∃v∃u∃f((x =
⟨w, v⟩ ⋀ y = ⟨u,
f⟩) ⋀ z = ⟨(w
·N u),
(v ·N
f)⟩))} |
| |
| Definition | df-enq 5028 |
Define equivalence relation for positive fractions. This is a
"temporary" set used in the construction of complex numbers df-c 5231,
and is intended to be used only by the construction. From Proposition
9-2.1 of [Gleason] p. 117.
|
| ⊢
~Q = {⟨x,
y⟩∣((x ∈ (N × N)
⋀ y ∈ (N ×
N)) ⋀ ∃z∃w∃v∃u((x =
⟨z, w⟩ ⋀ y = ⟨v,
u⟩) ⋀ (z ·N u) = (w
·N v)))} |
| |
| Definition | df-nq 5029 |
Define class of positive fractions. This is a "temporary" set
used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-2.2 of
[Gleason] p. 117.
|
| ⊢
Q = ((N × N) /
~Q ) |
| |
| Definition | df-plq 5030 |
Define addition on positive fractions. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-2.3
of [Gleason] p. 117.
|
| ⊢
+Q = {⟨⟨x, y⟩,
z⟩∣((x ∈ Q ⋀ y ∈ Q) ⋀ ∃w∃v∃u∃f((x =
[⟨w, v⟩] ~Q ⋀
y = [⟨u, f⟩]
~Q ) ⋀ z =
[(⟨w, v⟩ +pQ ⟨u, f⟩)]
~Q ))} |
| |
| Definition | df-mq 5031 |
Define multiplication on positive fractions. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-2.4
of [Gleason] p. 119.
|
| ⊢
·Q = {⟨⟨x, y⟩,
z⟩∣((x ∈ Q ⋀ y ∈ Q) ⋀ ∃w∃v∃u∃f((x =
[⟨w, v⟩] ~Q ⋀
y = [⟨u, f⟩]
~Q ) ⋀ z =
[(⟨w, v⟩ ·pQ
⟨u, f⟩)] ~Q ))} |
| |
| Definition | df-rq 5032 |
Define reciprocal on positive fractions. It means the same thing as
one divided by the argument (although we don't define full division
since we will never need it). This is a "temporary" set used
in the
construction of complex numbers df-c 5231, and is intended to be used only
by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who
uses an asterisk to denote this unary operation.
|
| ⊢
*Q = {⟨x, y⟩∣(x ∈ Q ⋀ (x ·Q y) = 1Q)} |
| |
| Definition | df-ltq 5033 |
Define ordering relation on positive fractions. This is a
"temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. Similar to Definition 5 of
[Suppes] p. 162.
|
| ⊢
<Q = {⟨x,
y⟩∣((x ∈ Q ⋀ y ∈ Q) ⋀ ∃z∃w∃v∃u((x =
[⟨z, w⟩] ~Q ⋀
y = [⟨v, u⟩]
~Q ) ⋀ (z
·N u)
<N (w
·N v)))} |
| |
| Definition | df-1q 5034 |
Define positive fraction constant 1. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-2.2 of
[Gleason] p. 117.
|
| ⊢
1Q = [⟨1o,
1o⟩] ~Q |
| |
| Theorem | enqbreq 5035 |
Equivalence relation for positive fractions in terms of positive
integers.
|
| ⊢
(((A ∈ N ⋀
B ∈ N) ⋀
(C ∈ N ⋀ D ∈ N)) → (⟨A, B⟩
~Q ⟨C,
D⟩ ↔ (A ·N D) = (B
·N C))) |
| |
| Theorem | dmenq 5036 |
Domain of equivalence relation for positive fractions.
|
| ⊢
dom ~Q = (N ×
N) |
| |
| Theorem | enqer 5037 |
The equivalence relation for positive fractions is an equivalence
relation. Proposition 9-2.1 of [Gleason] p. 117.
|
| ⊢
Er ~Q |
| |
| Theorem | enqeceq 5038 |
Equivalence class equality of positive fractions in terms of positive
integers.
|
| ⊢
(((A ∈ N ⋀
B ∈ N) ⋀
(C ∈ N ⋀ D ∈ N)) → ([⟨A, B⟩]
~Q = [⟨C,
D⟩] ~Q
↔ (A
·N D) =
(B ·N
C))) |
| |
| Theorem | enqex 5039 |
The equivalence relation for positive fractions exists.
|
| ⊢
~Q ∈ V |
| |
| Theorem | nqex 5040 |
The class of positive fractions exists.
|
| ⊢
Q ∈ V |
| |
| Theorem | 0npq 5041 |
The empty set is not a positive fraction.
|
| ⊢
¬ ∅ ∈ Q |
| |
| Theorem | ltrelpq 5042 |
Positive fraction 'less than' is a relation on positive fractions.
|
| ⊢
<Q ⊆ (Q ×
Q) |
| |
| Theorem | addcmpblnq 5043 |
Lemma showing compatibility of addition.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V
& ⊢ G ∈ V
& ⊢ R ∈ V
& ⊢ S ∈ V
⇒ ⊢ ((((A ∈ N ⋀ B ∈ N) ⋀ (C ∈ N ⋀ D ∈ N)) ⋀ ((F ∈ N ⋀ G ∈ N) ⋀ (R ∈ N ⋀ S ∈ N))) → (((A ·N D) = (B
·N C)
⋀ (F
·N S) =
(G ·N
R)) → ⟨((A ·N G) +N (B ·N F)), (B
·N G)⟩ ~Q
⟨((C
·N S)
+N (D
·N R)),
(D ·N
S)⟩)) |
| |
| Theorem | mulcmpblnq 5044 |
Lemma showing compatibility of multiplication.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
& ⊢ F ∈ V
& ⊢ G ∈ V
& ⊢ R ∈ V
& ⊢ S ∈ V
⇒ ⊢ ((((A ∈ N ⋀ B ∈ N) ⋀ (C ∈ N ⋀ D ∈ N)) ⋀ ((F ∈ N ⋀ G ∈ N) ⋀ (R ∈ N ⋀ S ∈ N))) → (((A ·N D) = (B
·N C)
⋀ (F
·N S) =
(G ·N
R)) → ⟨(A ·N F), (B
·N G)⟩ ~Q
⟨(C
·N R),
(D ·N
S)⟩)) |
| |
| Theorem | addpipq 5045 |
Addition of positive fractions in terms of positive integers.
|
| ⊢
(((A ∈ N ⋀
B ∈ N) ⋀
(C ∈ N ⋀ D ∈ N)) → ([⟨A, B⟩]
~Q +Q [⟨C, D⟩]
~Q ) = [⟨((A
·N D)
+N (B
·N C)),
(B ·N
D)⟩] ~Q
) |
| |
| Theorem | mulpipq 5046 |
Multiplication of positive fractions in terms of positive integers.
|
| ⊢
(((A ∈ N ⋀
B ∈ N) ⋀
(C ∈ N ⋀ D ∈ N)) → ([⟨A, B⟩]
~Q ·Q [⟨C, D⟩]
~Q ) = [⟨(A
·N C),
(B ·N
D)⟩] ~Q
) |
| |
| Theorem | ordpipq 5047 |
Ordering of positive fractions in terms of positive integers.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ ([⟨A, B⟩]
~Q <Q [⟨C, D⟩]
~Q ↔ (A
·N D)
<N (B
·N C)) |
| |
| Theorem | 1q 5048 |
The positive fraction 'one'.
|
| ⊢
1Q ∈ Q |
| |
| Theorem | addclpq 5049 |
Closure of addition on positive fractions.
|
| ⊢
((A ∈ Q ⋀
B ∈ Q) → (A +Q B) ∈ Q) |
| |
| Theorem | dmaddpq 5050 |
Domain of addition on positive fractions.
|
| ⊢
dom +Q = (Q ×
Q) |
| |
| Theorem | mulclpq 5051 |
Closure of multiplication on positive fractions.
|
| ⊢
((A ∈ Q ⋀
B ∈ Q) → (A ·Q B) ∈ Q) |
| |
| Theorem | dmmulpq 5052 |
Domain of multiplication on positive fractions.
|
| ⊢
dom ·Q = (Q ×
Q) |
| |
| Theorem | addcompq 5053 |
Addition of positive fractions is commutative.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A +Q B) = (B
+Q A) |
| |
| Theorem | addasspq 5054 |
Addition of positive fractions is associative.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A +Q B) +Q C) = (A
+Q (B
+Q C)) |
| |
| Theorem | mulcompq 5055 |
Multiplication of positive fractions is commutative.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A ·Q B) = (B
·Q A) |
| |
| Theorem | mulasspq 5056 |
Multiplication of positive fractions is associative.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ ((A ·Q B) ·Q C) = (A
·Q (B
·Q C)) |
| |
| Theorem | distrpqlem 5057 |
Lemma for distributive law: cancellation of common factor.
|
| |
| Theorem | distrpq 5058 |
Multiplication of positive fractions is distributive.
|
| ⊢
B ∈ V
& ⊢ C ∈ V
⇒ ⊢ (A ·Q (B +Q C)) = ((A
·Q B)
+Q (A
·Q C)) |
| |
| Theorem | 1qec 5059 |
The equivalence class of ratio 1.
|
| ⊢
A ∈ V
⇒ ⊢ (A ∈ N →
1Q = [⟨A,
A⟩] ~Q
) |
| |
| Theorem | mulidpq 5060 |
Multiplication identity element for positive fractions.
|
| ⊢
(A ∈ Q →
(A ·Q
1Q) = A) |
| |
| Theorem | recmulpq 5061 |
Relationship between reciprocal and multiplication on positive
fractions.
|
| ⊢
B ∈ V
⇒ ⊢ (A ∈ Q →
((*Q ‘A) =
B ↔ (A ·Q B) = 1Q)) |
| |
| Theorem | recidpq 5062 |
A positive fraction times its reciprocal is 1.
|
| ⊢
(A ∈ Q →
(A ·Q
(*Q ‘A)) =
1Q) |
| |
| Theorem | recclpq 5063 |
Closure law for positive fraction reciprocal.
|
| ⊢
(A ∈ Q →
(*Q ‘A)
∈ Q) |
| |
| Theorem | recrecpq 5064 |
Reciprocal of reciprocal of positive fraction.
|
| ⊢
A ∈ V
⇒ ⊢ (A ∈ Q →
(*Q ‘(*Q
‘A)) = A) |
| |
| Theorem | dmrecpq 5065 |
Domain of reciprocal on positive fractions.
|
| ⊢
dom *Q = Q |
| |
| Theorem | ltsopq 5066 |
'Less than' is a strict ordering on positive fractions.
|
| ⊢
<Q Or Q |
| |
| Theorem | ltapq 5067 |
Ordering property of addition for positive fractions. Proposition
9-2.6(ii) of [Gleason] p. 120.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (C ∈ Q → (A <Q B ↔ (C
+Q A)
<Q (C
+Q B))) |
| |
| Theorem | ltmpq 5068 |
Ordering property of multiplication for positive fractions. Proposition
9-2.6(iii) of [Gleason] p. 120.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (C ∈ Q → (A <Q B ↔ (C
·Q A)
<Q (C
·Q B))) |
| |
| Theorem | 1lt2pq 5069 |
One is less than two (one plus one).
|
| ⊢
1Q <Q
(1Q +Q
1Q) |
| |
| Theorem | ltaddpq 5070 |
The sum of two fractions is greater than one of them.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ ((A ∈ Q ⋀ B ∈ Q) → A <Q (A +Q B)) |
| |
| Theorem | ltexpq 5071 |
Ordering on positive fractions in terms of existence of sum. Definition
in Proposition 9-2.6 of [Gleason] p.
119.
|
| ⊢
A ∈ V
⇒ ⊢ ((A ∈ Q ⋀ B ∈ Q) → (A <Q B ↔ ∃x(A
+Q x) = B)) |
| |
| Theorem | ltexpq2 5072 |
Ordering on positive fractions in terms of existence of sum. Definition
in Proposition 9-2.6 of [Gleason] p.
119.
|
| ⊢
A ∈ V
⇒ ⊢ ((A ∈ Q ⋀ B ∈ Q) → (A <Q B ↔ ∃x(x ∈
Q ⋀ (A
+Q x) = B))) |
| |
| Theorem | halfpq 5073 |
One-half of any positive fraction exists. Lemma for Proposition
9-2.6(i) of [Gleason] p. 120.
|
| ⊢
(A ∈ Q →
∃x(x +Q x) = A) |
| |
| Theorem | nsmallpq 5074 |
The is no smallest positive fraction.
|
| ⊢
(A ∈ Q →
∃x x <Q A) |
| |
| Theorem | ltbtwnpq 5075 |
There exists a number between any two positive fractions. Proposition
9-2.6(i) of [Gleason] p. 120.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A <Q B → ∃x(A
<Q x ⋀
x <Q B)) |
| |
| Theorem | ltrpq 5076 |
Ordering property of reciprocal for positive fractions. Proposition
9-2.6(iv) of [Gleason] p. 120.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ (A <Q B → (*Q
‘B) <Q
(*Q ‘A)) |
| |
| Definition | df-np 5077 |
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 5231,
and is intended to be used
only by the construction.)
|
| ⊢
P = {x∣((∅ ⊂ x ⋀ x
⊂ Q) ⋀ ∀y
∈ x (∀z(z
<Q y →
z ∈ x) ⋀ ∃z ∈ x
y <Q z))} |
| |
| Definition | df-1p 5078 |
Define the positive real constant 1. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. Definition of [Gleason] p. 122.
|
| ⊢
1P = {x∣x
<Q 1Q} |
| |
| Definition | df-plp 5079 |
Define addition on positive reals. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-3.5 of
[Gleason] p. 123.
|
| ⊢
+P = {⟨⟨x, y⟩,
z⟩∣((x ∈ P ⋀ y ∈ P) ⋀ z = {w∣∃v ∈ x
∃u ∈ y w = (v +Q u)})} |
| |
| Definition | df-mp 5080 |
Define multiplication on positive reals. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-3.7 of
[Gleason] p. 124.
|
| ⊢
·P = {⟨⟨x, y⟩,
z⟩∣((x ∈ P ⋀ y ∈ P) ⋀ z = {w∣∃v ∈ x
∃u ∈ y w = (v ·Q u)})} |
| |
| Definition | df-ltp 5081 |
Define ordering on positive reals. This is a "temporary"
set used in the construction of complex numbers df-c 5231,
and is intended
to be used only by the construction. From Proposition 9-3.2 of
[Gleason] p. 122.
|
| ⊢
<P = {⟨x, y⟩∣((x ∈ P ⋀ y ∈ P) ⋀ x ⊂ y)} |
| |
| Theorem | npex 5082 |
The class of positive reals is a set.
|
| ⊢
P ∈ V |
| |
| Theorem | elnp 5083 |
Membership in positive reals.
|
| ⊢
(A ∈ P ↔
((∅ ⊂ A ⋀ A ⊂ Q) ⋀ ∀x ∈ A
(∀y(y <Q x → y
∈ A) ⋀ ∃y ∈ A
x <Q y))) |
| |
| Theorem | prn0 5084 |
A positive real is not empty.
|
| ⊢
(A ∈ P →
A ≠ ∅) |
| |
| Theorem | prpssnq 5085 |
A positive real is a subset of the positive fractions.
|
| ⊢
(A ∈ P →
A ⊂ Q) |
| |
| Theorem | elprpq 5086 |
A positive real is a set of positive fractions.
|
| ⊢
((A ∈ P ⋀
B ∈ A) → B
∈ Q) |
| |
| Theorem | 0npr 5087 |
The empty set is not a positive real.
|
| ⊢
¬ ∅ ∈ P |
| |
| Theorem | prcdpq 5088 |
A positive real is closed downwards under the positive fractions.
Definition 9-3.1 (ii) of [Gleason] p.
121.
|
| ⊢
((A ∈ P ⋀
B ∈ A) → (C
<Q B →
C ∈ A)) |
| |
| Theorem | prub 5089 |
A positive fraction not in a positive real is an upper bound. Remark (1)
of [Gleason] p. 122.
|
| ⊢
(((A ∈ P ⋀
B ∈ A) ⋀ C
∈ Q) → (¬ C
∈ A → B <Q C)) |
| |
| Theorem | prnmax 5090 |
A positive real has no largest member. Definition 9-3.1(iii) of
[Gleason] p. 121.
|
| ⊢
((A ∈ P ⋀
B ∈ A) → ∃x(x ∈
A ⋀ B <Q x)) |
| |
| Theorem | prnmadd 5091 |
A positive real has no largest member. Addition version.
|
| ⊢
B ∈ V
⇒ ⊢ ((A ∈ P ⋀ B ∈ A)
→ ∃x(B +Q x) ∈ A) |
| |
| Theorem | ltrelpr 5092 |
Positive real 'less than' is a relation on positive reals.
|
| ⊢
<P ⊆ (P ×
P) |
| |
| Theorem | genpv 5093 |
Value of general operation (addition or multiplication) on positive
reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ⋀ v ∈ P) ⋀ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
⇒ ⊢ ((A ∈ P ⋀ B ∈ P) → (AFB) = {f∣∃g∃h((g ∈
A ⋀ h ∈ B)
⋀ f = (gGh))}) |
| |
| Theorem | genpelv 5094 |
Membership in value of general operation (addition or multiplication)
on positive reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ⋀ v ∈ P) ⋀ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
& ⊢ C ∈ V
⇒ ⊢ ((A ∈ P ⋀ B ∈ P) → (C ∈ (AFB) ↔ ∃f∃g((f ∈
A ⋀ g ∈ B)
⋀ C = (fGg)))) |
| |
| Theorem | genpprecl 5095 |
Pre-closure law for general operation on positive reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ⋀ v ∈ P) ⋀ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
⇒ ⊢ ((A ∈ P ⋀ B ∈ P) → ((C ∈ A
⋀ D ∈ B) → (CGD) ∈ (AFB))) |
| |
| Theorem | genpdm 5096 |
Domain of general operation on positive reals.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ⋀ v ∈ P) ⋀ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
⇒ ⊢ dom F = (P ×
P) |
| |
| Theorem | genpn0 5097 |
The result of an operation on positive reals is not empty.
|
| ⊢
F = {⟨⟨w, v⟩,
u⟩∣((w ∈ P ⋀ v ∈ P) ⋀ u = {x∣∃y ∈ w
∃z ∈ v x = (yGz)})}
⇒ ⊢ ((A ∈ P ⋀ B ∈ P) → ∅ ⊂
(AFB)) |
| |
| Theorem | genpss 5098 |
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 5099 |
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 5100 |
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)))) |
Home
Hilbert Space Explorer
(8761-10688)