Home | Metamath
Proof Explorer Theorem List (p. 116 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | deceq1OLD 11501 | Obsolete proof of deceq1 11500 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | deceq2 11502 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | deceq2OLD 11503 | Obsolete proof of deceq1 11500 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | deceq1i 11504 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
; ; | ||
Theorem | deceq2i 11505 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
; ; | ||
Theorem | deceq12i 11506 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
; ; | ||
Theorem | numnncl 11507 | Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | num0u 11508 | Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | num0h 11509 | Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | numcl 11510 | Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | numsuc 11511 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | deccl 11512 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | decclOLD 11513 | Obsolete proof of deccl 11512 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | 10nn 11514 | 10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | 10pos 11515 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) |
; | ||
Theorem | 10nn0 11516 | 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | 10re 11517 | The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) |
; | ||
Theorem | decnncl 11518 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | decnnclOLD 11519 | Obsolete proof of decnncl 11518 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | dec0u 11520 | Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | dec0uOLD 11521 | Obsolete version of dec0u 11520 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | dec0h 11522 | Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | dec0hOLD 11523 | Obsolete proof of dec0h 11522 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | numnncl2 11524 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.) |
Theorem | decnncl2 11525 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | decnncl2OLD 11526 | Obsolete proof of decnncl2 11525 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | numlt 11527 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | numltc 11528 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | le9lt10 11529 | A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021.) |
; | ||
Theorem | declt 11530 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | decltOLD 11531 | Obsolete proof of declt 11530 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | decltc 11532 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; | ||
Theorem | decltcOLD 11533 | Obsolete version of decltc 11532 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | declth 11534 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
; ; | ||
Theorem | decsuc 11535 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | decsucOLD 11536 | Obsolete proof of decsuc 11535 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | 3declth 11537 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
;; ;; | ||
Theorem | 3decltc 11538 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
; ; ;; ;; | ||
Theorem | 3decltcOLD 11539 | Obsolete version of 3decltc 11538 as of 6-Sep-2021. (Contributed by AV, 15-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
;; ;; | ||
Theorem | decle 11540 | Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
; ; | ||
Theorem | decleh 11541 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
; ; | ||
Theorem | declei 11542 | Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.) |
; | ||
Theorem | decleOLD 11543 | Obsolete version of decle 11540 as of 8-Sep-2021. (Contributed by AV, 17-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | declecOLD 11544 | Obsolete version of decleh 11541 as of 8-Sep-2021. (Contributed by AV, 17-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | numlti 11545 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | declti 11546 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | decltdi 11547 | Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.) |
; | ||
Theorem | decltiOLD 11548 | Obsolete version of declti 11546 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | numsucc 11549 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | decsucc 11550 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | decsuccOLD 11551 | Obsolete version of decsucc 11550 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | 1e0p1 11552 | The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | dec10p 11553 | Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | dec10pOLD 11554 | Obsolete version of dec10p 11553 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | dec10OLD 11555 | The decimal form of 10. NB: In our presentations of large numbers later on, we will use our symbol for 10 at the highest digits when advantageous, because we can use this theorem to convert back to "long form" (where each digit is in the range 0-9) with no extra effort. However, we cannot do this for lower digits while maintaining the ease of use of the decimal system, since it requires nontrivial number knowledge (more than just equality theorems) to convert back. (Contributed by Mario Carneiro, 18-Feb-2014.) Obsolete as of 6-Sep-2021, because the symbol will be removed, and ; will be used instead in general. (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | 9p1e10bOLD 11556 | Obsolete proof of 9p1e10 11496 as of 1-Aug-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | numma 11557 | Perform a multiply-add of two decimal integers and against a fixed multiplicand (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | nummac 11558 | Perform a multiply-add of two decimal integers and against a fixed multiplicand (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | numma2c 11559 | Perform a multiply-add of two decimal integers and against a fixed multiplicand (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | numadd 11560 | Add two decimal integers and (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | numaddc 11561 | Add two decimal integers and (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | nummul1c 11562 | The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | nummul2c 11563 | The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | decma 11564 | 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.) |
; ; ; | ||
Theorem | decmaOLD 11565 | Obsolete proof of decma 11564 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; | ||
Theorem | decmac 11566 | 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.) |
; ; ; ; | ||
Theorem | decmacOLD 11567 | Obsolete proof of decmac 11566 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; ; | ||
Theorem | decma2c 11568 | 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.) |
; ; ; ; | ||
Theorem | decma2cOLD 11569 | Obsolete proof of decma2c 11568 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; ; | ||
Theorem | decadd 11570 | Add two numerals and (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; | ||
Theorem | decaddOLD 11571 | Obsolete proof of decadd 11570 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; | ||
Theorem | decaddc 11572 | Add two numerals and (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; ; | ||
Theorem | decaddcOLD 11573 | Obsolete proof of decaddc 11572 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; ; | ||
Theorem | decaddc2OLD 11574 | Obsolete version of decaddc2 11575 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; | ||
Theorem | decaddc2 11575 | Add two numerals and (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; ; | ||
Theorem | decrmanc 11576 | Perform a multiply-add of two numerals and against a fixed multiplicand (no carry). (Contributed by AV, 16-Sep-2021.) |
; ; | ||
Theorem | decrmac 11577 | Perform a multiply-add of two numerals and against a fixed multiplicand (with carry). (Contributed by AV, 16-Sep-2021.) |
; ; ; | ||
Theorem | decaddm10 11578 | The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.) |
; ; ; | ||
Theorem | decaddi 11579 | Add two numerals and (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
; ; | ||
Theorem | decaddci 11580 | Add two numerals and (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
; ; ; | ||
Theorem | decaddci2 11581 | Add two numerals and (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; | ||
Theorem | decaddci2OLD 11582 | Obsolete version of decaddci2 11581 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | decsubi 11583 | Difference between a numeral and a nonnegative integer (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | decsubiOLD 11584 | Obsolete proof of decsubi 11583 as of 6-Sep-2021. (Contributed by AV, 22-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | decmul1 11585 | The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
; ; | ||
Theorem | decmul1OLD 11586 | Obsolete proof of decmul1 11585 as of 6-Sep-2021. (Contributed by AV, 22-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | decmul1c 11587 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; | ||
Theorem | decmul1cOLD 11588 | Obsolete proof of decmul1c 11587 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; | ||
Theorem | decmul2c 11589 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
; ; ; | ||
Theorem | decmul2cOLD 11590 | Obsolete proof of decmul2c 11589 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; ; | ||
Theorem | decmulnc 11591 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
; ; | ||
Theorem | 11multnc 11592 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
; ; | ||
Theorem | decmul10add 11593 | 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.) |
; ; | ||
Theorem | decmul10addOLD 11594 | Obsolete proof of decmul10add 11593 as of 6-Sep-2021. (Contributed by AV, 22-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
; ; | ||
Theorem | 6p5lem 11595 | Lemma for 6p5e11 11600 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
; ; | ||
Theorem | 5p5e10 11596 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | 5p5e10bOLD 11597 | Obsolete proof of 5p5e10 11596 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | 6p4e10 11598 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
; | ||
Theorem | 6p4e10bOLD 11599 | Obsolete proof of 6p4e10 11598 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
; | ||
Theorem | 6p5e11 11600 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
; |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |