Theorem List for Intuitionistic Logic Explorer - 7101-7200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Syntax | cpp 7101 |
Positive real addition.
|
|
|
Syntax | cmp 7102 |
Positive real multiplication.
|
|
|
Syntax | cltp 7103 |
Positive real ordering relation.
|
|
|
Syntax | cer 7104 |
Equivalence class used to construct signed reals.
|
|
|
Syntax | cnr 7105 |
Set of signed reals.
|
|
|
Syntax | c0r 7106 |
The signed real constant 0.
|
|
|
Syntax | c1r 7107 |
The signed real constant 1.
|
|
|
Syntax | cm1r 7108 |
The signed real constant -1.
|
|
|
Syntax | cplr 7109 |
Signed real addition.
|
|
|
Syntax | cmr 7110 |
Signed real multiplication.
|
|
|
Syntax | cltr 7111 |
Signed real ordering relation.
|
|
|
Definition | df-ni 7112 |
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.)
|
|
|
Definition | df-pli 7113 |
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.)
|
|
|
Definition | df-mi 7114 |
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.)
|
|
|
Definition | df-lti 7115 |
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.)
|
|
|
Theorem | elni 7116 |
Membership in the class of positive integers. (Contributed by NM,
15-Aug-1995.)
|
|
|
Theorem | pinn 7117 |
A positive integer is a natural number. (Contributed by NM,
15-Aug-1995.)
|
|
|
Theorem | pion 7118 |
A positive integer is an ordinal number. (Contributed by NM,
23-Mar-1996.)
|
|
|
Theorem | piord 7119 |
A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|
|
|
Theorem | niex 7120 |
The class of positive integers is a set. (Contributed by NM,
15-Aug-1995.)
|
|
|
Theorem | 0npi 7121 |
The empty set is not a positive integer. (Contributed by NM,
26-Aug-1995.)
|
|
|
Theorem | elni2 7122 |
Membership in the class of positive integers. (Contributed by NM,
27-Nov-1995.)
|
|
|
Theorem | 1pi 7123 |
Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|
|
|
Theorem | addpiord 7124 |
Positive integer addition in terms of ordinal addition. (Contributed by
NM, 27-Aug-1995.)
|
|
|
Theorem | mulpiord 7125 |
Positive integer multiplication in terms of ordinal multiplication.
(Contributed by NM, 27-Aug-1995.)
|
|
|
Theorem | mulidpi 7126 |
1 is an identity element for multiplication on positive integers.
(Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro,
17-Nov-2014.)
|
|
|
Theorem | ltpiord 7127 |
Positive integer 'less than' in terms of ordinal membership. (Contributed
by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
|
|
Theorem | ltsopi 7128 |
Positive integer 'less than' is a strict ordering. (Contributed by NM,
8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
|
|
|
Theorem | pitric 7129 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
|
|
Theorem | pitri3or 7130 |
Trichotomy for positive integers. (Contributed by Jim Kingdon,
21-Sep-2019.)
|
|
|
Theorem | ltdcpi 7131 |
Less-than for positive integers is decidable. (Contributed by Jim
Kingdon, 12-Dec-2019.)
|
DECID |
|
Theorem | ltrelpi 7132 |
Positive integer 'less than' is a relation on positive integers.
(Contributed by NM, 8-Feb-1996.)
|
|
|
Theorem | dmaddpi 7133 |
Domain of addition on positive integers. (Contributed by NM,
26-Aug-1995.)
|
|
|
Theorem | dmmulpi 7134 |
Domain of multiplication on positive integers. (Contributed by NM,
26-Aug-1995.)
|
|
|
Theorem | addclpi 7135 |
Closure of addition of positive integers. (Contributed by NM,
18-Oct-1995.)
|
|
|
Theorem | mulclpi 7136 |
Closure of multiplication of positive integers. (Contributed by NM,
18-Oct-1995.)
|
|
|
Theorem | addcompig 7137 |
Addition of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | addasspig 7138 |
Addition of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | mulcompig 7139 |
Multiplication of positive integers is commutative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | mulasspig 7140 |
Multiplication of positive integers is associative. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | distrpig 7141 |
Multiplication of positive integers is distributive. (Contributed by Jim
Kingdon, 26-Aug-2019.)
|
|
|
Theorem | addcanpig 7142 |
Addition cancellation law for positive integers. (Contributed by Jim
Kingdon, 27-Aug-2019.)
|
|
|
Theorem | mulcanpig 7143 |
Multiplication cancellation law for positive integers. (Contributed by
Jim Kingdon, 29-Aug-2019.)
|
|
|
Theorem | addnidpig 7144 |
There is no identity element for addition on positive integers.
(Contributed by NM, 28-Nov-1995.)
|
|
|
Theorem | ltexpi 7145* |
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 7146 |
Ordering property of addition for positive integers. (Contributed by Jim
Kingdon, 31-Aug-2019.)
|
|
|
Theorem | ltmpig 7147 |
Ordering property of multiplication for positive integers. (Contributed
by Jim Kingdon, 31-Aug-2019.)
|
|
|
Theorem | 1lt2pi 7148 |
One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|
|
|
Theorem | nlt1pig 7149 |
No positive integer is less than one. (Contributed by Jim Kingdon,
31-Aug-2019.)
|
|
|
Theorem | indpi 7150* |
Principle of Finite Induction on positive integers. (Contributed by NM,
23-Mar-1996.)
|
|
|
Theorem | nnppipi 7151 |
A natural number plus a positive integer is a positive integer.
(Contributed by Jim Kingdon, 10-Nov-2019.)
|
|
|
Definition | df-plpq 7152* |
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 7157) works with the equivalence classes of these
ordered pairs determined by the equivalence relation
(df-enq 7155). (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 7153* |
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 7154* |
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 7155* |
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 7156 |
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 7157* |
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 7158* |
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 7159 |
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 7160* |
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 7161* |
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 7162* |
Alternate definition of pre-addition on positive fractions.
(Contributed by Jim Kingdon, 12-Sep-2019.)
|
|
|
Theorem | dfmpq2 7163* |
Alternate definition of pre-multiplication on positive fractions.
(Contributed by Jim Kingdon, 13-Sep-2019.)
|
|
|
Theorem | enqbreq 7164 |
Equivalence relation for positive fractions in terms of positive
integers. (Contributed by NM, 27-Aug-1995.)
|
|
|
Theorem | enqbreq2 7165 |
Equivalence relation for positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | enqer 7166 |
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 7167 |
Equivalence class equality of positive fractions in terms of positive
integers. (Contributed by NM, 29-Nov-1995.)
|
|
|
Theorem | enqex 7168 |
The equivalence relation for positive fractions exists. (Contributed by
NM, 3-Sep-1995.)
|
|
|
Theorem | enqdc 7169 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
DECID
|
|
Theorem | enqdc1 7170 |
The equivalence relation for positive fractions is decidable.
(Contributed by Jim Kingdon, 7-Sep-2019.)
|
DECID |
|
Theorem | nqex 7171 |
The class of positive fractions exists. (Contributed by NM,
16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
|
|
Theorem | 0nnq 7172 |
The empty set is not a positive fraction. (Contributed by NM,
24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|
|
|
Theorem | ltrelnq 7173 |
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 7174 |
The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|
|
|
Theorem | addcmpblnq 7175 |
Lemma showing compatibility of addition. (Contributed by NM,
27-Aug-1995.)
|
|
|
Theorem | mulcmpblnq 7176 |
Lemma showing compatibility of multiplication. (Contributed by NM,
27-Aug-1995.)
|
|
|
Theorem | addpipqqslem 7177 |
Lemma for addpipqqs 7178. (Contributed by Jim Kingdon, 11-Sep-2019.)
|
|
|
Theorem | addpipqqs 7178 |
Addition of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
|
|
Theorem | mulpipq2 7179 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | mulpipq 7180 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro,
8-May-2013.)
|
|
|
Theorem | mulpipqqs 7181 |
Multiplication of positive fractions in terms of positive integers.
(Contributed by NM, 28-Aug-1995.)
|
|
|
Theorem | ordpipqqs 7182 |
Ordering of positive fractions in terms of positive integers.
(Contributed by Jim Kingdon, 14-Sep-2019.)
|
|
|
Theorem | addclnq 7183 |
Closure of addition on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
|
|
Theorem | mulclnq 7184 |
Closure of multiplication on positive fractions. (Contributed by NM,
29-Aug-1995.)
|
|
|
Theorem | dmaddpqlem 7185* |
Decomposition of a positive fraction into numerator and denominator.
Lemma for dmaddpq 7187. (Contributed by Jim Kingdon, 15-Sep-2019.)
|
|
|
Theorem | nqpi 7186* |
Decomposition of a positive fraction into numerator and denominator.
Similar to dmaddpqlem 7185 but also shows that the numerator and
denominator are positive integers. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
|
|
Theorem | dmaddpq 7187 |
Domain of addition on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | dmmulpq 7188 |
Domain of multiplication on positive fractions. (Contributed by NM,
24-Aug-1995.)
|
|
|
Theorem | addcomnqg 7189 |
Addition of positive fractions is commutative. (Contributed by Jim
Kingdon, 15-Sep-2019.)
|
|
|
Theorem | addassnqg 7190 |
Addition of positive fractions is associative. (Contributed by Jim
Kingdon, 16-Sep-2019.)
|
|
|
Theorem | mulcomnqg 7191 |
Multiplication of positive fractions is commutative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | mulassnqg 7192 |
Multiplication of positive fractions is associative. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | mulcanenq 7193 |
Lemma for distributive law: cancellation of common factor. (Contributed
by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
|
|
|
Theorem | mulcanenqec 7194 |
Lemma for distributive law: cancellation of common factor. (Contributed
by Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | distrnqg 7195 |
Multiplication of positive fractions is distributive. (Contributed by
Jim Kingdon, 17-Sep-2019.)
|
|
|
Theorem | 1qec 7196 |
The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|
|
|
Theorem | mulidnq 7197 |
Multiplication identity element for positive fractions. (Contributed by
NM, 3-Mar-1996.)
|
|
|
Theorem | recexnq 7198* |
Existence of positive fraction reciprocal. (Contributed by Jim Kingdon,
20-Sep-2019.)
|
|
|
Theorem | recmulnqg 7199 |
Relationship between reciprocal and multiplication on positive
fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
|
|
|
Theorem | recclnq 7200 |
Closure law for positive fraction reciprocal. (Contributed by NM,
6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|
|