Theorem List for Intuitionistic Logic Explorer - 6501-6600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | piord 6501 |
A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|
⊢ (𝐴 ∈ N → Ord 𝐴) |
|
Theorem | niex 6502 |
The class of positive integers is a set. (Contributed by NM,
15-Aug-1995.)
|
⊢ N ∈ V |
|
Theorem | 0npi 6503 |
The empty set is not a positive integer. (Contributed by NM,
26-Aug-1995.)
|
⊢ ¬ ∅ ∈
N |
|
Theorem | elni2 6504 |
Membership in the class of positive integers. (Contributed by NM,
27-Nov-1995.)
|
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅
∈ 𝐴)) |
|
Theorem | 1pi 6505 |
Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|
⊢ 1𝑜 ∈
N |
|
Theorem | addpiord 6506 |
Positive integer addition in terms of ordinal addition. (Contributed by
NM, 27-Aug-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐵) = (𝐴 +𝑜 𝐵)) |
|
Theorem | mulpiord 6507 |
Positive integer multiplication in terms of ordinal multiplication.
(Contributed by NM, 27-Aug-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐵) = (𝐴 ·𝑜 𝐵)) |
|
Theorem | mulidpi 6508 |
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 6509 |
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 6510 |
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 6511 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<N 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <N 𝐴))) |
|
Theorem | pitri3or 6512 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
<N 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <N 𝐴)) |
|
Theorem | ltdcpi 6513 |
Less-than for positive integers is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
DECID 𝐴
<N 𝐵) |
|
Theorem | ltrelpi 6514 |
Positive integer 'less than' is a relation on positive integers.
(Contributed by NM, 8-Feb-1996.)
|
⊢ <N ⊆
(N × N) |
|
Theorem | dmaddpi 6515 |
Domain of addition on positive integers. (Contributed by NM,
26-Aug-1995.)
|
⊢ dom +N =
(N × N) |
|
Theorem | dmmulpi 6516 |
Domain of multiplication on positive integers. (Contributed by NM,
26-Aug-1995.)
|
⊢ dom ·N =
(N × N) |
|
Theorem | addclpi 6517 |
Closure of addition of positive integers. (Contributed by NM,
18-Oct-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐵) ∈ N) |
|
Theorem | mulclpi 6518 |
Closure of multiplication of positive integers. (Contributed by NM,
18-Oct-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐵) ∈ N) |
|
Theorem | addcompig 6519 |
Addition of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
+N 𝐵) = (𝐵 +N 𝐴)) |
|
Theorem | addasspig 6520 |
Addition of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
+N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N
𝐶))) |
|
Theorem | mulcompig 6521 |
Multiplication of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
(𝐴
·N 𝐵) = (𝐵 ·N 𝐴)) |
|
Theorem | mulasspig 6522 |
Multiplication of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵
·N 𝐶))) |
|
Theorem | distrpig 6523 |
Multiplication of positive integers is distributive. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶))) |
|
Theorem | addcanpig 6524 |
Addition cancellation law for positive integers. (Contributed by Jim
Kingdon, 27-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
+N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | mulcanpig 6525 |
Multiplication cancellation law for positive integers. (Contributed by
Jim Kingdon, 29-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ ((𝐴
·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addnidpig 6526 |
There is no identity element for addition on positive integers.
(Contributed by NM, 28-Nov-1995.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) →
¬ (𝐴
+N 𝐵) = 𝐴) |
|
Theorem | ltexpi 6527* |
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 6528 |
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
<N 𝐵 ↔ (𝐶 +N 𝐴)
<N (𝐶 +N 𝐵))) |
|
Theorem | ltmpig 6529 |
Ordering property of multiplication for positive integers. (Contributed
by Jim Kingdon, 31-Aug-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
<N 𝐵 ↔ (𝐶 ·N 𝐴)
<N (𝐶 ·N 𝐵))) |
|
Theorem | 1lt2pi 6530 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|
⊢ 1𝑜
<N (1𝑜
+N 1𝑜) |
|
Theorem | nlt1pig 6531 |
No positive integer is less than one. (Contributed by Jim Kingdon,
31-Aug-2019.)
|
⊢ (𝐴 ∈ N → ¬ 𝐴 <N
1𝑜) |
|
Theorem | indpi 6532* |
Principle of Finite Induction on positive integers. (Contributed by NM,
23-Mar-1996.)
|
⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +N
1𝑜) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ N →
(𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ N → 𝜏) |
|
Theorem | nnppipi 6533 |
A natural number plus a positive integer is a positive integer.
(Contributed by Jim Kingdon, 10-Nov-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) → (𝐴 +𝑜 𝐵) ∈
N) |
|
Definition | df-plpq 6534* |
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 6539) works with the equivalence classes of these
ordered pairs determined by the equivalence relation ~Q
(df-enq 6537). (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 6535* |
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 6536* |
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 6537* |
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 6538 |
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 6539* |
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 6540* |
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 6541 |
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 6542* |
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 6543* |
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 6544* |
Alternate 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 6545* |
Alternate definition of pre-multiplication on positive fractions.
(Contributed by Jim Kingdon, 13-Sep-2019.)
|
⊢ ·pQ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 ·N 𝑢), (𝑣 ·N 𝑓)〉))} |
|
Theorem | enqbreq 6546 |
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 6547 |
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 6548 |
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 6549 |
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 6550 |
The equivalence relation for positive fractions exists. (Contributed by
NM, 3-Sep-1995.)
|
⊢ ~Q ∈
V |
|
Theorem | enqdc 6551 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → DECID 〈𝐴, 𝐵〉 ~Q
〈𝐶, 𝐷〉) |
|
Theorem | enqdc1 6552 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
𝐶 ∈ (N
× N)) → DECID 〈𝐴, 𝐵〉 ~Q 𝐶) |
|
Theorem | nqex 6553 |
The class of positive fractions exists. (Contributed by NM,
16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
⊢ Q ∈ V |
|
Theorem | 0nnq 6554 |
The empty set is not a positive fraction. (Contributed by NM,
24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
⊢ ¬ ∅ ∈
Q |
|
Theorem | ltrelnq 6555 |
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 6556 |
The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|
⊢ 1Q ∈
Q |
|
Theorem | addcmpblnq 6557 |
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 6558 |
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 6559 |
Lemma for addpipqqs 6560. (Contributed by Jim Kingdon, 11-Sep-2019.)
|
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧
(𝐶 ∈ N
∧ 𝐷 ∈
N)) → 〈((𝐴 ·N 𝐷) +N
(𝐵
·N 𝐶)), (𝐵 ·N 𝐷)〉 ∈ (N
× N)) |
|
Theorem | addpipqqs 6560 |
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 6561 |
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 6562 |
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 6563 |
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 6564 |
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 6565 |
Closure of addition on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
+Q 𝐵) ∈ Q) |
|
Theorem | mulclnq 6566 |
Closure of multiplication on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
·Q 𝐵) ∈ Q) |
|
Theorem | dmaddpqlem 6567* |
Decomposition of a positive fraction into numerator and denominator.
Lemma for dmaddpq 6569. (Contributed by Jim Kingdon, 15-Sep-2019.)
|
⊢ (𝑥 ∈ Q → ∃𝑤∃𝑣 𝑥 = [〈𝑤, 𝑣〉] ~Q
) |
|
Theorem | nqpi 6568* |
Decomposition of a positive fraction into numerator and denominator.
Similar to dmaddpqlem 6567 but also shows that the numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
⊢ (𝐴 ∈ Q → ∃𝑤∃𝑣((𝑤 ∈ N ∧ 𝑣 ∈ N) ∧
𝐴 = [〈𝑤, 𝑣〉] ~Q
)) |
|
Theorem | dmaddpq 6569 |
Domain of addition on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom +Q =
(Q × Q) |
|
Theorem | dmmulpq 6570 |
Domain of multiplication on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
⊢ dom ·Q =
(Q × Q) |
|
Theorem | addcomnqg 6571 |
Addition of positive fractions is commutative. (Contributed by Jim
Kingdon, 15-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
+Q 𝐵) = (𝐵 +Q 𝐴)) |
|
Theorem | addassnqg 6572 |
Addition of positive fractions is associative. (Contributed by Jim
Kingdon, 16-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ((𝐴
+Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q
𝐶))) |
|
Theorem | mulcomnqg 6573 |
Multiplication of positive fractions is commutative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
·Q 𝐵) = (𝐵 ·Q 𝐴)) |
|
Theorem | mulassnqg 6574 |
Multiplication of positive fractions is associative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ ((𝐴
·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵
·Q 𝐶))) |
|
Theorem | mulcanenq 6575 |
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 6576 |
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧
𝐶 ∈ N)
→ [〈(𝐴
·N 𝐵), (𝐴 ·N 𝐶)〉]
~Q = [〈𝐵, 𝐶〉] ~Q
) |
|
Theorem | distrnqg 6577 |
Multiplication of positive fractions is distributive. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q
(𝐴
·Q 𝐶))) |
|
Theorem | 1qec 6578 |
The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|
⊢ (𝐴 ∈ N →
1Q = [〈𝐴, 𝐴〉] ~Q
) |
|
Theorem | mulidnq 6579 |
Multiplication identity element for positive fractions. (Contributed by
NM, 3-Mar-1996.)
|
⊢ (𝐴 ∈ Q → (𝐴
·Q 1Q) = 𝐴) |
|
Theorem | recexnq 6580* |
Existence of positive fraction reciprocal. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
⊢ (𝐴 ∈ Q → ∃𝑦(𝑦 ∈ Q ∧ (𝐴
·Q 𝑦) =
1Q)) |
|
Theorem | recmulnqg 6581 |
Relationship between reciprocal and multiplication on positive
fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) =
1Q)) |
|
Theorem | recclnq 6582 |
Closure law for positive fraction reciprocal. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
⊢ (𝐴 ∈ Q →
(*Q‘𝐴) ∈ Q) |
|
Theorem | recidnq 6583 |
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 6584 |
Reciprocal of reciprocal of positive fraction. (Contributed by NM,
26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
|
⊢ (𝐴 ∈ Q →
(*Q‘(*Q‘𝐴)) = 𝐴) |
|
Theorem | rec1nq 6585 |
Reciprocal of positive fraction one. (Contributed by Jim Kingdon,
29-Dec-2019.)
|
⊢
(*Q‘1Q) =
1Q |
|
Theorem | nqtri3or 6586 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<Q 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴)) |
|
Theorem | ltdcnq 6587 |
Less-than for positive fractions is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
DECID 𝐴
<Q 𝐵) |
|
Theorem | ltsonq 6588 |
'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 6589 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<Q 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴))) |
|
Theorem | ltanqg 6590 |
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 6591 |
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 6592 |
Ordering property of addition for positive fractions. One direction of
ltanqg 6590. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 +Q
𝐴)
<Q (𝐶 +Q 𝐵)) |
|
Theorem | ltmnqi 6593 |
Ordering property of multiplication for positive fractions. One direction
of ltmnqg 6591. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶
·Q 𝐴) <Q (𝐶
·Q 𝐵)) |
|
Theorem | lt2addnq 6594 |
Ordering property of addition for positive fractions. (Contributed by Jim
Kingdon, 7-Dec-2019.)
|
⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧
(𝐶 ∈ Q
∧ 𝐷 ∈
Q)) → ((𝐴 <Q 𝐵 ∧ 𝐶 <Q 𝐷) → (𝐴 +Q 𝐶)
<Q (𝐵 +Q 𝐷))) |
|
Theorem | lt2mulnq 6595 |
Ordering property of multiplication for positive fractions. (Contributed
by Jim Kingdon, 18-Jul-2021.)
|
⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧
(𝐶 ∈ Q
∧ 𝐷 ∈
Q)) → ((𝐴 <Q 𝐵 ∧ 𝐶 <Q 𝐷) → (𝐴 ·Q 𝐶)
<Q (𝐵 ·Q 𝐷))) |
|
Theorem | 1lt2nq 6596 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
(Revised by Mario Carneiro, 10-May-2013.)
|
⊢ 1Q
<Q (1Q
+Q 1Q) |
|
Theorem | ltaddnq 6597 |
The sum of two fractions is greater than one of them. (Contributed by
NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
𝐴
<Q (𝐴 +Q 𝐵)) |
|
Theorem | ltexnqq 6598* |
Ordering on positive fractions in terms of existence of sum. Definition
in Proposition 9-2.6 of [Gleason] p.
119. (Contributed by Jim Kingdon,
23-Sep-2019.)
|
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) →
(𝐴
<Q 𝐵 ↔ ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵)) |
|
Theorem | ltexnqi 6599* |
Ordering on positive fractions in terms of existence of sum.
(Contributed by Jim Kingdon, 30-Apr-2020.)
|
⊢ (𝐴 <Q 𝐵 → ∃𝑥 ∈ Q (𝐴 +Q
𝑥) = 𝐵) |
|
Theorem | halfnqq 6600* |
One-half of any positive fraction is a fraction. (Contributed by Jim
Kingdon, 23-Sep-2019.)
|
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +Q
𝑥) = 𝐴) |