Theorem List for Intuitionistic Logic Explorer - 9401-9500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 9p4e13 9401 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p5e14 9402 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p6e15 9403 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p7e16 9404 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p8e17 9405 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p9e18 9406 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 10p10e20 9407 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
; ; ; |
|
Theorem | 10m1e9 9408 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
; |
|
Theorem | 4t3lem 9409 |
Lemma for 4t3e12 9410 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
|
|
Theorem | 4t3e12 9410 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 4t4e16 9411 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 5t2e10 9412 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
; |
|
Theorem | 5t3e15 9413 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 5t4e20 9414 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 5t5e25 9415 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 6t2e12 9416 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t3e18 9417 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t4e24 9418 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t5e30 9419 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 6t6e36 9420 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 7t2e14 9421 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t3e21 9422 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t4e28 9423 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t5e35 9424 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t6e42 9425 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t7e49 9426 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t2e16 9427 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t3e24 9428 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t4e32 9429 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t5e40 9430 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 8t6e48 9431 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
; |
|
Theorem | 8t7e56 9432 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t8e64 9433 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t2e18 9434 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t3e27 9435 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t4e36 9436 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t5e45 9437 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t6e54 9438 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t7e63 9439 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t8e72 9440 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t9e81 9441 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t11e99 9442 |
9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
; ; |
|
Theorem | 9lt10 9443 |
9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
; |
|
Theorem | 8lt10 9444 |
8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised
by AV, 8-Sep-2021.)
|
; |
|
Theorem | 7lt10 9445 |
7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 6lt10 9446 |
6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 5lt10 9447 |
5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 4lt10 9448 |
4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 3lt10 9449 |
3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 2lt10 9450 |
2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.)
(Revised by AV, 8-Sep-2021.)
|
; |
|
Theorem | 1lt10 9451 |
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 9452 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin2 9453 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin3 9454 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | halfthird 9455 |
Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
|
|
|
Theorem | 5recm6rec 9456 |
One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
|
; |
|
4.4.11 Upper sets of integers
|
|
Syntax | cuz 9457 |
Extend class notation with the upper integer function.
Read " " as "the
set of integers greater than or equal to
."
|
|
|
Definition | df-uz 9458* |
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 9459 for its
value, uzssz 9476 for its relationship to , nnuz 9492
and nn0uz 9491 for
its relationships to and , and eluz1 9461 and eluz2 9463 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | uzval 9459* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | uzf 9460 |
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 9461 |
Membership in the upper set of integers starting at .
(Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | eluzel2 9462 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | eluz2 9463 |
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 9464 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | eluzuzle 9465 |
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 9466 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
|
|
Theorem | eluzelre 9467 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
|
|
Theorem | eluzelcn 9468 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | eluzle 9469 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
|
|
Theorem | eluz 9470 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
|
|
Theorem | uzid 9471 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
|
|
Theorem | uzn0 9472 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
|
|
Theorem | uztrn 9473 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
|
|
Theorem | uztrn2 9474 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
|
|
Theorem | uzneg 9475 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
|
|
Theorem | uzssz 9476 |
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 9477 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | uztric 9478 |
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 9479 |
The upper integers function is one-to-one. (Contributed by NM,
12-Dec-2005.)
|
|
|
Theorem | eluzp1m1 9480 |
Membership in the next upper set of integers. (Contributed by NM,
12-Sep-2005.)
|
|
|
Theorem | eluzp1l 9481 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
|
|
Theorem | eluzp1p1 9482 |
Membership in the next upper set of integers. (Contributed by NM,
5-Oct-2005.)
|
|
|
Theorem | eluzaddi 9483 |
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
|
|
Theorem | eluzsubi 9484 |
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
|
|
Theorem | eluzadd 9485 |
Membership in a later upper set of integers. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
|
|
Theorem | eluzsub 9486 |
Membership in an earlier upper set of integers. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | uzm1 9487 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | uznn0sub 9488 |
The nonnegative difference of integers is a nonnegative integer.
(Contributed by NM, 4-Sep-2005.)
|
|
|
Theorem | uzin 9489 |
Intersection of two upper intervals of integers. (Contributed by Mario
Carneiro, 24-Dec-2013.)
|
|
|
Theorem | uzp1 9490 |
Choices for an element of an upper interval of integers. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | nn0uz 9491 |
Nonnegative integers expressed as an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
|
|
Theorem | nnuz 9492 |
Positive integers expressed as an upper set of integers. (Contributed by
NM, 2-Sep-2005.)
|
|
|
Theorem | elnnuz 9493 |
A positive integer expressed as a member of an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | elnn0uz 9494 |
A nonnegative integer expressed as a member an upper set of integers.
(Contributed by NM, 6-Jun-2006.)
|
|
|
Theorem | eluz2nn 9495 |
An integer is greater than or equal to 2 is a positive integer.
(Contributed by AV, 3-Nov-2018.)
|
|
|
Theorem | eluz4eluz2 9496 |
An integer greater than or equal to 4 is an integer greater than or equal
to 2. (Contributed by AV, 30-May-2023.)
|
|
|
Theorem | eluz4nn 9497 |
An integer greater than or equal to 4 is a positive integer. (Contributed
by AV, 30-May-2023.)
|
|
|
Theorem | eluzge2nn0 9498 |
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 | eluz2n0 9499 |
An integer greater than or equal to 2 is not 0. (Contributed by AV,
25-May-2020.)
|
|
|
Theorem | uzuzle23 9500 |
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.)
|
|