Home | Metamath
Proof Explorer Theorem List (p. 117 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 6p5e11OLD 11601 | Obsolete proof of 6p5e11 11600 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (6 + 5) = ;11 | ||
Theorem | 6p6e12 11602 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (6 + 6) = ;12 | ||
Theorem | 7p3e10 11603 | 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 | 7p3e10bOLD 11604 | Obsolete proof of 7p3e10 11603 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (7 + 3) = ;10 | ||
Theorem | 7p4e11 11605 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (7 + 4) = ;11 | ||
Theorem | 7p4e11OLD 11606 | Obsolete proof of 7p4e11 11605 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (7 + 4) = ;11 | ||
Theorem | 7p5e12 11607 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 + 5) = ;12 | ||
Theorem | 7p6e13 11608 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 + 6) = ;13 | ||
Theorem | 7p7e14 11609 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 + 7) = ;14 | ||
Theorem | 8p2e10 11610 | 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 | 8p2e10bOLD 11611 | Obsolete proof of 8p2e10 11610 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (8 + 2) = ;10 | ||
Theorem | 8p3e11 11612 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (8 + 3) = ;11 | ||
Theorem | 8p3e11OLD 11613 | Obsolete proof of 8p3e11 11612 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (8 + 3) = ;11 | ||
Theorem | 8p4e12 11614 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 4) = ;12 | ||
Theorem | 8p5e13 11615 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 5) = ;13 | ||
Theorem | 8p6e14 11616 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 6) = ;14 | ||
Theorem | 8p7e15 11617 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 7) = ;15 | ||
Theorem | 8p8e16 11618 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 8) = ;16 | ||
Theorem | 9p2e11 11619 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (9 + 2) = ;11 | ||
Theorem | 9p2e11OLD 11620 | Obsolete proof of 9p2e11 11619 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (9 + 2) = ;11 | ||
Theorem | 9p3e12 11621 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 3) = ;12 | ||
Theorem | 9p4e13 11622 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 4) = ;13 | ||
Theorem | 9p5e14 11623 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 5) = ;14 | ||
Theorem | 9p6e15 11624 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 6) = ;15 | ||
Theorem | 9p7e16 11625 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 7) = ;16 | ||
Theorem | 9p8e17 11626 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 8) = ;17 | ||
Theorem | 9p9e18 11627 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 9) = ;18 | ||
Theorem | 10p10e20 11628 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (;10 + ;10) = ;20 | ||
Theorem | 10p10e20OLD 11629 | Obsolete version of 10p10e20 11628 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (10 + 10) = ;20 | ||
Theorem | 10m1e9 11630 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
⊢ (;10 − 1) = 9 | ||
Theorem | 4t3lem 11631 | Lemma for 4t3e12 11632 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷 & ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 | ||
Theorem | 4t3e12 11632 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (4 · 3) = ;12 | ||
Theorem | 4t4e16 11633 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (4 · 4) = ;16 | ||
Theorem | 5t2e10 11634 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
⊢ (5 · 2) = ;10 | ||
Theorem | 5t3e15 11635 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (5 · 3) = ;15 | ||
Theorem | 5t3e15OLD 11636 | Obsolete proof of 5t3e15 11635 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (5 · 3) = ;15 | ||
Theorem | 5t4e20 11637 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (5 · 4) = ;20 | ||
Theorem | 5t4e20OLD 11638 | Obsolete proof of 5t4e20 11637 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (5 · 4) = ;20 | ||
Theorem | 5t5e25 11639 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (5 · 5) = ;25 | ||
Theorem | 5t5e25OLD 11640 | Obsolete proof of 5t5e25 11639 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (5 · 5) = ;25 | ||
Theorem | 6t2e12 11641 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (6 · 2) = ;12 | ||
Theorem | 6t3e18 11642 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (6 · 3) = ;18 | ||
Theorem | 6t4e24 11643 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (6 · 4) = ;24 | ||
Theorem | 6t5e30 11644 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (6 · 5) = ;30 | ||
Theorem | 6t5e30OLD 11645 | Obsolete proof of 6t5e30 11644 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (6 · 5) = ;30 | ||
Theorem | 6t6e36 11646 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (6 · 6) = ;36 | ||
Theorem | 6t6e36OLD 11647 | Obsolete proof of 6t6e36 11646 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (6 · 6) = ;36 | ||
Theorem | 7t2e14 11648 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 2) = ;14 | ||
Theorem | 7t3e21 11649 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 3) = ;21 | ||
Theorem | 7t4e28 11650 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 4) = ;28 | ||
Theorem | 7t5e35 11651 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 5) = ;35 | ||
Theorem | 7t6e42 11652 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 6) = ;42 | ||
Theorem | 7t7e49 11653 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 7) = ;49 | ||
Theorem | 8t2e16 11654 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 2) = ;16 | ||
Theorem | 8t3e24 11655 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 3) = ;24 | ||
Theorem | 8t4e32 11656 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 4) = ;32 | ||
Theorem | 8t5e40 11657 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (8 · 5) = ;40 | ||
Theorem | 8t5e40OLD 11658 | Obsolete proof of 8t5e40 11657 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (8 · 5) = ;40 | ||
Theorem | 8t6e48 11659 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (8 · 6) = ;48 | ||
Theorem | 8t6e48OLD 11660 | Obsolete proof of 8t6e48 11659 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (8 · 6) = ;48 | ||
Theorem | 8t7e56 11661 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 7) = ;56 | ||
Theorem | 8t8e64 11662 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 8) = ;64 | ||
Theorem | 9t2e18 11663 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 2) = ;18 | ||
Theorem | 9t3e27 11664 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 3) = ;27 | ||
Theorem | 9t4e36 11665 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 4) = ;36 | ||
Theorem | 9t5e45 11666 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 5) = ;45 | ||
Theorem | 9t6e54 11667 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 6) = ;54 | ||
Theorem | 9t7e63 11668 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 7) = ;63 | ||
Theorem | 9t8e72 11669 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 8) = ;72 | ||
Theorem | 9t9e81 11670 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 9) = ;81 | ||
Theorem | 9t11e99 11671 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
⊢ (9 · ;11) = ;99 | ||
Theorem | 9t11e99OLD 11672 | Obsolete proof of 9t11e99 11671 as of 6-Sep-2021. (Contributed by AV, 14-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (9 · ;11) = ;99 | ||
Theorem | 9lt10 11673 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 9 < ;10 | ||
Theorem | 8lt10 11674 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 8 < ;10 | ||
Theorem | 7lt10 11675 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 7 < ;10 | ||
Theorem | 6lt10 11676 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 6 < ;10 | ||
Theorem | 5lt10 11677 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 5 < ;10 | ||
Theorem | 4lt10 11678 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 4 < ;10 | ||
Theorem | 3lt10 11679 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 3 < ;10 | ||
Theorem | 2lt10 11680 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 2 < ;10 | ||
Theorem | 1lt10 11681 | 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 11682 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) | ||
Theorem | decbin2 11683 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) | ||
Theorem | decbin3 11684 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) | ||
Theorem | halfthird 11685 | Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ ((1 / 2) − (1 / 3)) = (1 / 6) | ||
Theorem | 5recm6rec 11686 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) | ||
Syntax | cuz 11687 | Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀." |
class ℤ≥ | ||
Definition | df-uz 11688* | 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 11689 for its value, uzssz 11707 for its relationship to ℤ, nnuz 11723 and nn0uz 11722 for its relationships to ℕ and ℕ0, and eluz1 11691 and eluz2 11693 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | ||
Theorem | uzval 11689* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) | ||
Theorem | uzf 11690 | The domain and range of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ ℤ≥:ℤ⟶𝒫 ℤ | ||
Theorem | eluz1 11691 | Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | ||
Theorem | eluzel2 11692 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | ||
Theorem | eluz2 11693 | 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 11694 | Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
Theorem | eluz1i 11695 | Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.) |
⊢ 𝑀 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | ||
Theorem | eluzuzle 11696 | An integer in an upper set of integers is an element of an upper set of integers with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018.) |
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≤ 𝐴) → (𝐶 ∈ (ℤ≥‘𝐴) → 𝐶 ∈ (ℤ≥‘𝐵))) | ||
Theorem | eluzelz 11697 | A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | ||
Theorem | eluzelre 11698 | A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | ||
Theorem | eluzelcn 11699 | A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) | ||
Theorem | eluzle 11700 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |