Type  Label  Description 
Statement 

Theorem  9t5e45 8201 
9 times 5 equals 45. (Contributed by Mario Carneiro, 19Apr2015.)

; 

Theorem  9t6e54 8202 
9 times 6 equals 54. (Contributed by Mario Carneiro, 19Apr2015.)

; 

Theorem  9t7e63 8203 
9 times 7 equals 63. (Contributed by Mario Carneiro, 19Apr2015.)

; 

Theorem  9t8e72 8204 
9 times 8 equals 72. (Contributed by Mario Carneiro, 19Apr2015.)

; 

Theorem  9t9e81 8205 
9 times 9 equals 81. (Contributed by Mario Carneiro, 19Apr2015.)

; 

Theorem  decbin0 8206 
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  decbin2 8207 
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  decbin3 8208 
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18Feb2014.)



3.4.10 Upper sets of integers


Syntax  cuz 8209 
Extend class notation with the upper integer function.
Read " " as "the
set of integers greater than or equal to
."



Definition  dfuz 8210* 
Define a function whose value at is the semiinfinite set of
contiguous integers starting at , which we will also call the
upper integers starting at . Read " " as "the
set
of integers greater than or equal to ." See uzval 8211 for its
value, uzssz 8228 for its relationship to , nnuz 8244
and nn0uz 8243 for
its relationships to and , and eluz1 8213 and eluz2 8215 for
its membership relations. (Contributed by NM, 5Sep2005.)



Theorem  uzval 8211* 
The value of the upper integers function. (Contributed by NM,
5Sep2005.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  uzf 8212 
The domain and range of the upper integers function. (Contributed by
Scott Fenton, 8Aug2013.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  eluz1 8213 
Membership in the upper set of integers starting at .
(Contributed by NM, 5Sep2005.)



Theorem  eluzel2 8214 
Implication of membership in an upper set of integers. (Contributed by
NM, 6Sep2005.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  eluz2 8215 
Membership in an upper set of integers. We use the fact that a
function's value (under our function value definition) is empty outside
of its domain to show . (Contributed by NM,
5Sep2005.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  eluz1i 8216 
Membership in an upper set of integers. (Contributed by NM,
5Sep2005.)



Theorem  eluzuzle 8217 
An integer in an upper set of integers is an element of an upper set of
integers with a smaller bound. (Contributed by Alexander van der Vekens,
17Jun2018.)



Theorem  eluzelz 8218 
A member of an upper set of integers is an integer. (Contributed by NM,
6Sep2005.)



Theorem  eluzelre 8219 
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31Aug2013.)



Theorem  eluzelcn 8220 
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29Jun2017.)



Theorem  eluzle 8221 
Implication of membership in an upper set of integers. (Contributed by
NM, 6Sep2005.)



Theorem  eluz 8222 
Membership in an upper set of integers. (Contributed by NM,
2Oct2005.)



Theorem  uzid 8223 
Membership of the least member in an upper set of integers. (Contributed
by NM, 2Sep2005.)



Theorem  uzn0 8224 
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16Jan2014.)



Theorem  uztrn 8225 
Transitive law for sets of upper integers. (Contributed by NM,
20Sep2005.)



Theorem  uztrn2 8226 
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26Dec2013.)



Theorem  uzneg 8227 
Contraposition law for upper integers. (Contributed by NM,
28Nov2005.)



Theorem  uzssz 8228 
An upper set of integers is a subset of all integers. (Contributed by
NM, 2Sep2005.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  uzss 8229 
Subset relationship for two sets of upper integers. (Contributed by NM,
5Sep2005.)



Theorem  uztric 8230 
Trichotomy of the ordering relation on integers, stated in terms of upper
integers. (Contributed by NM, 6Jul2005.) (Revised by Mario Carneiro,
25Jun2013.)



Theorem  uz11 8231 
The upper integers function is onetoone. (Contributed by NM,
12Dec2005.)



Theorem  eluzp1m1 8232 
Membership in the next upper set of integers. (Contributed by NM,
12Sep2005.)



Theorem  eluzp1l 8233 
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12Sep2005.)



