Theorem List for Intuitionistic Logic Explorer - 6401-6500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | cltr 6401 |
Signed real ordering relation.
|
class
<R |
|
Definition | df-ni 6402 |
Define the class of positive integers. This is a "temporary" set
used in
the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 15-Aug-1995.)
|
⊢ N = (ω ∖
{∅}) |
|
Definition | df-pli 6403 |
Define addition on positive integers. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 26-Aug-1995.)
|
⊢ +N = (
+𝑜 ↾ (N ×
N)) |
|
Definition | df-mi 6404 |
Define multiplication on positive integers. This is a "temporary"
set
used in the construction of complex numbers and is intended to be used
only by the construction. (Contributed by NM, 26-Aug-1995.)
|
⊢ ·N = (
·𝑜 ↾ (N ×
N)) |
|
Definition | df-lti 6405 |
Define 'less than' on positive integers. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only by
the construction. (Contributed by NM, 6-Feb-1996.)
|
⊢ <N = ( E ∩
(N × N)) |
|
Theorem | elni 6406 |
Membership in the class of positive integers. (Contributed by NM,
15-Aug-1995.)
|
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠
∅)) |
|
Theorem | pinn 6407 |
A positive integer is a natural number. (Contributed by NM,
15-Aug-1995.)
|
⊢ (𝐴 ∈ N → 𝐴 ∈
ω) |
|
Theorem | pion 6408 |
A positive integer is an ordinal number. (Contributed by NM,
23-Mar-1996.)
|
⊢ (𝐴 ∈ N → 𝐴 ∈ On) |
|
Theorem | piord 6409 |
A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|
⊢ (𝐴 ∈ N → Ord 𝐴) |
|
Theorem | niex 6410 |
The class of positive integers is a set. (Contributed by NM,
15-Aug-1995.)
|
⊢ N ∈ V |
|
Theorem | 0npi 6411 |
The empty set is not a positive integer. (Contributed by NM,
26-Aug-1995.)
|
⊢ ¬ ∅ ∈
N |
|
Theorem | elni2 6412 |
Membership in the class of positive integers. (Contributed by NM,
27-Nov-1995.)
|
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅
∈ 𝐴)) |
|
Theorem | 1pi 6413 |
Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|
⊢ 1𝑜 ∈
N |
|
Theorem | addpiord 6414 |
Positive integer addition in terms of ordinal addition. (Contributed by
NM, 27-Aug-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐵) = (𝐴 +𝑜 𝐵)) |
|
Theorem | mulpiord 6415 |
Positive integer multiplication in terms of ordinal multiplication.
(Contributed by NM, 27-Aug-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐵) = (𝐴 ·𝑜 𝐵)) |
|
Theorem | mulidpi 6416 |
1 is an identity element for multiplication on positive integers.
(Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro,
17-Nov-2014.)
|
⊢ (𝐴 ∈ N → (𝐴
·N 1𝑜) = 𝐴) |
|
Theorem | ltpiord 6417 |
Positive integer 'less than' in terms of ordinal membership. (Contributed
by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<N 𝐵 ↔ 𝐴 ∈ 𝐵)) |
|
Theorem | ltsopi 6418 |
Positive integer 'less than' is a strict ordering. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
|
⊢ <N Or
N |
|
Theorem | pitric 6419 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<N 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <N 𝐴))) |
|
Theorem | pitri3or 6420 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<N 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <N 𝐴)) |
|
Theorem | ltdcpi 6421 |
Less-than for positive integers is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
DECID 𝐴
<N 𝐵) |
|
Theorem | ltrelpi 6422 |
Positive integer 'less than' is a relation on positive integers.
(Contributed by NM, 8-Feb-1996.)
|
⊢ <N ⊆
(N × N) |
|
Theorem | dmaddpi 6423 |
Domain of addition on positive integers. (Contributed by NM,
26-Aug-1995.)
|
⊢ dom +N =
(N × N) |
|
Theorem | dmmulpi 6424 |
Domain of multiplication on positive integers. (Contributed by NM,
26-Aug-1995.)
|
⊢ dom ·N =
(N × N) |
|
Theorem | addclpi 6425 |
Closure of addition of positive integers. (Contributed by NM,
18-Oct-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐵) ∈ N) |
|
Theorem | mulclpi 6426 |
Closure of multiplication of positive integers. (Contributed by NM,
18-Oct-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐵) ∈ N) |
|
Theorem | addcompig 6427 |
Addition of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐵) = (𝐵 +N 𝐴)) |
|
Theorem | addasspig 6428 |
Addition of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
+N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N
𝐶))) |
|
Theorem | mulcompig 6429 |
Multiplication of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐵) = (𝐵 ·N 𝐴)) |
|
Theorem | mulasspig 6430 |
Multiplication of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵
·N 𝐶))) |
|
Theorem | distrpig 6431 |
Multiplication of positive integers is distributive. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶))) |
|
Theorem | addcanpig 6432 |
Addition cancellation law for positive integers. (Contributed by Jim
Kingdon, 27-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | mulcanpig 6433 |
Multiplication cancellation law for positive integers. (Contributed by
Jim Kingdon, 29-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addnidpig 6434 |
There is no identity element for addition on positive integers.
(Contributed by NM, 28-Nov-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
¬ (𝐴
+N 𝐵) = 𝐴) |
|
Theorem | ltexpi 6435* |
Ordering on positive integers in terms of existence of sum.
(Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro,
14-Jun-2013.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<N 𝐵 ↔ ∃𝑥 ∈ N (𝐴 +N 𝑥) = 𝐵)) |
|
Theorem | ltapig 6436 |
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
<N 𝐵 ↔ (𝐶 +N 𝐴)
<N (𝐶 +N 𝐵))) |
|
Theorem | ltmpig 6437 |
Ordering property of multiplication for positive integers. (Contributed
by Jim Kingdon, 31-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
<N 𝐵 ↔ (𝐶 ·N 𝐴)
<N (𝐶 ·N 𝐵))) |
|
Theorem | 1lt2pi 6438 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|
⊢ 1𝑜
<N (1𝑜
+N 1𝑜) |
|
Theorem | nlt1pig 6439 |
No positive integer is less than one. (Contributed by Jim Kingdon,
31-Aug-2019.)
|
⊢ (𝐴 ∈ N → ¬ 𝐴 <N
1𝑜) |
|
Theorem | indpi 6440* |
Principle of Finite Induction on positive integers. (Contributed by NM,
23-Mar-1996.)
|
⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +N
1𝑜) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ N →
(𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ N → 𝜏) |
|
Theorem | nnppipi 6441 |
A natural number plus a positive integer is a positive integer.
(Contributed by Jim Kingdon, 10-Nov-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) → (𝐴 +𝑜 𝐵) ∈
N) |
|
Definition | df-plpq 6442* |
Define pre-addition on positive fractions. This is a "temporary" set
used in the construction of complex numbers, and is intended to be used
only by the construction. This "pre-addition" operation works
directly
with ordered pairs of integers. The actual positive fraction addition
+Q (df-plqqs 6447) works with the equivalence classes of these
ordered pairs determined by the equivalence relation ~Q
(df-enq 6445). (Analogous remarks apply to the other
"pre-" operations
in the complex number construction that follows.) From Proposition
9-2.3 of [Gleason] p. 117. (Contributed
by NM, 28-Aug-1995.)
|
⊢ +pQ = (𝑥 ∈ (N
× N), 𝑦 ∈ (N ×
N) ↦ 〈(((1st ‘𝑥) ·N
(2nd ‘𝑦))
+N ((1st ‘𝑦) ·N
(2nd ‘𝑥))), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |
|
Definition | df-mpq 6443* |
Define pre-multiplication on positive fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. From Proposition 9-2.4 of [Gleason]
p. 119. (Contributed by NM, 28-Aug-1995.)
|
⊢ ·pQ =
(𝑥 ∈ (N
× N), 𝑦 ∈ (N ×
N) ↦ 〈((1st ‘𝑥) ·N
(1st ‘𝑦)), ((2nd ‘𝑥)
·N (2nd ‘𝑦))〉) |
|
Definition | df-ltpq 6444* |
Define pre-ordering relation on positive fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. Similar to Definition 5
of [Suppes] p. 162. (Contributed by NM,
28-Aug-1995.)
|
⊢ <pQ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N
× N) ∧ 𝑦 ∈ (N ×
N)) ∧ ((1st ‘𝑥) ·N
(2nd ‘𝑦))
<N ((1st ‘𝑦) ·N
(2nd ‘𝑥)))} |
|
Definition | df-enq 6445* |
Define equivalence relation for positive fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. From Proposition 9-2.1 of
[Gleason] p. 117. (Contributed by NM,
27-Aug-1995.)
|
⊢ ~Q = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} |
|
Definition | df-nqqs 6446 |
Define class of positive fractions. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. From Proposition 9-2.2 of [Gleason] p. 117.
(Contributed by NM, 16-Aug-1995.)
|
⊢ Q = ((N ×
N) / ~Q ) |
|
Definition | df-plqqs 6447* |
Define addition on positive fractions. This is a "temporary" set
used
in the construction of complex numbers, and is intended to be used only
by the construction. From Proposition 9-2.3 of [Gleason] p. 117.
(Contributed by NM, 24-Aug-1995.)
|
⊢ +Q =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 +pQ
〈𝑢, 𝑓〉)]
~Q ))} |
|
Definition | df-mqqs 6448* |
Define multiplication on positive fractions. This is a "temporary"
set
used in the construction of complex numbers, and is intended to be used
only by the construction. From Proposition 9-2.4 of [Gleason] p. 119.
(Contributed by NM, 24-Aug-1995.)
|
⊢ ·Q =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧
∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [〈𝑤, 𝑣〉] ~Q ∧
𝑦 = [〈𝑢, 𝑓〉] ~Q ) ∧
𝑧 = [(〈𝑤, 𝑣〉 ·pQ
〈𝑢, 𝑓〉)]
~Q ))} |
|
Definition | df-1nqqs 6449 |
Define positive fraction constant 1. This is a "temporary" set used
in
the construction of complex numbers, and is intended to be used only by
the construction. From Proposition 9-2.2 of [Gleason] p. 117.
(Contributed by NM, 29-Oct-1995.)
|
⊢ 1Q =
[〈1𝑜, 1𝑜〉]
~Q |
|
Definition | df-rq 6450* |
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, 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. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
⊢ *Q = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧
(𝑥
·Q 𝑦) =
1Q)} |
|
Definition | df-ltnqqs 6451* |
Define ordering relation on positive fractions. This is a
"temporary"
set used in the construction of complex numbers, and is intended to be
used only by the construction. Similar to Definition 5 of [Suppes]
p. 162. (Contributed by NM, 13-Feb-1996.)
|
⊢ <Q =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~Q ∧
𝑦 = [〈𝑣, 𝑢〉] ~Q ) ∧
(𝑧
·N 𝑢) <N (𝑤
·N 𝑣)))} |
|
Theorem | dfplpq2 6452* |
Alternative definition of pre-addition on positive fractions.
(Contributed by Jim Kingdon, 12-Sep-2019.)
|
⊢ +pQ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·N 𝑓) +N
(𝑣
·N 𝑢)), (𝑣 ·N 𝑓)〉))} |
|
Theorem | dfmpq2 6453* |
Alternative definition of pre-multiplication on positive fractions.
(Contributed by Jim Kingdon, 13-Sep-2019.)
|
⊢ ·pQ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 ·N 𝑢), (𝑣 ·N 𝑓)〉))} |
|
Theorem | enqbreq 6454 |
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by NM, 27-Aug-1995.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → (〈𝐴, 𝐵〉 ~Q
〈𝐶, 𝐷〉 ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶))) |
|
Theorem | enqbreq2 6455 |
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by Mario Carneiro, 8-May-2013.)
|
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ ((1st
‘𝐴)
·N (2nd ‘𝐵)) = ((1st ‘𝐵)
·N (2nd ‘𝐴)))) |
|
Theorem | enqer 6456 |
The equivalence relation for positive fractions is an equivalence
relation. Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM,
27-Aug-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|
⊢ ~Q Er
(N × N) |
|
Theorem | enqeceq 6457 |
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29-Nov-1995.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([〈𝐴, 𝐵〉] ~Q =
[〈𝐶, 𝐷〉]
~Q ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶))) |
|
Theorem | enqex 6458 |
The equivalence relation for positive fractions exists. (Contributed by
NM, 3-Sep-1995.)
|
⊢ ~Q ∈
V |
|
Theorem | enqdc 6459 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → DECID 〈𝐴, 𝐵〉 ~Q
〈𝐶, 𝐷〉) |
|
Theorem | enqdc1 6460 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
𝐶 ∈ (N
× N)) → DECID 〈𝐴, 𝐵〉 ~Q 𝐶) |
|
Theorem | nqex 6461 |
The class of positive fractions exists. (Contributed by NM,
16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
⊢ Q ∈ V |
|
Theorem | 0nnq 6462 |
The empty set is not a positive fraction. (Contributed by NM,
24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
⊢ ¬ ∅ ∈
Q |
|
Theorem | ltrelnq 6463 |
Positive fraction 'less than' is a relation on positive fractions.
(Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro,
27-Apr-2013.)
|
⊢ <Q ⊆
(Q × Q) |
|
Theorem | 1nq 6464 |
The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|
⊢ 1Q ∈
Q |
|
Theorem | addcmpblnq 6465 |
Lemma showing compatibility of addition. (Contributed by NM,
27-Aug-1995.)
|
⊢ ((((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → 〈((𝐴
·N 𝐺) +N (𝐵
·N 𝐹)), (𝐵 ·N 𝐺)〉
~Q 〈((𝐶 ·N 𝑆) +N
(𝐷
·N 𝑅)), (𝐷 ·N 𝑆)〉)) |
|
Theorem | mulcmpblnq 6466 |
Lemma showing compatibility of multiplication. (Contributed by NM,
27-Aug-1995.)
|
⊢ ((((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧
(𝑅 ∈ N
∧ 𝑆 ∈
N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → 〈(𝐴
·N 𝐹), (𝐵 ·N 𝐺)〉
~Q 〈(𝐶 ·N 𝑅), (𝐷 ·N 𝑆)〉)) |
|
Theorem | addpipqqslem 6467 |
Lemma for addpipqqs 6468. (Contributed by Jim Kingdon, 11-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → 〈((𝐴 ·N 𝐷) +N
(𝐵
·N 𝐶)), (𝐵 ·N 𝐷)〉 ∈ (N
× N)) |
|
Theorem | addpipqqs 6468 |
Addition of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([〈𝐴, 𝐵〉] ~Q
+Q [〈𝐶, 𝐷〉] ~Q ) =
[〈((𝐴
·N 𝐷) +N (𝐵
·N 𝐶)), (𝐵 ·N 𝐷)〉]
~Q ) |
|
Theorem | mulpipq2 6469 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8-May-2013.)
|
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·pQ 𝐵) = 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) |
|
Theorem | mulpipq 6470 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro,
8-May-2013.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → (〈𝐴, 𝐵〉 ·pQ
〈𝐶, 𝐷〉) = 〈(𝐴 ·N 𝐶), (𝐵 ·N 𝐷)〉) |
|
Theorem | mulpipqqs 6471 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([〈𝐴, 𝐵〉] ~Q
·Q [〈𝐶, 𝐷〉] ~Q ) =
[〈(𝐴
·N 𝐶), (𝐵 ·N 𝐷)〉]
~Q ) |
|
Theorem | ordpipqqs 6472 |
Ordering of positive fractions in terms of positive integers.
(Contributed by Jim Kingdon, 14-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → ([〈𝐴, 𝐵〉] ~Q
<Q [〈𝐶, 𝐷〉] ~Q ↔
(𝐴
·N 𝐷) <N (𝐵
·N 𝐶))) |
|
Theorem | addclnq 6473 |
Closure of addition on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
+Q 𝐵) ∈ Q) |
|
Theorem | mulclnq 6474 |
Closure of multiplication on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
·Q 𝐵) ∈ Q) |
|
Theorem | dmaddpqlem 6475* |
Decomposition of a positive fraction into numerator and denominator.
Lemma for dmaddpq 6477. (Contributed by Jim Kingdon, 15-Sep-2019.)
|
⊢ (𝑥 ∈ Q → ∃𝑤∃𝑣 𝑥 = [〈𝑤, 𝑣〉] ~Q
) |
|
Theorem | nqpi 6476* |
Decomposition of a positive fraction into numerator and denominator.
Similar to dmaddpqlem 6475 but also shows that the numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
⊢ (𝐴 ∈ Q → ∃𝑤∃𝑣((𝑤 ∈ N ∧ 𝑣 ∈ N) ∧
𝐴 = [〈𝑤, 𝑣〉] ~Q
)) |
|
Theorem | dmaddpq 6477 |
Domain of addition on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom +Q =
(Q × Q) |
|
Theorem | dmmulpq 6478 |
Domain of multiplication on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom ·Q =
(Q × Q) |
|
Theorem | addcomnqg 6479 |
Addition of positive fractions is commutative. (Contributed by Jim
Kingdon, 15-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
+Q 𝐵) = (𝐵 +Q 𝐴)) |
|
Theorem | addassnqg 6480 |
Addition of positive fractions is associative. (Contributed by Jim
Kingdon, 16-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ((𝐴
+Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q
𝐶))) |
|
Theorem | mulcomnqg 6481 |
Multiplication of positive fractions is commutative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
·Q 𝐵) = (𝐵 ·Q 𝐴)) |
|
Theorem | mulassnqg 6482 |
Multiplication of positive fractions is associative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ((𝐴
·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵
·Q 𝐶))) |
|
Theorem | mulcanenq 6483 |
Lemma for distributive law: cancellation of common factor. (Contributed
by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ 〈(𝐴
·N 𝐵), (𝐴 ·N 𝐶)〉
~Q 〈𝐵, 𝐶〉) |
|
Theorem | mulcanenqec 6484 |
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ [〈(𝐴
·N 𝐵), (𝐴 ·N 𝐶)〉]
~Q = [〈𝐵, 𝐶〉] ~Q
) |
|
Theorem | distrnqg 6485 |
Multiplication of positive fractions is distributive. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q
(𝐴
·Q 𝐶))) |
|
Theorem | 1qec 6486 |
The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|
⊢ (𝐴 ∈ N →
1Q = [〈𝐴, 𝐴〉] ~Q
) |
|
Theorem | mulidnq 6487 |
Multiplication identity element for positive fractions. (Contributed by
NM, 3-Mar-1996.)
|
⊢ (𝐴 ∈ Q → (𝐴
·Q 1Q) = 𝐴) |
|
Theorem | recexnq 6488* |
Existence of positive fraction reciprocal. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
⊢ (𝐴 ∈ Q → ∃𝑦(𝑦 ∈ Q ∧ (𝐴
·Q 𝑦) =
1Q)) |
|
Theorem | recmulnqg 6489 |
Relationship between reciprocal and multiplication on positive
fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) =
1Q)) |
|
Theorem | recclnq 6490 |
Closure law for positive fraction reciprocal. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
⊢ (𝐴 ∈ Q →
(*Q‘𝐴) ∈ Q) |
|
Theorem | recidnq 6491 |
A positive fraction times its reciprocal is 1. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
⊢ (𝐴 ∈ Q → (𝐴
·Q (*Q‘𝐴)) =
1Q) |
|
Theorem | recrecnq 6492 |
Reciprocal of reciprocal of positive fraction. (Contributed by NM,
26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
|
⊢ (𝐴 ∈ Q →
(*Q‘(*Q‘𝐴)) = 𝐴) |
|
Theorem | rec1nq 6493 |
Reciprocal of positive fraction one. (Contributed by Jim Kingdon,
29-Dec-2019.)
|
⊢
(*Q‘1Q) =
1Q |
|
Theorem | nqtri3or 6494 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<Q 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴)) |
|
Theorem | ltdcnq 6495 |
Less-than for positive fractions is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
DECID 𝐴
<Q 𝐵) |
|
Theorem | ltsonq 6496 |
'Less than' is a strict ordering on positive fractions. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
|
⊢ <Q Or
Q |
|
Theorem | nqtric 6497 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<Q 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴))) |
|
Theorem | ltanqg 6498 |
Ordering property of addition for positive fractions. Proposition
9-2.6(ii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ (𝐶 +Q 𝐴)
<Q (𝐶 +Q 𝐵))) |
|
Theorem | ltmnqg 6499 |
Ordering property of multiplication for positive fractions. Proposition
9-2.6(iii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
<Q 𝐵 ↔ (𝐶 ·Q 𝐴)
<Q (𝐶 ·Q 𝐵))) |
|
Theorem | ltanqi 6500 |
Ordering property of addition for positive fractions. One direction of
ltanqg 6498. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 +Q
𝐴)
<Q (𝐶 +Q 𝐵)) |