![]() |
Metamath
Proof Explorer Theorem List (p. 128 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | decnncl 12701 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ โ โข ;๐ด๐ต โ โ | ||
Theorem | dec0u 12702 | Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 โ โข (;10 ยท ๐ด) = ;๐ด0 | ||
Theorem | dec0h 12703 | Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 โ โข ๐ด = ;0๐ด | ||
Theorem | numnncl2 12704 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.) |
โข ๐ โ โ & โข ๐ด โ โ โ โข ((๐ ยท ๐ด) + 0) โ โ | ||
Theorem | decnncl2 12705 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ โ โข ;๐ด0 โ โ | ||
Theorem | numlt 12706 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ & โข ๐ต < ๐ถ โ โข ((๐ ยท ๐ด) + ๐ต) < ((๐ ยท ๐ด) + ๐ถ) | ||
Theorem | numltc 12707 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ถ < ๐ & โข ๐ด < ๐ต โ โข ((๐ ยท ๐ด) + ๐ถ) < ((๐ ยท ๐ต) + ๐ท) | ||
Theorem | le9lt10 12708 | A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ด โค 9 โ โข ๐ด < ;10 | ||
Theorem | declt 12709 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ & โข ๐ต < ๐ถ โ โข ;๐ด๐ต < ;๐ด๐ถ | ||
Theorem | decltc 12710 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ถ < ;10 & โข ๐ด < ๐ต โ โข ;๐ด๐ถ < ;๐ต๐ท | ||
Theorem | declth 12711 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ถ โค 9 & โข ๐ด < ๐ต โ โข ;๐ด๐ถ < ;๐ต๐ท | ||
Theorem | decsuc 12712 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข (๐ต + 1) = ๐ถ & โข ๐ = ;๐ด๐ต โ โข (๐ + 1) = ;๐ด๐ถ | ||
Theorem | 3declth 12713 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐น โ โ0 & โข ๐ด < ๐ต & โข ๐ถ โค 9 & โข ๐ธ โค 9 โ โข ;;๐ด๐ถ๐ธ < ;;๐ต๐ท๐น | ||
Theorem | 3decltc 12714 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐น โ โ0 & โข ๐ด < ๐ต & โข ๐ถ < ;10 & โข ๐ธ < ;10 โ โข ;;๐ด๐ถ๐ธ < ;;๐ต๐ท๐น | ||
Theorem | decle 12715 | Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ต โค ๐ถ โ โข ;๐ด๐ต โค ;๐ด๐ถ | ||
Theorem | decleh 12716 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ถ โค 9 & โข ๐ด < ๐ต โ โข ;๐ด๐ถ โค ;๐ต๐ท | ||
Theorem | declei 12717 | Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ถ โค 9 โ โข ๐ถ โค ;๐ด๐ต | ||
Theorem | numlti 12718 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ถ < ๐ โ โข ๐ถ < ((๐ ยท ๐ด) + ๐ต) | ||
Theorem | declti 12719 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ถ < ;10 โ โข ๐ถ < ;๐ด๐ต | ||
Theorem | decltdi 12720 | Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ถ โค 9 โ โข ๐ถ < ;๐ด๐ต | ||
Theorem | numsucc 12721 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ = (๐ + 1) & โข ๐ด โ โ0 & โข (๐ด + 1) = ๐ต & โข ๐ = ((๐ ยท ๐ด) + ๐) โ โข (๐ + 1) = ((๐ ยท ๐ต) + 0) | ||
Theorem | decsucc 12722 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ๐ด โ โ0 & โข (๐ด + 1) = ๐ต & โข ๐ = ;๐ด9 โ โข (๐ + 1) = ;๐ต0 | ||
Theorem | 1e0p1 12723 | The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข 1 = (0 + 1) | ||
Theorem | dec10p 12724 | Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (;10 + ๐ด) = ;1๐ด | ||
Theorem | numma 12725 | Perform a multiply-add of two decimal integers ๐ and ๐ against a fixed multiplicand ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ = ((๐ ยท ๐ถ) + ๐ท) & โข ๐ โ โ0 & โข ((๐ด ยท ๐) + ๐ถ) = ๐ธ & โข ((๐ต ยท ๐) + ๐ท) = ๐น โ โข ((๐ ยท ๐) + ๐) = ((๐ ยท ๐ธ) + ๐น) | ||
Theorem | nummac 12726 | Perform a multiply-add of two decimal integers ๐ and ๐ against a fixed multiplicand ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ = ((๐ ยท ๐ถ) + ๐ท) & โข ๐ โ โ0 & โข ๐น โ โ0 & โข ๐บ โ โ0 & โข ((๐ด ยท ๐) + (๐ถ + ๐บ)) = ๐ธ & โข ((๐ต ยท ๐) + ๐ท) = ((๐ ยท ๐บ) + ๐น) โ โข ((๐ ยท ๐) + ๐) = ((๐ ยท ๐ธ) + ๐น) | ||
Theorem | numma2c 12727 | Perform a multiply-add of two decimal integers ๐ and ๐ against a fixed multiplicand ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ = ((๐ ยท ๐ถ) + ๐ท) & โข ๐ โ โ0 & โข ๐น โ โ0 & โข ๐บ โ โ0 & โข ((๐ ยท ๐ด) + (๐ถ + ๐บ)) = ๐ธ & โข ((๐ ยท ๐ต) + ๐ท) = ((๐ ยท ๐บ) + ๐น) โ โข ((๐ ยท ๐) + ๐) = ((๐ ยท ๐ธ) + ๐น) | ||
Theorem | numadd 12728 | Add two decimal integers ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ = ((๐ ยท ๐ถ) + ๐ท) & โข (๐ด + ๐ถ) = ๐ธ & โข (๐ต + ๐ท) = ๐น โ โข (๐ + ๐) = ((๐ ยท ๐ธ) + ๐น) | ||
Theorem | numaddc 12729 | Add two decimal integers ๐ and ๐ (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ = ((๐ ยท ๐ถ) + ๐ท) & โข ๐น โ โ0 & โข ((๐ด + ๐ถ) + 1) = ๐ธ & โข (๐ต + ๐ท) = ((๐ ยท 1) + ๐น) โ โข (๐ + ๐) = ((๐ ยท ๐ธ) + ๐น) | ||
Theorem | nummul1c 12730 | The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ0 & โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ = ((๐ ยท ๐ด) + ๐ต) & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ((๐ด ยท ๐) + ๐ธ) = ๐ถ & โข (๐ต ยท ๐) = ((๐ ยท ๐ธ) + ๐ท) โ โข (๐ ยท ๐) = ((๐ ยท ๐ถ) + ๐ท) | ||
Theorem | nummul2c 12731 | 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 12732 | 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 12733 | 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 12734 | 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 12735 | 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 12736 | 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 12737 | 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 12738 | 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 12739 | 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 12740 | 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 12741 | Add two numerals ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ต + ๐) = ๐ถ โ โข (๐ + ๐) = ;๐ด๐ถ | ||
Theorem | decaddci 12742 | Add two numerals ๐ and ๐ (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข ๐ = ;๐ด๐ต & โข (๐ด + 1) = ๐ท & โข ๐ถ โ โ0 & โข (๐ต + ๐) = ;1๐ถ โ โข (๐ + ๐) = ;๐ท๐ถ | ||
Theorem | decaddci2 12743 | 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 12744 | 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 12745 | 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 12746 | 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 12747 | 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 12748 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
โข ๐ โ โ0 & โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข (๐ ยท ;๐ด๐ต) = ;(๐ ยท ๐ด)(๐ ยท ๐ต) | ||
Theorem | 11multnc 12749 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
โข ๐ โ โ0 โ โข (๐ ยท ;11) = ;๐๐ | ||
Theorem | decmul10add 12750 | 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 12751 | Lemma for 6p5e11 12754 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ท โ โ0 & โข ๐ธ โ โ0 & โข ๐ต = (๐ท + 1) & โข ๐ถ = (๐ธ + 1) & โข (๐ด + ๐ท) = ;1๐ธ โ โข (๐ด + ๐ต) = ;1๐ถ | ||
Theorem | 5p5e10 12752 | 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 12753 | 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 12754 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (6 + 5) = ;11 | ||
Theorem | 6p6e12 12755 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 + 6) = ;12 | ||
Theorem | 7p3e10 12756 | 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 12757 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (7 + 4) = ;11 | ||
Theorem | 7p5e12 12758 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 + 5) = ;12 | ||
Theorem | 7p6e13 12759 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 + 6) = ;13 | ||
Theorem | 7p7e14 12760 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 + 7) = ;14 | ||
Theorem | 8p2e10 12761 | 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 12762 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (8 + 3) = ;11 | ||
Theorem | 8p4e12 12763 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 4) = ;12 | ||
Theorem | 8p5e13 12764 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 5) = ;13 | ||
Theorem | 8p6e14 12765 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 6) = ;14 | ||
Theorem | 8p7e15 12766 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 7) = ;15 | ||
Theorem | 8p8e16 12767 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 + 8) = ;16 | ||
Theorem | 9p2e11 12768 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (9 + 2) = ;11 | ||
Theorem | 9p3e12 12769 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 3) = ;12 | ||
Theorem | 9p4e13 12770 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 4) = ;13 | ||
Theorem | 9p5e14 12771 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 5) = ;14 | ||
Theorem | 9p6e15 12772 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 6) = ;15 | ||
Theorem | 9p7e16 12773 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 7) = ;16 | ||
Theorem | 9p8e17 12774 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 8) = ;17 | ||
Theorem | 9p9e18 12775 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (9 + 9) = ;18 | ||
Theorem | 10p10e20 12776 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (;10 + ;10) = ;20 | ||
Theorem | 10m1e9 12777 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
โข (;10 โ 1) = 9 | ||
Theorem | 4t3lem 12778 | Lemma for 4t3e12 12779 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ = (๐ต + 1) & โข (๐ด ยท ๐ต) = ๐ท & โข (๐ท + ๐ด) = ๐ธ โ โข (๐ด ยท ๐ถ) = ๐ธ | ||
Theorem | 4t3e12 12779 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (4 ยท 3) = ;12 | ||
Theorem | 4t4e16 12780 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (4 ยท 4) = ;16 | ||
Theorem | 5t2e10 12781 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
โข (5 ยท 2) = ;10 | ||
Theorem | 5t3e15 12782 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (5 ยท 3) = ;15 | ||
Theorem | 5t4e20 12783 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (5 ยท 4) = ;20 | ||
Theorem | 5t5e25 12784 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (5 ยท 5) = ;25 | ||
Theorem | 6t2e12 12785 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 ยท 2) = ;12 | ||
Theorem | 6t3e18 12786 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 ยท 3) = ;18 | ||
Theorem | 6t4e24 12787 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (6 ยท 4) = ;24 | ||
Theorem | 6t5e30 12788 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (6 ยท 5) = ;30 | ||
Theorem | 6t6e36 12789 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (6 ยท 6) = ;36 | ||
Theorem | 7t2e14 12790 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 2) = ;14 | ||
Theorem | 7t3e21 12791 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 3) = ;21 | ||
Theorem | 7t4e28 12792 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 4) = ;28 | ||
Theorem | 7t5e35 12793 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 5) = ;35 | ||
Theorem | 7t6e42 12794 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 6) = ;42 | ||
Theorem | 7t7e49 12795 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (7 ยท 7) = ;49 | ||
Theorem | 8t2e16 12796 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 2) = ;16 | ||
Theorem | 8t3e24 12797 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 3) = ;24 | ||
Theorem | 8t4e32 12798 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข (8 ยท 4) = ;32 | ||
Theorem | 8t5e40 12799 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (8 ยท 5) = ;40 | ||
Theorem | 8t6e48 12800 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
โข (8 ยท 6) = ;48 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |