Home | Metamath
Proof Explorer Theorem List (p. 127 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nummul2c 12601 | The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ((๐ ยท ๐ด) + ๐ธ) = ๐ถ & โข (๐ ยท ๐ต) = ((๐ ยท ๐ธ) + ๐ท) โ โข (๐ ยท ๐) = ((๐ ยท ๐ถ) + ๐ท) | ||
Theorem | decma 12602 | Perform a multiply-add of two numerals ๐ and ๐ against a fixed multiplicand ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ = ;๐ถ๐ท & โข ๐ โ โ0 & โข ((๐ด ยท ๐) + ๐ถ) = ๐ธ & โข ((๐ต ยท ๐) + ๐ท) = ๐น โ โข ((๐ ยท ๐) + ๐) = ;๐ธ๐น | ||
Theorem | decmac 12603 | Perform a multiply-add of two numerals ๐ and ๐ against a fixed multiplicand ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ = ;๐ถ๐ท & โข ๐ โ โ0 & โข ๐น โ โ0 & โข ๐บ โ โ0 & โข ((๐ด ยท ๐) + (๐ถ + ๐บ)) = ๐ธ & โข ((๐ต ยท ๐) + ๐ท) = ;๐บ๐น โ โข ((๐ ยท ๐) + ๐) = ;๐ธ๐น | ||
Theorem | decma2c 12604 | Perform a multiply-add of two numerals ๐ and ๐ against a fixed multiplier ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ = ;๐ถ๐ท & โข ๐ โ โ0 & โข ๐น โ โ0 & โข ๐บ โ โ0 & โข ((๐ ยท ๐ด) + (๐ถ + ๐บ)) = ๐ธ & โข ((๐ ยท ๐ต) + ๐ท) = ;๐บ๐น โ โข ((๐ ยท ๐) + ๐) = ;๐ธ๐น | ||
Theorem | decadd 12605 | Add two numerals ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ = ;๐ถ๐ท & โข (๐ด + ๐ถ) = ๐ธ & โข (๐ต + ๐ท) = ๐น โ โข (๐ + ๐) = ;๐ธ๐น | ||
Theorem | decaddc 12606 | Add two numerals ๐ and ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ = ;๐ถ๐ท & โข ((๐ด + ๐ถ) + 1) = ๐ธ & โข ๐น โ โ0 & โข (๐ต + ๐ท) = ;1๐น โ โข (๐ + ๐) = ;๐ธ๐น | ||
Theorem | decaddc2 12607 | Add two numerals ๐ and ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ = ;๐ถ๐ท & โข ((๐ด + ๐ถ) + 1) = ๐ธ & โข (๐ต + ๐ท) = ;10 โ โข (๐ + ๐) = ;๐ธ0 | ||
Theorem | decrmanc 12608 | Perform a multiply-add of two numerals ๐ and ๐ against a fixed multiplicand ๐ (no carry). (Contributed by AV, 16-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ โ โ0 & โข (๐ด ยท ๐) = ๐ธ & โข ((๐ต ยท ๐) + ๐) = ๐น โ โข ((๐ ยท ๐) + ๐) = ;๐ธ๐น | ||
Theorem | decrmac 12609 | Perform a multiply-add of two numerals ๐ and ๐ against a fixed multiplicand ๐ (with carry). (Contributed by AV, 16-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ โ โ0 & โข ๐น โ โ0 & โข ๐บ โ โ0 & โข ((๐ด ยท ๐) + ๐บ) = ๐ธ & โข ((๐ต ยท ๐) + ๐) = ;๐บ๐น โ โข ((๐ ยท ๐) + ๐) = ;๐ธ๐น | ||
Theorem | decaddm10 12610 | The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข (;๐ด0 + ;๐ต0) = ;(๐ด + ๐ต)0 | ||
Theorem | decaddi 12611 | Add two numerals ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ต + ๐) = ๐ถ โ โข (๐ + ๐) = ;๐ด๐ถ | ||
Theorem | decaddci 12612 | Add two numerals ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ด + 1) = ๐ท & โข ๐ถ โ โ0 & โข (๐ต + ๐) = ;1๐ถ โ โข (๐ + ๐) = ;๐ท๐ถ | ||
Theorem | decaddci2 12613 | Add two numerals ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ด + 1) = ๐ท & โข (๐ต + ๐) = ;10 โ โข (๐ + ๐) = ;๐ท0 | ||
Theorem | decsubi 12614 | Difference between a numeral ๐ and a nonnegative integer ๐ (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ด + 1) = ๐ท & โข (๐ต โ ๐) = ๐ถ โ โข (๐ โ ๐) = ;๐ด๐ถ | ||
Theorem | decmul1 12615 | The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) Remove hypothesis ๐ท โ โ0. (Revised by Steven Nguyen, 7-Dec-2022.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ด ยท ๐) = ๐ถ & โข (๐ต ยท ๐) = ๐ท โ โข (๐ ยท ๐) = ;๐ถ๐ท | ||
Theorem | decmul1c 12616 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ((๐ด ยท ๐) + ๐ธ) = ๐ถ & โข (๐ต ยท ๐) = ;๐ธ๐ท โ โข (๐ ยท ๐) = ;๐ถ๐ท | ||
Theorem | decmul2c 12617 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ = ;๐ด๐ต & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ((๐ ยท ๐ด) + ๐ธ) = ๐ถ & โข (๐ ยท ๐ต) = ;๐ธ๐ท โ โข (๐ ยท ๐) = ;๐ถ๐ท | ||
Theorem | decmulnc 12618 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข (๐ ยท ;๐ด๐ต) = ;(๐ ยท ๐ด)(๐ ยท ๐ต) | ||
Theorem | 11multnc 12619 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
โข ๐ โ โ0 โ โข (๐ ยท ;11) = ;๐๐ | ||
Theorem | decmul10add 12620 | A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ธ = (๐ ยท ๐ด) & โข ๐น = (๐ ยท ๐ต) โ โข (๐ ยท ;๐ด๐ต) = (;๐ธ0 + ๐น) | ||
Theorem | 6p5lem 12621 | Lemma for 6p5e11 12624 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐ต = (๐ท + 1) & โข ๐ถ = (๐ธ + 1) & โข (๐ด + ๐ท) = ;1๐ธ โ โข (๐ด + ๐ต) = ;1๐ถ | ||
Theorem | 5p5e10 12622 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
โข (5 + 5) = ;10 | ||
Theorem | 6p4e10 12623 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
โข (6 + 4) = ;10 | ||
Theorem | 6p5e11 12624 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (6 + 5) = ;11 | ||
Theorem | 6p6e12 12625 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 + 6) = ;12 | ||
Theorem | 7p3e10 12626 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
โข (7 + 3) = ;10 | ||
Theorem | 7p4e11 12627 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (7 + 4) = ;11 | ||
Theorem | 7p5e12 12628 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 + 5) = ;12 | ||
Theorem | 7p6e13 12629 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 + 6) = ;13 | ||
Theorem | 7p7e14 12630 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 + 7) = ;14 | ||
Theorem | 8p2e10 12631 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
โข (8 + 2) = ;10 | ||
Theorem | 8p3e11 12632 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (8 + 3) = ;11 | ||
Theorem | 8p4e12 12633 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 4) = ;12 | ||
Theorem | 8p5e13 12634 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 5) = ;13 | ||
Theorem | 8p6e14 12635 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 6) = ;14 | ||
Theorem | 8p7e15 12636 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 7) = ;15 | ||
Theorem | 8p8e16 12637 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 8) = ;16 | ||
Theorem | 9p2e11 12638 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (9 + 2) = ;11 | ||
Theorem | 9p3e12 12639 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 3) = ;12 | ||
Theorem | 9p4e13 12640 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 4) = ;13 | ||
Theorem | 9p5e14 12641 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 5) = ;14 | ||
Theorem | 9p6e15 12642 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 6) = ;15 | ||
Theorem | 9p7e16 12643 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 7) = ;16 | ||
Theorem | 9p8e17 12644 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 8) = ;17 | ||
Theorem | 9p9e18 12645 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 9) = ;18 | ||
Theorem | 10p10e20 12646 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (;10 + ;10) = ;20 | ||
Theorem | 10m1e9 12647 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
โข (;10 โ 1) = 9 | ||
Theorem | 4t3lem 12648 | Lemma for 4t3e12 12649 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ = (๐ต + 1) & โข (๐ด ยท ๐ต) = ๐ท & โข (๐ท + ๐ด) = ๐ธ โ โข (๐ด ยท ๐ถ) = ๐ธ | ||
Theorem | 4t3e12 12649 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (4 ยท 3) = ;12 | ||
Theorem | 4t4e16 12650 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (4 ยท 4) = ;16 | ||
Theorem | 5t2e10 12651 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
โข (5 ยท 2) = ;10 | ||
Theorem | 5t3e15 12652 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (5 ยท 3) = ;15 | ||
Theorem | 5t4e20 12653 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (5 ยท 4) = ;20 | ||
Theorem | 5t5e25 12654 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (5 ยท 5) = ;25 | ||
Theorem | 6t2e12 12655 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 ยท 2) = ;12 | ||
Theorem | 6t3e18 12656 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 ยท 3) = ;18 | ||
Theorem | 6t4e24 12657 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 ยท 4) = ;24 | ||
Theorem | 6t5e30 12658 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (6 ยท 5) = ;30 | ||
Theorem | 6t6e36 12659 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (6 ยท 6) = ;36 | ||
Theorem | 7t2e14 12660 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 2) = ;14 | ||
Theorem | 7t3e21 12661 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 3) = ;21 | ||
Theorem | 7t4e28 12662 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 4) = ;28 | ||
Theorem | 7t5e35 12663 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 5) = ;35 | ||
Theorem | 7t6e42 12664 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 6) = ;42 | ||
Theorem | 7t7e49 12665 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 7) = ;49 | ||
Theorem | 8t2e16 12666 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 2) = ;16 | ||
Theorem | 8t3e24 12667 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 3) = ;24 | ||
Theorem | 8t4e32 12668 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 4) = ;32 | ||
Theorem | 8t5e40 12669 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (8 ยท 5) = ;40 | ||
Theorem | 8t6e48 12670 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (8 ยท 6) = ;48 | ||
Theorem | 8t7e56 12671 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 7) = ;56 | ||
Theorem | 8t8e64 12672 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 8) = ;64 | ||
Theorem | 9t2e18 12673 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 2) = ;18 | ||
Theorem | 9t3e27 12674 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 3) = ;27 | ||
Theorem | 9t4e36 12675 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 4) = ;36 | ||
Theorem | 9t5e45 12676 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 5) = ;45 | ||
Theorem | 9t6e54 12677 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 6) = ;54 | ||
Theorem | 9t7e63 12678 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 7) = ;63 | ||
Theorem | 9t8e72 12679 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 8) = ;72 | ||
Theorem | 9t9e81 12680 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 ยท 9) = ;81 | ||
Theorem | 9t11e99 12681 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
โข (9 ยท ;11) = ;99 | ||
Theorem | 9lt10 12682 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
โข 9 < ;10 | ||
Theorem | 8lt10 12683 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
โข 8 < ;10 | ||
Theorem | 7lt10 12684 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 7 < ;10 | ||
Theorem | 6lt10 12685 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 6 < ;10 | ||
Theorem | 5lt10 12686 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 5 < ;10 | ||
Theorem | 4lt10 12687 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 4 < ;10 | ||
Theorem | 3lt10 12688 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 3 < ;10 | ||
Theorem | 2lt10 12689 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 2 < ;10 | ||
Theorem | 1lt10 12690 | 1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
โข 1 < ;10 | ||
Theorem | decbin0 12691 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 โ โข (4 ยท ๐ด) = (2 ยท (2 ยท ๐ด)) | ||
Theorem | decbin2 12692 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 โ โข ((4 ยท ๐ด) + 2) = (2 ยท ((2 ยท ๐ด) + 1)) | ||
Theorem | decbin3 12693 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 โ โข ((4 ยท ๐ด) + 3) = ((2 ยท ((2 ยท ๐ด) + 1)) + 1) | ||
Theorem | halfthird 12694 | Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข ((1 / 2) โ (1 / 3)) = (1 / 6) | ||
Theorem | 5recm6rec 12695 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
โข ((1 / 5) โ (1 / 6)) = (1 / ;30) | ||
Syntax | cuz 12696 | Extend class notation with the upper integer function. Read "โคโฅโ๐ " as "the set of integers greater than or equal to ๐". |
class โคโฅ | ||
Definition | df-uz 12697* | 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 12698 for its value, uzssz 12717 for its relationship to โค, nnuz 12735 and nn0uz 12734 for its relationships to โ and โ0, and eluz1 12700 and eluz2 12702 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
โข โคโฅ = (๐ โ โค โฆ {๐ โ โค โฃ ๐ โค ๐}) | ||
Theorem | uzval 12698* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
โข (๐ โ โค โ (โคโฅโ๐) = {๐ โ โค โฃ ๐ โค ๐}) | ||
Theorem | uzf 12699 | The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.) |
โข โคโฅ:โคโถ๐ซ โค | ||
Theorem | eluz1 12700 | Membership in the upper set of integers starting at ๐. (Contributed by NM, 5-Sep-2005.) |
โข (๐ โ โค โ (๐ โ (โคโฅโ๐) โ (๐ โ โค โง ๐ โค ๐))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |