HomeTheorem List (p. 130 of 514)
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. 130 of 514) | < 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-31553) |
Hilbert Space Explorer
(31554-33076) |
Users' Mathboxes
(33077-51302) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | decmac 12901 | 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 12902 | 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 12903 | 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 12904 | 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 12905 | 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 12906 | 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 12907 | 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 12908 | 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 12909 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 | ||
| Theorem | decaddci 12910 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 | ||
| Theorem | decaddci2 12911 | 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 12912 | 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 12913 | 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 12914 | 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 12915 | 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 12916 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) | ||
| Theorem | 11multnc 12917 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 | ||
| Theorem | decmul10add 12918 | 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 12919 | Lemma for 6p5e11 12922 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 | ||
| Theorem | 5p5e10 12920 | 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 12921 | 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 12922 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 5) = ;11 | ||
| Theorem | 6p6e12 12923 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 + 6) = ;12 | ||
| Theorem | 7p3e10 12924 | 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 12925 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 4) = ;11 | ||
| Theorem | 7p5e12 12926 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 5) = ;12 | ||
| Theorem | 7p6e13 12927 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 6) = ;13 | ||
| Theorem | 7p7e14 12928 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 7) = ;14 | ||
| Theorem | 8p2e10 12929 | 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 12930 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 3) = ;11 | ||
| Theorem | 8p4e12 12931 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 4) = ;12 | ||
| Theorem | 8p5e13 12932 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 5) = ;13 | ||
| Theorem | 8p6e14 12933 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 6) = ;14 | ||
| Theorem | 8p7e15 12934 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 7) = ;15 | ||
| Theorem | 8p8e16 12935 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 8) = ;16 | ||
| Theorem | 9p2e11 12936 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (9 + 2) = ;11 | ||
| Theorem | 9p3e12 12937 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 3) = ;12 | ||
| Theorem | 9p4e13 12938 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 4) = ;13 | ||
| Theorem | 9p5e14 12939 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 5) = ;14 | ||
| Theorem | 9p6e15 12940 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 6) = ;15 | ||
| Theorem | 9p7e16 12941 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 7) = ;16 | ||
| Theorem | 9p8e17 12942 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 8) = ;17 | ||
| Theorem | 9p9e18 12943 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 9) = ;18 | ||
| Theorem | 10p10e20 12944 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (;10 + ;10) = ;20 | ||
| Theorem | 10m1e9 12945 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (;10 − 1) = 9 | ||
| Theorem | 4t3lem 12946 | Lemma for 4t3e12 12947 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷 & ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 | ||
| Theorem | 4t3e12 12947 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (4 · 3) = ;12 | ||
| Theorem | 4t4e16 12948 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (4 · 4) = ;16 | ||
| Theorem | 5t2e10 12949 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
| ⊢ (5 · 2) = ;10 | ||
| Theorem | 5t3e15 12950 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 3) = ;15 | ||
| Theorem | 5t4e20 12951 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 4) = ;20 | ||
| Theorem | 5t5e25 12952 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 5) = ;25 | ||
| Theorem | 6t2e12 12953 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 2) = ;12 | ||
| Theorem | 6t3e18 12954 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 3) = ;18 | ||
| Theorem | 6t4e24 12955 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 4) = ;24 | ||
| Theorem | 6t5e30 12956 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 · 5) = ;30 | ||
| Theorem | 6t6e36 12957 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 · 6) = ;36 | ||
| Theorem | 7t2e14 12958 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 2) = ;14 | ||
| Theorem | 7t3e21 12959 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 3) = ;21 | ||
| Theorem | 7t4e28 12960 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 4) = ;28 | ||
| Theorem | 7t5e35 12961 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 5) = ;35 | ||
| Theorem | 7t6e42 12962 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 6) = ;42 | ||
| Theorem | 7t7e49 12963 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 7) = ;49 | ||
| Theorem | 8t2e16 12964 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 2) = ;16 | ||
| Theorem | 8t3e24 12965 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 3) = ;24 | ||
| Theorem | 8t4e32 12966 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 4) = ;32 | ||
| Theorem | 8t5e40 12967 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 · 5) = ;40 | ||
| Theorem | 8t6e48 12968 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 · 6) = ;48 | ||
| Theorem | 8t7e56 12969 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 7) = ;56 | ||
| Theorem | 8t8e64 12970 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 8) = ;64 | ||
| Theorem | 9t2e18 12971 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 2) = ;18 | ||
| Theorem | 9t3e27 12972 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 3) = ;27 | ||
| Theorem | 9t4e36 12973 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 4) = ;36 | ||
| Theorem | 9t5e45 12974 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 5) = ;45 | ||
| Theorem | 9t6e54 12975 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 6) = ;54 | ||
| Theorem | 9t7e63 12976 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 7) = ;63 | ||
| Theorem | 9t8e72 12977 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 8) = ;72 | ||
| Theorem | 9t9e81 12978 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 9) = ;81 | ||
| Theorem | 9t11e99 12979 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ (9 · ;11) = ;99 | ||
| Theorem | 9t11e99OLD 12980 | Obsolete version of 9t11e99 12979 as of 10-Jun-2026. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (9 · ;11) = ;99 | ||
| Theorem | 9lt10 12981 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 9 < ;10 | ||
| Theorem | 8lt10 12982 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 8 < ;10 | ||
| Theorem | 7lt10 12983 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 7 < ;10 | ||
| Theorem | 6lt10 12984 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 6 < ;10 | ||
| Theorem | 5lt10 12985 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 5 < ;10 | ||
| Theorem | 4lt10 12986 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 4 < ;10 | ||
| Theorem | 3lt10 12987 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 3 < ;10 | ||
| Theorem | 2lt10 12988 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 2 < ;10 | ||
| Theorem | 1lt10 12989 | 1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.) |
| ⊢ 1 < ;10 | ||
| Theorem | 1lt10OLD 12990 | Obsolete version of 1lt10 12989 as of 10-Jun-2026. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 1 < ;10 | ||
| Theorem | decbin0 12991 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) | ||
| Theorem | decbin2 12992 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) | ||
| Theorem | decbin3 12993 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) | ||
| Theorem | 5recm6rec 12994 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
| ⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) | ||
| Syntax | cuz 12995 | Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". |
| class ℤ≥ | ||
| Definition | df-uz 12996* | 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 12997 for its value, uzssz 13016 for its relationship to ℤ, nnuz 13034 and nn0uz 13033 for its relationships to ℕ and ℕ0, and eluz1 12999 and eluz2 13001 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
| ⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | ||
| Theorem | uzval 12997* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) | ||
| Theorem | uzf 12998 | 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 12999 | Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
| ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | ||
| Theorem | eluzel2 13000 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |