![]() |
Metamath
Proof Explorer Theorem List (p. 117 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-27775) |
![]() (27776-29300) |
![]() (29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 6p5e11OLD 11601 | Obsolete proof of 6p5e11 11600 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6p6e12 11602 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p3e10 11603 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p3e10bOLD 11604 | Obsolete proof of 7p3e10 11603 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p4e11 11605 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p4e11OLD 11606 | Obsolete proof of 7p4e11 11605 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p5e12 11607 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p6e13 11608 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7p7e14 11609 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p2e10 11610 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p2e10bOLD 11611 | Obsolete proof of 8p2e10 11610 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p3e11 11612 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p3e11OLD 11613 | Obsolete proof of 8p3e11 11612 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p4e12 11614 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p5e13 11615 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p6e14 11616 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p7e15 11617 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8p8e16 11618 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p2e11 11619 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p2e11OLD 11620 | Obsolete proof of 9p2e11 11619 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p3e12 11621 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p4e13 11622 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p5e14 11623 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p6e15 11624 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p7e16 11625 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p8e17 11626 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9p9e18 11627 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 10p10e20 11628 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 10p10e20OLD 11629 | Obsolete version of 10p10e20 11628 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 10m1e9 11630 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4t3lem 11631 | Lemma for 4t3e12 11632 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4t3e12 11632 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4t4e16 11633 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t2e10 11634 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t3e15 11635 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t3e15OLD 11636 | Obsolete proof of 5t3e15 11635 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t4e20 11637 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t4e20OLD 11638 | Obsolete proof of 5t4e20 11637 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t5e25 11639 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5t5e25OLD 11640 | Obsolete proof of 5t5e25 11639 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t2e12 11641 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t3e18 11642 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t4e24 11643 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t5e30 11644 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t5e30OLD 11645 | Obsolete proof of 6t5e30 11644 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t6e36 11646 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6t6e36OLD 11647 | Obsolete proof of 6t6e36 11646 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7t2e14 11648 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7t3e21 11649 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7t4e28 11650 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7t5e35 11651 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7t6e42 11652 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7t7e49 11653 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t2e16 11654 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t3e24 11655 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t4e32 11656 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t5e40 11657 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t5e40OLD 11658 | Obsolete proof of 8t5e40 11657 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t6e48 11659 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t6e48OLD 11660 | Obsolete proof of 8t6e48 11659 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t7e56 11661 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8t8e64 11662 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t2e18 11663 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t3e27 11664 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t4e36 11665 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t5e45 11666 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t6e54 11667 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t7e63 11668 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t8e72 11669 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t9e81 11670 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t11e99 11671 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9t11e99OLD 11672 | Obsolete proof of 9t11e99 11671 as of 6-Sep-2021. (Contributed by AV, 14-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 9lt10 11673 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 8lt10 11674 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 7lt10 11675 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 6lt10 11676 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5lt10 11677 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 4lt10 11678 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 3lt10 11679 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 2lt10 11680 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
![]() ![]() ![]() ![]() ![]() | ||
Theorem | 1lt10 11681 | 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 11682 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | decbin2 11683 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | decbin3 11684 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | halfthird 11685 | Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | 5recm6rec 11686 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Syntax | cuz 11687 |
Extend class notation with the upper integer function.
Read "![]() ![]() ![]() ![]() |
![]() ![]() | ||
Definition | df-uz 11688* |
Define a function whose value at ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | uzval 11689* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | uzf 11690 | 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 11691 |
Membership in the upper set of integers starting at ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluzel2 11692 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluz2 11693 |
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 ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluzmn 11694 | Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluz1i 11695 | Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluzuzle 11696 | 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 11697 | A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluzelre 11698 | A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluzelcn 11699 | A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | ||
Theorem | eluzle 11700 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |