HomeTheorem List (p. 128 of 498)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 128 of 498) | < 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-30847) |
Hilbert Space Explorer
(30848-32370) |
Users' Mathboxes
(32371-49794) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | decmac 12701 | 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 12702 | 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 12703 | 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 12704 | 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 12705 | 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 12706 | 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 12707 | 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 12708 | 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 12709 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 | ||
| Theorem | decaddci 12710 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 | ||
| Theorem | decaddci2 12711 | 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 12712 | 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 12713 | 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 12714 | 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 12715 | 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 12716 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) | ||
| Theorem | 11multnc 12717 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 | ||
| Theorem | decmul10add 12718 | 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 12719 | Lemma for 6p5e11 12722 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 | ||
| Theorem | 5p5e10 12720 | 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 12721 | 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 12722 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 5) = ;11 | ||
| Theorem | 6p6e12 12723 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 + 6) = ;12 | ||
| Theorem | 7p3e10 12724 | 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 12725 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 4) = ;11 | ||
| Theorem | 7p5e12 12726 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 5) = ;12 | ||
| Theorem | 7p6e13 12727 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 6) = ;13 | ||
| Theorem | 7p7e14 12728 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 7) = ;14 | ||
| Theorem | 8p2e10 12729 | 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 12730 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 3) = ;11 | ||
| Theorem | 8p4e12 12731 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 4) = ;12 | ||
| Theorem | 8p5e13 12732 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 5) = ;13 | ||
| Theorem | 8p6e14 12733 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 6) = ;14 | ||
| Theorem | 8p7e15 12734 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 7) = ;15 | ||
| Theorem | 8p8e16 12735 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 8) = ;16 | ||
| Theorem | 9p2e11 12736 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (9 + 2) = ;11 | ||
| Theorem | 9p3e12 12737 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 3) = ;12 | ||
| Theorem | 9p4e13 12738 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 4) = ;13 | ||
| Theorem | 9p5e14 12739 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 5) = ;14 | ||
| Theorem | 9p6e15 12740 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 6) = ;15 | ||
| Theorem | 9p7e16 12741 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 7) = ;16 | ||
| Theorem | 9p8e17 12742 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 8) = ;17 | ||
| Theorem | 9p9e18 12743 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 9) = ;18 | ||
| Theorem | 10p10e20 12744 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (;10 + ;10) = ;20 | ||
| Theorem | 10m1e9 12745 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (;10 − 1) = 9 | ||
| Theorem | 4t3lem 12746 | Lemma for 4t3e12 12747 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷 & ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 | ||
| Theorem | 4t3e12 12747 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (4 · 3) = ;12 | ||
| Theorem | 4t4e16 12748 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (4 · 4) = ;16 | ||
| Theorem | 5t2e10 12749 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
| ⊢ (5 · 2) = ;10 | ||
| Theorem | 5t3e15 12750 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 3) = ;15 | ||
| Theorem | 5t4e20 12751 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 4) = ;20 | ||
| Theorem | 5t5e25 12752 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 5) = ;25 | ||
| Theorem | 6t2e12 12753 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 2) = ;12 | ||
| Theorem | 6t3e18 12754 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 3) = ;18 | ||
| Theorem | 6t4e24 12755 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 4) = ;24 | ||
| Theorem | 6t5e30 12756 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 · 5) = ;30 | ||
| Theorem | 6t6e36 12757 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 · 6) = ;36 | ||
| Theorem | 7t2e14 12758 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 2) = ;14 | ||
| Theorem | 7t3e21 12759 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 3) = ;21 | ||
| Theorem | 7t4e28 12760 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 4) = ;28 | ||
| Theorem | 7t5e35 12761 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 5) = ;35 | ||
| Theorem | 7t6e42 12762 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 6) = ;42 | ||
| Theorem | 7t7e49 12763 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 7) = ;49 | ||
| Theorem | 8t2e16 12764 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 2) = ;16 | ||
| Theorem | 8t3e24 12765 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 3) = ;24 | ||
| Theorem | 8t4e32 12766 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 4) = ;32 | ||
| Theorem | 8t5e40 12767 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 · 5) = ;40 | ||
| Theorem | 8t6e48 12768 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 · 6) = ;48 | ||
| Theorem | 8t7e56 12769 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 7) = ;56 | ||
| Theorem | 8t8e64 12770 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 8) = ;64 | ||
| Theorem | 9t2e18 12771 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 2) = ;18 | ||
| Theorem | 9t3e27 12772 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 3) = ;27 | ||
| Theorem | 9t4e36 12773 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 4) = ;36 | ||
| Theorem | 9t5e45 12774 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 5) = ;45 | ||
| Theorem | 9t6e54 12775 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 6) = ;54 | ||
| Theorem | 9t7e63 12776 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 7) = ;63 | ||
| Theorem | 9t8e72 12777 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 8) = ;72 | ||
| Theorem | 9t9e81 12778 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 9) = ;81 | ||
| Theorem | 9t11e99 12779 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (9 · ;11) = ;99 | ||
| Theorem | 9lt10 12780 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 9 < ;10 | ||
| Theorem | 8lt10 12781 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 8 < ;10 | ||
| Theorem | 7lt10 12782 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 7 < ;10 | ||
| Theorem | 6lt10 12783 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 6 < ;10 | ||
| Theorem | 5lt10 12784 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 5 < ;10 | ||
| Theorem | 4lt10 12785 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 4 < ;10 | ||
| Theorem | 3lt10 12786 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 3 < ;10 | ||
| Theorem | 2lt10 12787 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 2 < ;10 | ||
| Theorem | 1lt10 12788 | 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 12789 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) | ||
| Theorem | decbin2 12790 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) | ||
| Theorem | decbin3 12791 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) | ||
| Theorem | 5recm6rec 12792 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
| ⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) | ||
| Syntax | cuz 12793 | Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". |
| class ℤ≥ | ||
| Definition | df-uz 12794* | 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 12795 for its value, uzssz 12814 for its relationship to ℤ, nnuz 12836 and nn0uz 12835 for its relationships to ℕ and ℕ0, and eluz1 12797 and eluz2 12799 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
| ⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | ||
| Theorem | uzval 12795* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) | ||
| Theorem | uzf 12796 | 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 12797 | Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
| ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | ||
| Theorem | eluzel2 12798 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | ||
| Theorem | eluz2 12799 | 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 | eluzmn 12800 | Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |