| Metamath
Proof Explorer Theorem List (p. 129 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 11multnc 12801 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 | ||
| Theorem | decmul10add 12802 | 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 12803 | Lemma for 6p5e11 12806 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 | ||
| Theorem | 5p5e10 12804 | 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 12805 | 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 12806 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 5) = ;11 | ||
| Theorem | 6p6e12 12807 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 + 6) = ;12 | ||
| Theorem | 7p3e10 12808 | 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 12809 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 4) = ;11 | ||
| Theorem | 7p5e12 12810 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 5) = ;12 | ||
| Theorem | 7p6e13 12811 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 6) = ;13 | ||
| Theorem | 7p7e14 12812 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 7) = ;14 | ||
| Theorem | 8p2e10 12813 | 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 12814 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 3) = ;11 | ||
| Theorem | 8p4e12 12815 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 4) = ;12 | ||
| Theorem | 8p5e13 12816 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 5) = ;13 | ||
| Theorem | 8p6e14 12817 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 6) = ;14 | ||
| Theorem | 8p7e15 12818 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 7) = ;15 | ||
| Theorem | 8p8e16 12819 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 8) = ;16 | ||
| Theorem | 9p2e11 12820 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (9 + 2) = ;11 | ||
| Theorem | 9p3e12 12821 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 3) = ;12 | ||
| Theorem | 9p4e13 12822 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 4) = ;13 | ||
| Theorem | 9p5e14 12823 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 5) = ;14 | ||
| Theorem | 9p6e15 12824 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 6) = ;15 | ||
| Theorem | 9p7e16 12825 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 7) = ;16 | ||
| Theorem | 9p8e17 12826 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 8) = ;17 | ||
| Theorem | 9p9e18 12827 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 9) = ;18 | ||
| Theorem | 10p10e20 12828 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (;10 + ;10) = ;20 | ||
| Theorem | 10m1e9 12829 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
| ⊢ (;10 − 1) = 9 | ||
| Theorem | 4t3lem 12830 | Lemma for 4t3e12 12831 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷 & ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 | ||
| Theorem | 4t3e12 12831 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (4 · 3) = ;12 | ||
| Theorem | 4t4e16 12832 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (4 · 4) = ;16 | ||
| Theorem | 5t2e10 12833 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
| ⊢ (5 · 2) = ;10 | ||
| Theorem | 5t3e15 12834 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 3) = ;15 | ||
| Theorem | 5t4e20 12835 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 4) = ;20 | ||
| Theorem | 5t5e25 12836 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 · 5) = ;25 | ||
| Theorem | 6t2e12 12837 | 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 2) = ;12 | ||
| Theorem | 6t3e18 12838 | 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 3) = ;18 | ||
| Theorem | 6t4e24 12839 | 6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 · 4) = ;24 | ||
| Theorem | 6t5e30 12840 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 · 5) = ;30 | ||
| Theorem | 6t6e36 12841 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 · 6) = ;36 | ||
| Theorem | 7t2e14 12842 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 2) = ;14 | ||
| Theorem | 7t3e21 12843 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 3) = ;21 | ||
| Theorem | 7t4e28 12844 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 4) = ;28 | ||
| Theorem | 7t5e35 12845 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 5) = ;35 | ||
| Theorem | 7t6e42 12846 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 6) = ;42 | ||
| Theorem | 7t7e49 12847 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 · 7) = ;49 | ||
| Theorem | 8t2e16 12848 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 2) = ;16 | ||
| Theorem | 8t3e24 12849 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 3) = ;24 | ||
| Theorem | 8t4e32 12850 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 4) = ;32 | ||
| Theorem | 8t5e40 12851 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 · 5) = ;40 | ||
| Theorem | 8t6e48 12852 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 · 6) = ;48 | ||
| Theorem | 8t7e56 12853 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 7) = ;56 | ||
| Theorem | 8t8e64 12854 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 · 8) = ;64 | ||
| Theorem | 9t2e18 12855 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 2) = ;18 | ||
| Theorem | 9t3e27 12856 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 3) = ;27 | ||
| Theorem | 9t4e36 12857 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 4) = ;36 | ||
| Theorem | 9t5e45 12858 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 5) = ;45 | ||
| Theorem | 9t6e54 12859 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 6) = ;54 | ||
| Theorem | 9t7e63 12860 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 7) = ;63 | ||
| Theorem | 9t8e72 12861 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 8) = ;72 | ||
| Theorem | 9t9e81 12862 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 · 9) = ;81 | ||
| Theorem | 9t11e99 12863 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (9 · ;11) = ;99 | ||
| Theorem | 9lt10 12864 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 9 < ;10 | ||
| Theorem | 8lt10 12865 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 8 < ;10 | ||
| Theorem | 7lt10 12866 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 7 < ;10 | ||
| Theorem | 6lt10 12867 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 6 < ;10 | ||
| Theorem | 5lt10 12868 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 5 < ;10 | ||
| Theorem | 4lt10 12869 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 4 < ;10 | ||
| Theorem | 3lt10 12870 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 3 < ;10 | ||
| Theorem | 2lt10 12871 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 2 < ;10 | ||
| Theorem | 1lt10 12872 | 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 12873 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) | ||
| Theorem | decbin2 12874 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) | ||
| Theorem | decbin3 12875 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) | ||
| Theorem | halfthird 12876 | Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.) |
| ⊢ ((1 / 2) − (1 / 3)) = (1 / 6) | ||
| Theorem | 5recm6rec 12877 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
| ⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) | ||
| Syntax | cuz 12878 | Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". |
| class ℤ≥ | ||
| Definition | df-uz 12879* | 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 12880 for its value, uzssz 12899 for its relationship to ℤ, nnuz 12921 and nn0uz 12920 for its relationships to ℕ and ℕ0, and eluz1 12882 and eluz2 12884 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
| ⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | ||
| Theorem | uzval 12880* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) | ||
| Theorem | uzf 12881 | 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 12882 | Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
| ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | ||
| Theorem | eluzel2 12883 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | ||
| Theorem | eluz2 12884 | 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 12885 | Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
| Theorem | eluz1i 12886 | Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.) |
| ⊢ 𝑀 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | ||
| Theorem | eluzuzle 12887 | 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 12888 | A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | ||
| Theorem | eluzelre 12889 | A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | ||
| Theorem | eluzelcn 12890 | A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) | ||
| Theorem | eluzle 12891 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) | ||
| Theorem | eluz 12892 | Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) | ||
| Theorem | uzid 12893 | Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
| ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
| Theorem | uzidd 12894 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
| Theorem | uzn0 12895 | The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.) |
| ⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅) | ||
| Theorem | uztrn 12896 | Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.) |
| ⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) | ||
| Theorem | uztrn2 12897 | Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
| ⊢ 𝑍 = (ℤ≥‘𝐾) ⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) | ||
| Theorem | uzneg 12898 | Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁)) | ||
| Theorem | uzssz 12899 | An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
| ⊢ (ℤ≥‘𝑀) ⊆ ℤ | ||
| Theorem | uzssre 12900 | An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
| ⊢ (ℤ≥‘𝑀) ⊆ ℝ | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |