Theorem List for Intuitionistic Logic Explorer - 9301-9400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 9t7e63 9301 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t8e72 9302 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t9e81 9303 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t11e99 9304 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
; ; |
|
Theorem | 9lt10 9305 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
; |
|
Theorem | 8lt10 9306 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
; |
|
Theorem | 7lt10 9307 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 6lt10 9308 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 5lt10 9309 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 4lt10 9310 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 3lt10 9311 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 2lt10 9312 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 1lt10 9313 |
1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario
Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | decbin0 9314 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin2 9315 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin3 9316 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | halfthird 9317 |
Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|
|
|
Theorem | 5recm6rec 9318 |
One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
|
; |
|
4.4.11 Upper sets of integers
|
|
Syntax | cuz 9319 |
Extend class notation with the upper integer function.
Read " " as "the
set of integers greater than or equal to
."
|
|
|
Definition | df-uz 9320* |
Define a function whose value at is the semi-infinite 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 9321 for its
value, uzssz 9338 for its relationship to , nnuz 9354
and nn0uz 9353 for
its relationships to and , and eluz1 9323 and eluz2 9325 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | uzval 9321* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | uzf 9322 |
The domain and range of the upper integers function. (Contributed by
Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | eluz1 9323 |
Membership in the upper set of integers starting at .
(Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | eluzel2 9324 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | eluz2 9325 |
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,
5-Sep-2005.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | eluz1i 9326 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | eluzuzle 9327 |
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,
17-Jun-2018.)
|
|
|
Theorem | eluzelz 9328 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
|
|
Theorem | eluzelre 9329 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
|
|
Theorem | eluzelcn 9330 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | eluzle 9331 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
|
|
Theorem | eluz 9332 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
|
|
Theorem | uzid 9333 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
|
|
Theorem | uzn0 9334 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
|
|
Theorem | uztrn 9335 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
|
|
Theorem | uztrn2 9336 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
|
|
Theorem | uzneg 9337 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
|
|
Theorem | uzssz 9338 |
An upper set of integers is a subset of all integers. (Contributed by
NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | uzss 9339 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | uztric 9340 |
Trichotomy of the ordering relation on integers, stated in terms of upper
integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro,
25-Jun-2013.)
|
|
|
Theorem | uz11 9341 |
The upper integers function is one-to-one. (Contributed by NM,
12-Dec-2005.)
|
|
|
Theorem | eluzp1m1 9342 |
Membership in the next upper set of integers. (Contributed by NM,
12-Sep-2005.)
|
|
|
Theorem | eluzp1l 9343 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
|
|
Theorem | eluzp1p1 9344 |
Membership in the next upper set of integers. (Contributed by NM,
5-Oct-2005.)
|
|
|
Theorem | eluzaddi 9345 |
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
|
|
Theorem | eluzsubi 9346 |
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
|
|
Theorem | eluzadd 9347 |
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | eluzsub 9348 |
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | uzm1 9349 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | uznn0sub 9350 |
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4-Sep-2005.)
|
|
|
Theorem | uzin 9351 |
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24-Dec-2013.)
|
|
|
Theorem | uzp1 9352 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | nn0uz 9353 |
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
|
|
Theorem | nnuz 9354 |
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2-Sep-2005.)
|
|
|
Theorem | elnnuz 9355 |
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | elnn0uz 9356 |
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | eluz2nn 9357 |
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3-Nov-2018.)
|
|
|
Theorem | eluzge2nn0 9358 |
If an integer is greater than or equal to 2, then it is a nonnegative
integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV,
3-Nov-2018.)
|
|
|
Theorem | uzuzle23 9359 |
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, 17-Sep-2018.)
|
|
|
Theorem | eluzge3nn 9360 |
If an integer is greater than 3, then it is a positive integer.
(Contributed by Alexander van der Vekens, 17-Sep-2018.)
|
|
|
Theorem | uz3m2nn 9361 |
An integer greater than or equal to 3 decreased by 2 is a positive
integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
|
|
|
Theorem | 1eluzge0 9362 |
1 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8-Jun-2018.)
|
|
|
Theorem | 2eluzge0 9363 |
2 is an integer greater than or equal to 0. (Contributed by Alexander van
der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|
|
|
Theorem | 2eluzge1 9364 |
2 is an integer greater than or equal to 1. (Contributed by Alexander van
der Vekens, 8-Jun-2018.)
|
|
|
Theorem | uznnssnn 9365 |
The upper integers starting from a natural are a subset of the naturals.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
|
|
Theorem | raluz 9366* |
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
|
|
Theorem | raluz2 9367* |
Restricted universal quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
|
|
Theorem | rexuz 9368* |
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
|
|
Theorem | rexuz2 9369* |
Restricted existential quantification in an upper set of integers.
(Contributed by NM, 9-Sep-2005.)
|
|
|
Theorem | 2rexuz 9370* |
Double existential quantification in an upper set of integers.
(Contributed by NM, 3-Nov-2005.)
|
|
|
Theorem | peano2uz 9371 |
Second Peano postulate for an upper set of integers. (Contributed by NM,
7-Sep-2005.)
|
|
|
Theorem | peano2uzs 9372 |
Second Peano postulate for an upper set of integers. (Contributed by
Mario Carneiro, 26-Dec-2013.)
|
|
|
Theorem | peano2uzr 9373 |
Reversed second Peano axiom for upper integers. (Contributed by NM,
2-Jan-2006.)
|
|
|
Theorem | uzaddcl 9374 |
Addition closure law for an upper set of integers. (Contributed by NM,
4-Jun-2006.)
|
|
|
Theorem | nn0pzuz 9375 |
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,
3-Oct-2018.)
|
|
|
Theorem | uzind4 9376* |
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, 7-Sep-2005.)
|
|
|
Theorem | uzind4ALT 9377* |
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 9376 or
uzind4ALT 9377 may be used; see comment for nnind 8729. (Contributed by NM,
7-Sep-2005.) (New usage is discouraged.)
(Proof modification is discouraged.)
|
|
|
Theorem | uzind4s 9378* |
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, 4-Nov-2005.)
|
|
|
Theorem | uzind4s2 9379* |
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 9378 when and
must
be distinct in . (Contributed by NM,
16-Nov-2005.)
|
|
|
Theorem | uzind4i 9380* |
Induction on the upper integers that start at . The first four
give us the substitution instances we need, and the last two are the
basis and the induction step. This is a stronger version of uzind4 9376
assuming that holds unconditionally. Notice that
implies that the lower bound
is an integer
( , see eluzel2 9324). (Contributed by NM, 4-Sep-2005.)
(Revised by AV, 13-Jul-2022.)
|
|
|
Theorem | indstr 9381* |
Strong Mathematical Induction for positive integers (inference schema).
(Contributed by NM, 17-Aug-2001.)
|
|
|
Theorem | infrenegsupex 9382* |
The infimum of a set of reals is the negative of the supremum of
the negatives of its elements. (Contributed by Jim Kingdon,
14-Jan-2022.)
|
inf |
|
Theorem | supinfneg 9383* |
If a set of real numbers has a least upper bound, the set of the
negation of those numbers has a greatest lower bound. For a theorem
which is similar but only for the boundedness part, see ublbneg 9398.
(Contributed by Jim Kingdon, 15-Jan-2022.)
|
|
|
Theorem | infsupneg 9384* |
If a set of real numbers has a greatest lower bound, the set of the
negation of those numbers has a least upper bound. To go in the other
direction see supinfneg 9383. (Contributed by Jim Kingdon,
15-Jan-2022.)
|
|
|
Theorem | supminfex 9385* |
A supremum is the negation of the infimum of that set's image under
negation. (Contributed by Jim Kingdon, 14-Jan-2022.)
|
inf |
|
Theorem | eluznn0 9386 |
Membership in a nonnegative upper set of integers implies membership in
.
(Contributed by Paul Chapman, 22-Jun-2011.)
|
|
|
Theorem | eluznn 9387 |
Membership in a positive upper set of integers implies membership in
. (Contributed
by JJ, 1-Oct-2018.)
|
|
|
Theorem | eluz2b1 9388 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
|
|
Theorem | eluz2gt1 9389 |
An integer greater than or equal to 2 is greater than 1. (Contributed by
AV, 24-May-2020.)
|
|
|
Theorem | eluz2b2 9390 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
|
|
Theorem | eluz2b3 9391 |
Two ways to say "an integer greater than or equal to 2."
(Contributed by
Paul Chapman, 23-Nov-2012.)
|
|
|
Theorem | uz2m1nn 9392 |
One less than an integer greater than or equal to 2 is a positive integer.
(Contributed by Paul Chapman, 17-Nov-2012.)
|
|
|
Theorem | 1nuz2 9393 |
1 is not in . (Contributed by Paul Chapman,
21-Nov-2012.)
|
|
|
Theorem | elnn1uz2 9394 |
A positive integer is either 1 or greater than or equal to 2.
(Contributed by Paul Chapman, 17-Nov-2012.)
|
|
|
Theorem | uz2mulcl 9395 |
Closure of multiplication of integers greater than or equal to 2.
(Contributed by Paul Chapman, 26-Oct-2012.)
|
|
|
Theorem | indstr2 9396* |
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, 21-Nov-2012.)
|
|
|
Theorem | eluzdc 9397 |
Membership of an integer in an upper set of integers is decidable.
(Contributed by Jim Kingdon, 18-Apr-2020.)
|
DECID
|
|
Theorem | ublbneg 9398* |
The image under negation of a bounded-above set of reals is bounded
below. For a theorem which is similar but also adds that the bounds
need to be the tightest possible, see supinfneg 9383. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | eqreznegel 9399* |
Two ways to express the image under negation of a set of integers.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
|
|
Theorem | negm 9400* |
The image under negation of an inhabited set of reals is inhabited.
(Contributed by Jim Kingdon, 10-Apr-2020.)
|
|