Theorem List for Intuitionistic Logic Explorer - 8401-8500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | numadd 8401 |
Add two decimal integers and (no
carry). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | numaddc 8402 |
Add two decimal integers and (with
carry). (Contributed
by Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | nummul1c 8403 |
The product of a decimal integer with a number. (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
|
|
Theorem | nummul2c 8404 |
The product of a decimal integer with a number (with carry).
(Contributed by Mario Carneiro, 18-Feb-2014.)
|
|
|
Theorem | decma 8405 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(no carry). (Contributed by Mario Carneiro,
18-Feb-2014.)
|
; ;
; |
|
Theorem | decmac 8406 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(with carry). (Contributed by Mario Carneiro,
18-Feb-2014.)
|
; ;
;
; |
|
Theorem | decma2c 8407 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(with carry). (Contributed by Mario Carneiro,
18-Feb-2014.)
|
; ;
;
; |
|
Theorem | decadd 8408 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
; ;
; |
|
Theorem | decaddc 8409 |
Add two numerals and
(with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
; ;
;
; |
|
Theorem | decaddc2 8410 |
Add two numerals and
(with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
; ;
; |
|
Theorem | decaddi 8411 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;
; |
|
Theorem | decaddci 8412 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;
;
; |
|
Theorem | decaddci2 8413 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;
; |
|
Theorem | decmul1c 8414 |
The product of a numeral with a number. (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;
;
; |
|
Theorem | decmul2c 8415 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
;
;
; |
|
Theorem | 6p5lem 8416 |
Lemma for 6p5e11 8417 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
;
; |
|
Theorem | 6p5e11 8417 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6p6e12 8418 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p4e11 8419 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p5e12 8420 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p6e13 8421 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7p7e14 8422 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p3e11 8423 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p4e12 8424 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p5e13 8425 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p6e14 8426 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p7e15 8427 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8p8e16 8428 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p2e11 8429 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p3e12 8430 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p4e13 8431 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p5e14 8432 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p6e15 8433 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p7e16 8434 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p8e17 8435 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9p9e18 8436 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 10p10e20 8437 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 4t3lem 8438 |
Lemma for 4t3e12 8439 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
|
|
Theorem | 4t3e12 8439 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 4t4e16 8440 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 5t3e15 8441 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 5t4e20 8442 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 5t5e25 8443 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t2e12 8444 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t3e18 8445 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t4e24 8446 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t5e30 8447 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 6t6e36 8448 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t2e14 8449 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t3e21 8450 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t4e28 8451 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t5e35 8452 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t6e42 8453 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 7t7e49 8454 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t2e16 8455 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t3e24 8456 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t4e32 8457 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t5e40 8458 |
8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t6e48 8459 |
8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t7e56 8460 |
8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 8t8e64 8461 |
8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t2e18 8462 |
9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t3e27 8463 |
9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t4e36 8464 |
9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t5e45 8465 |
9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t6e54 8466 |
9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t7e63 8467 |
9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t8e72 8468 |
9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | 9t9e81 8469 |
9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
; |
|
Theorem | decbin0 8470 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin2 8471 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
Theorem | decbin3 8472 |
Decompose base 4 into base 2. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
|
|
3.4.10 Upper sets of integers
|
|
Syntax | cuz 8473 |
Extend class notation with the upper integer function.
Read " " as "the
set of integers greater than or equal to
."
|
|
|
Definition | df-uz 8474* |
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 8475 for its
value, uzssz 8492 for its relationship to , nnuz 8508
and nn0uz 8507 for
its relationships to and , and eluz1 8477 and eluz2 8479 for
its membership relations. (Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | uzval 8475* |
The value of the upper integers function. (Contributed by NM,
5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | uzf 8476 |
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 8477 |
Membership in the upper set of integers starting at .
(Contributed by NM, 5-Sep-2005.)
|
|
|
Theorem | eluzel2 8478 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | eluz2 8479 |
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 8480 |
Membership in an upper set of integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | eluzuzle 8481 |
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 8482 |
A member of an upper set of integers is an integer. (Contributed by NM,
6-Sep-2005.)
|
|
|
Theorem | eluzelre 8483 |
A member of an upper set of integers is a real. (Contributed by Mario
Carneiro, 31-Aug-2013.)
|
|
|
Theorem | eluzelcn 8484 |
A member of an upper set of integers is a complex number. (Contributed by
Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | eluzle 8485 |
Implication of membership in an upper set of integers. (Contributed by
NM, 6-Sep-2005.)
|
|
|
Theorem | eluz 8486 |
Membership in an upper set of integers. (Contributed by NM,
2-Oct-2005.)
|
|
|
Theorem | uzid 8487 |
Membership of the least member in an upper set of integers. (Contributed
by NM, 2-Sep-2005.)
|
|
|
Theorem | uzn0 8488 |
The upper integers are all nonempty. (Contributed by Mario Carneiro,
16-Jan-2014.)
|
|
|
Theorem | uztrn 8489 |
Transitive law for sets of upper integers. (Contributed by NM,
20-Sep-2005.)
|
|
|
Theorem | uztrn2 8490 |
Transitive law for sets of upper integers. (Contributed by Mario
Carneiro, 26-Dec-2013.)
|
|
|
Theorem | uzneg 8491 |
Contraposition law for upper integers. (Contributed by NM,
28-Nov-2005.)
|
|
|
Theorem | uzssz 8492 |
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 8493 |
Subset relationship for two sets of upper integers. (Contributed by NM,
5-Sep-2005.)
|
|
|
Theorem | uztric 8494 |
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 8495 |
The upper integers function is one-to-one. (Contributed by NM,
12-Dec-2005.)
|
|
|
Theorem | eluzp1m1 8496 |
Membership in the next upper set of integers. (Contributed by NM,
12-Sep-2005.)
|
|
|
Theorem | eluzp1l 8497 |
Strict ordering implied by membership in the next upper set of integers.
(Contributed by NM, 12-Sep-2005.)
|
|
|
Theorem | eluzp1p1 8498 |
Membership in the next upper set of integers. (Contributed by NM,
5-Oct-2005.)
|
|
|
Theorem | eluzaddi 8499 |
Membership in a later upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
|
|
Theorem | eluzsubi 8500 |
Membership in an earlier upper set of integers. (Contributed by Paul
Chapman, 22-Nov-2007.)
|
|