Theorem  eluzp1p1 8234 
Membership in the next upper set of integers. (Contributed by NM,
5Oct2005.)



Theorem  eluzaddi 8235 
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22Nov2007.)



Theorem  eluzsubi 8236 
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22Nov2007.)



Theorem  eluzadd 8237 
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  eluzsub 8238 
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2Sep2009.)



Theorem  uzm1 8239 
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  uznn0sub 8240 
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4Sep2005.)



Theorem  uzin 8241 
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24Dec2013.)



Theorem  uzp1 8242 
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  nn0uz 8243 
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2Sep2005.)



Theorem  nnuz 8244 
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2Sep2005.)



Theorem  elnnuz 8245 
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6Jun2006.)



Theorem  elnn0uz 8246 
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6Jun2006.)



Theorem  eluz2nn 8247 
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3Nov2018.)



Theorem  eluzge2nn0 8248 
If an integer is greater than or equal to 2, then it is a nonnegative
integer. (Contributed by AV, 27Aug2018.) (Proof shortened by AV,
3Nov2018.)



Theorem  uzuzle23 8249 
An integer in the upper set of integers starting at 3 is element of the
upper set of integers starting at 2. (Contributed by Alexander van der
Vekens, 17Sep2018.)



Theorem  eluzge3nn 8250 
If an integer is greater than 3, then it is a positive integer.
(Contributed by Alexander van der Vekens, 17Sep2018.)



Theorem  uz3m2nn 8251 
An integer greater than or equal to 3 decreased by 2 is a positive
integer. (Contributed by Alexander van der Vekens, 17Sep2018.)



Theorem  1eluzge0 8252 
1 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.)



Theorem  2eluzge0 8253 
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.) (Proof shortened by OpenAI, 25Mar2020.)



Theorem  2eluzge0OLD 8254 
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8Jun2018.) Obsolete version of 2eluzge0 8253 as of
25Mar2020. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  2eluzge1 8255 
2 is an integer greater than or equal to 1. (Contributed by Alexander van
der Vekens, 8Jun2018.)



Theorem  uznnssnn 8256 
The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29Jun2013.)



Theorem  raluz 8257* 
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  raluz2 8258* 
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  rexuz 8259* 
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  rexuz2 8260* 
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9Sep2005.)



Theorem  2rexuz 8261* 
Double existential quantification in an upper set of integers.
(Contributed by NM, 3Nov2005.)



Theorem  peano2uz 8262 
Second Peano postulate for an upper set of integers. (Contributed by NM,
7Sep2005.)



Theorem  peano2uzs 8263 
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26Dec2013.)



Theorem  peano2uzr 8264 
Reversed second Peano axiom for upper integers. (Contributed by NM,
2Jan2006.)



Theorem  uzaddcl 8265 
Addition closure law for an upper set of integers. (Contributed by NM,
4Jun2006.)



Theorem  nn0pzuz 8266 
The sum of a nonnegative integer and an integer is an integer greater than
or equal to that integer. (Contributed by Alexander van der Vekens,
3Oct2018.)



Theorem  uzind4 8267* 
Induction on the upper set of integers that starts at an integer
. The first
four hypotheses give us the substitution instances we
need, and the last two are the basis and the induction step.
(Contributed by NM, 7Sep2005.)



Theorem  uzind4ALT 8268* 
Induction on the upper set of integers that starts at an integer
. The last
four hypotheses give us the substitution instances we
need; the first two are the basis and the induction step. Either
uzind4 8267 or uzind4ALT 8268 may be used; see comment for nnind 7671.
(Contributed by NM, 7Sep2005.) (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  uzind4s 8269* 
Induction on the upper set of integers that starts at an integer ,
using explicit substitution. The hypotheses are the basis and the
induction step. (Contributed by NM, 4Nov2005.)



Theorem  uzind4s2 8270* 
Induction on the upper set of integers that starts at an integer ,
using explicit substitution. The hypotheses are the basis and the
induction step. Use this instead of uzind4s 8269 when and
must
be distinct in . (Contributed by NM,
16Nov2005.)



Theorem  uzind4i 8271* 
Induction on the upper integers that start at . The first
hypothesis specifies the lower bound, the next four give us the
substitution instances we need, and the last two are the basis and the
induction step. (Contributed by NM, 4Sep2005.)



Theorem  indstr 8272* 
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17Aug2001.)



Theorem  eluznn0 8273 
Membership in a nonnegative upper set of integers implies membership in
.
(Contributed by Paul Chapman, 22Jun2011.)



Theorem  eluznn 8274 
Membership in a positive upper set of integers implies membership in
. (Contributed
by JJ, 1Oct2018.)



Theorem  eluz2b1 8275 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)



Theorem  eluz2b2 8276 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)



Theorem  eluz2b3 8277 
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23Nov2012.)



Theorem  uz2m1nn 8278 
One less than an integer greater than or equal to 2 is a positive
integer. (Contributed by Paul Chapman, 17Nov2012.)



Theorem  1nuz2 8279 
1 is not in . (Contributed by Paul Chapman,
21Nov2012.)



Theorem  elnn1uz2 8280 
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17Nov2012.)



Theorem  uz2mulcl 8281 
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26Oct2012.)



Theorem  indstr2 8282* 
Strong Mathematical Induction for positive integers (inference schema).
The first two hypotheses give us the substitution instances we need; the
last two are the basis and the induction step. (Contributed by Paul
Chapman, 21Nov2012.)



Theorem  eluzdc 8283 
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18Apr2020.)

DECID 

Theorem  ublbneg 8284* 
The image under negation of a boundedabove set of reals is bounded
below. (Contributed by Paul Chapman, 21Mar2011.)



Theorem  eqreznegel 8285* 
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21Mar2011.)



Theorem  negm 8286* 
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10Apr2020.)



Theorem  lbzbi 8287* 
If a set of reals is bounded below, it is bounded below by an integer.
(Contributed by Paul Chapman, 21Mar2011.)



Theorem  nn01to3 8288 
A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed
by Alexander van der Vekens, 13Sep2018.)



Theorem  nn0ge2m1nnALT 8289 
Alternate proof of nn0ge2m1nn 7978: If a nonnegative integer is greater
than or equal to two, the integer decreased by 1 is a positive integer.
This version is proved using eluz2 8215, a theorem for upper sets of
integers, which are defined later than the positive and nonnegative
integers. This proof is, however, much shorter than the proof of
nn0ge2m1nn 7978. (Contributed by Alexander van der Vekens,
1Aug2018.)
(New usage is discouraged.) (Proof modification is discouraged.)



3.4.11 Rational numbers (as a subset of complex
numbers)


Syntax  cq 8290 
Extend class notation to include the class of rationals.



Definition  dfq 8291 
Define the set of rational numbers. Based on definition of rationals in
[Apostol] p. 22. See elq 8293
for the relation "is rational." (Contributed
by NM, 8Jan2002.)



Theorem  divfnzn 8292 
Division restricted to is a function. Given
excluded
middle, it would be easy to prove this for .
The key difference is that an element of is apart from zero,
whereas being an element of
implies being not equal to
zero. (Contributed by Jim Kingdon, 19Mar2020.)



Theorem  elq 8293* 
Membership in the set of rationals. (Contributed by NM, 8Jan2002.)
(Revised by Mario Carneiro, 28Jan2014.)



Theorem  qmulz 8294* 
If is rational, then
some integer multiple of it is an integer.
(Contributed by NM, 7Nov2008.) (Revised by Mario Carneiro,
22Jul2014.)



Theorem  znq 8295 
The ratio of an integer and a positive integer is a rational number.
(Contributed by NM, 12Jan2002.)



Theorem  qre 8296 
A rational number is a real number. (Contributed by NM,
14Nov2002.)



Theorem  zq 8297 
An integer is a rational number. (Contributed by NM, 9Jan2002.)



Theorem  zssq 8298 
The integers are a subset of the rationals. (Contributed by NM,
9Jan2002.)



Theorem  nn0ssq 8299 
The nonnegative integers are a subset of the rationals. (Contributed by
NM, 31Jul2004.)



Theorem  nnssq 8300 
The positive integers are a subset of the rationals. (Contributed by NM,
31Jul2004.)

