Theorem List for Intuitionistic Logic Explorer - 7101-7200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | dmaddpi 7101 |
Domain of addition on positive integers. (Contributed by NM,
26-Aug-1995.)
|
|
|
Theorem | dmmulpi 7102 |
Domain of multiplication on positive integers. (Contributed by NM,
26-Aug-1995.)
|
|
|
Theorem | addclpi 7103 |
Closure of addition of positive integers. (Contributed by NM,
18-Oct-1995.)
|
|
|
Theorem | mulclpi 7104 |
Closure of multiplication of positive integers. (Contributed by NM,
18-Oct-1995.)
|
|
|
Theorem | addcompig 7105 |
Addition of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | addasspig 7106 |
Addition of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | mulcompig 7107 |
Multiplication of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | mulasspig 7108 |
Multiplication of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | distrpig 7109 |
Multiplication of positive integers is distributive. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | addcanpig 7110 |
Addition cancellation law for positive integers. (Contributed by Jim
Kingdon, 27-Aug-2019.)
|
|
|
Theorem | mulcanpig 7111 |
Multiplication cancellation law for positive integers. (Contributed by
Jim Kingdon, 29-Aug-2019.)
|
|
|
Theorem | addnidpig 7112 |
There is no identity element for addition on positive integers.
(Contributed by NM, 28-Nov-1995.)
|
|
|
Theorem | ltexpi 7113* |
Ordering on positive integers in terms of existence of sum.
(Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro,
14-Jun-2013.)
|
|
|
Theorem | ltapig 7114 |
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31-Aug-2019.)
|
|
|
Theorem | ltmpig 7115 |
Ordering property of multiplication for positive integers. (Contributed
by Jim Kingdon, 31-Aug-2019.)
|
|
|
Theorem | 1lt2pi 7116 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|
|
|
Theorem | nlt1pig 7117 |
No positive integer is less than one. (Contributed by Jim Kingdon,
31-Aug-2019.)
|
|
|
Theorem | indpi 7118* |
Principle of Finite Induction on positive integers. (Contributed by NM,
23-Mar-1996.)
|
|
|
Theorem | nnppipi 7119 |
A natural number plus a positive integer is a positive integer.
(Contributed by Jim Kingdon, 10-Nov-2019.)
|
|
|
Definition | df-plpq 7120* |
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
(df-plqqs 7125) works with the equivalence classes of these
ordered pairs determined by the equivalence relation
(df-enq 7123). (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.)
|
|
|
Definition | df-mpq 7121* |
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.)
|
|
|
Definition | df-ltpq 7122* |
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.)
|
|
|
Definition | df-enq 7123* |
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.)
|
|
|
Definition | df-nqqs 7124 |
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.)
|
|
|
Definition | df-plqqs 7125* |
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.)
|
|
|
Definition | df-mqqs 7126* |
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.)
|
|
|
Definition | df-1nqqs 7127 |
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.)
|
|
|
Definition | df-rq 7128* |
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.)
|
|
|
Definition | df-ltnqqs 7129* |
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.)
|
|
|
Theorem | dfplpq2 7130* |
Alternate definition of pre-addition on positive fractions.
(Contributed by Jim Kingdon, 12-Sep-2019.)
|
|
|
Theorem | dfmpq2 7131* |
Alternate definition of pre-multiplication on positive fractions.
(Contributed by Jim Kingdon, 13-Sep-2019.)
|
|
|
Theorem | enqbreq 7132 |
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by NM, 27-Aug-1995.)
|
|
|
Theorem | enqbreq2 7133 |
Equivalence relation for positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | enqer 7134 |
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.)
|
|
|
Theorem | enqeceq 7135 |
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29-Nov-1995.)
|
|
|
Theorem | enqex 7136 |
The equivalence relation for positive fractions exists. (Contributed by
NM, 3-Sep-1995.)
|
|
|
Theorem | enqdc 7137 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
DECID
|
|
Theorem | enqdc1 7138 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
DECID |
|
Theorem | nqex 7139 |
The class of positive fractions exists. (Contributed by NM,
16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
|
|
Theorem | 0nnq 7140 |
The empty set is not a positive fraction. (Contributed by NM,
24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
|
|
Theorem | ltrelnq 7141 |
Positive fraction 'less than' is a relation on positive fractions.
(Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro,
27-Apr-2013.)
|
|
|
Theorem | 1nq 7142 |
The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|
|
|
Theorem | addcmpblnq 7143 |
Lemma showing compatibility of addition. (Contributed by NM,
27-Aug-1995.)
|
|
|
Theorem | mulcmpblnq 7144 |
Lemma showing compatibility of multiplication. (Contributed by NM,
27-Aug-1995.)
|
|
|
Theorem | addpipqqslem 7145 |
Lemma for addpipqqs 7146. (Contributed by Jim Kingdon, 11-Sep-2019.)
|
|
|
Theorem | addpipqqs 7146 |
Addition of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
|
|
Theorem | mulpipq2 7147 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | mulpipq 7148 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro,
8-May-2013.)
|
|
|
Theorem | mulpipqqs 7149 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
|
|
Theorem | ordpipqqs 7150 |
Ordering of positive fractions in terms of positive integers.
(Contributed by Jim Kingdon, 14-Sep-2019.)
|
|
|
Theorem | addclnq 7151 |
Closure of addition on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
|
|
Theorem | mulclnq 7152 |
Closure of multiplication on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
|
|
Theorem | dmaddpqlem 7153* |
Decomposition of a positive fraction into numerator and denominator.
Lemma for dmaddpq 7155. (Contributed by Jim Kingdon, 15-Sep-2019.)
|
|
|
Theorem | nqpi 7154* |
Decomposition of a positive fraction into numerator and denominator.
Similar to dmaddpqlem 7153 but also shows that the numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
|
|
Theorem | dmaddpq 7155 |
Domain of addition on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | dmmulpq 7156 |
Domain of multiplication on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | addcomnqg 7157 |
Addition of positive fractions is commutative. (Contributed by Jim
Kingdon, 15-Sep-2019.)
|
|
|
Theorem | addassnqg 7158 |
Addition of positive fractions is associative. (Contributed by Jim
Kingdon, 16-Sep-2019.)
|
|
|
Theorem | mulcomnqg 7159 |
Multiplication of positive fractions is commutative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | mulassnqg 7160 |
Multiplication of positive fractions is associative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | mulcanenq 7161 |
Lemma for distributive law: cancellation of common factor. (Contributed
by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | mulcanenqec 7162 |
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | distrnqg 7163 |
Multiplication of positive fractions is distributive. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | 1qec 7164 |
The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|
|
|
Theorem | mulidnq 7165 |
Multiplication identity element for positive fractions. (Contributed by
NM, 3-Mar-1996.)
|
|
|
Theorem | recexnq 7166* |
Existence of positive fraction reciprocal. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
|
|
Theorem | recmulnqg 7167 |
Relationship between reciprocal and multiplication on positive
fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
|
|
|
Theorem | recclnq 7168 |
Closure law for positive fraction reciprocal. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | recidnq 7169 |
A positive fraction times its reciprocal is 1. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | recrecnq 7170 |
Reciprocal of reciprocal of positive fraction. (Contributed by NM,
26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
|
|
|
Theorem | rec1nq 7171 |
Reciprocal of positive fraction one. (Contributed by Jim Kingdon,
29-Dec-2019.)
|
|
|
Theorem | nqtri3or 7172 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
|
|
Theorem | ltdcnq 7173 |
Less-than for positive fractions is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
DECID |
|
Theorem | ltsonq 7174 |
'Less than' is a strict ordering on positive fractions. (Contributed by
NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
|
|
|
Theorem | nqtric 7175 |
Trichotomy for positive fractions. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
|
|
Theorem | ltanqg 7176 |
Ordering property of addition for positive fractions. Proposition
9-2.6(ii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22-Sep-2019.)
|
|
|
Theorem | ltmnqg 7177 |
Ordering property of multiplication for positive fractions. Proposition
9-2.6(iii) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
22-Sep-2019.)
|
|
|
Theorem | ltanqi 7178 |
Ordering property of addition for positive fractions. One direction of
ltanqg 7176. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
|
|
Theorem | ltmnqi 7179 |
Ordering property of multiplication for positive fractions. One direction
of ltmnqg 7177. (Contributed by Jim Kingdon, 9-Dec-2019.)
|
|
|
Theorem | lt2addnq 7180 |
Ordering property of addition for positive fractions. (Contributed by Jim
Kingdon, 7-Dec-2019.)
|
|
|
Theorem | lt2mulnq 7181 |
Ordering property of multiplication for positive fractions. (Contributed
by Jim Kingdon, 18-Jul-2021.)
|
|
|
Theorem | 1lt2nq 7182 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
(Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | ltaddnq 7183 |
The sum of two fractions is greater than one of them. (Contributed by
NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | ltexnqq 7184* |
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.)
|
|
|
Theorem | ltexnqi 7185* |
Ordering on positive fractions in terms of existence of sum.
(Contributed by Jim Kingdon, 30-Apr-2020.)
|
|
|
Theorem | halfnqq 7186* |
One-half of any positive fraction is a fraction. (Contributed by Jim
Kingdon, 23-Sep-2019.)
|
|
|
Theorem | halfnq 7187* |
One-half of any positive fraction exists. Lemma for Proposition
9-2.6(i) of [Gleason] p. 120.
(Contributed by NM, 16-Mar-1996.)
(Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | nsmallnqq 7188* |
There is no smallest positive fraction. (Contributed by Jim Kingdon,
24-Sep-2019.)
|
|
|
Theorem | nsmallnq 7189* |
There is no smallest positive fraction. (Contributed by NM,
26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | subhalfnqq 7190* |
There is a number which is less than half of any positive fraction. The
case where is
one is Lemma 11.4 of [BauerTaylor], p. 50,
and they
use the word "approximate half" for such a number (since there
may be
constructions, for some structures other than the rationals themselves,
which rely on such an approximate half but do not require division by
two as seen at halfnqq 7186). (Contributed by Jim Kingdon,
25-Nov-2019.)
|
|
|
Theorem | ltbtwnnqq 7191* |
There exists a number between any two positive fractions. Proposition
9-2.6(i) of [Gleason] p. 120.
(Contributed by Jim Kingdon,
24-Sep-2019.)
|
|
|
Theorem | ltbtwnnq 7192* |
There exists a number between any two positive fractions. Proposition
9-2.6(i) of [Gleason] p. 120.
(Contributed by NM, 17-Mar-1996.)
(Revised by Mario Carneiro, 10-May-2013.)
|
|
|
Theorem | archnqq 7193* |
For any fraction, there is an integer that is greater than it. This is
also known as the "archimedean property". (Contributed by Jim
Kingdon,
1-Dec-2019.)
|
|
|
Theorem | prarloclemarch 7194* |
A version of the Archimedean property. This variation is "stronger"
than archnqq 7193 in the sense that we provide an integer which
is larger
than a given rational even after being multiplied by a second
rational .
(Contributed by Jim Kingdon, 30-Nov-2019.)
|
|
|
Theorem | prarloclemarch2 7195* |
Like prarloclemarch 7194 but the integer must be at least two, and
there is
also added to
the right hand side. These details follow
straightforwardly but are chosen to be helpful in the proof of
prarloc 7279. (Contributed by Jim Kingdon, 25-Nov-2019.)
|
|
|
Theorem | ltrnqg 7196 |
Ordering property of reciprocal for positive fractions. For a simplified
version of the forward implication, see ltrnqi 7197. (Contributed by Jim
Kingdon, 29-Dec-2019.)
|
|
|
Theorem | ltrnqi 7197 |
Ordering property of reciprocal for positive fractions. For the converse,
see ltrnqg 7196. (Contributed by Jim Kingdon, 24-Sep-2019.)
|
|
|
Theorem | nnnq 7198 |
The canonical embedding of positive integers into positive fractions.
(Contributed by Jim Kingdon, 26-Apr-2020.)
|
|
|
Theorem | ltnnnq 7199 |
Ordering of positive integers via or is equivalent.
(Contributed by Jim Kingdon, 3-Oct-2020.)
|
|
|
Definition | df-enq0 7200* |
Define equivalence relation for nonnegative fractions. This is a
"temporary" set used in the construction of complex numbers,
and is
intended to be used only by the construction. (Contributed by Jim
Kingdon, 2-Nov-2019.)
|
~Q0
|