Home | Metamath
Proof Explorer Theorem List (p. 123 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 7t2e14 12201 | 7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 2) = ;14 | ||
Theorem | 7t3e21 12202 | 7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 3) = ;21 | ||
Theorem | 7t4e28 12203 | 7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 4) = ;28 | ||
Theorem | 7t5e35 12204 | 7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 5) = ;35 | ||
Theorem | 7t6e42 12205 | 7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 6) = ;42 | ||
Theorem | 7t7e49 12206 | 7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 · 7) = ;49 | ||
Theorem | 8t2e16 12207 | 8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 2) = ;16 | ||
Theorem | 8t3e24 12208 | 8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 3) = ;24 | ||
Theorem | 8t4e32 12209 | 8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 4) = ;32 | ||
Theorem | 8t5e40 12210 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (8 · 5) = ;40 | ||
Theorem | 8t6e48 12211 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (8 · 6) = ;48 | ||
Theorem | 8t7e56 12212 | 8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 7) = ;56 | ||
Theorem | 8t8e64 12213 | 8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 · 8) = ;64 | ||
Theorem | 9t2e18 12214 | 9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 2) = ;18 | ||
Theorem | 9t3e27 12215 | 9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 3) = ;27 | ||
Theorem | 9t4e36 12216 | 9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 4) = ;36 | ||
Theorem | 9t5e45 12217 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 5) = ;45 | ||
Theorem | 9t6e54 12218 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 6) = ;54 | ||
Theorem | 9t7e63 12219 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 7) = ;63 | ||
Theorem | 9t8e72 12220 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 8) = ;72 | ||
Theorem | 9t9e81 12221 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 9) = ;81 | ||
Theorem | 9t11e99 12222 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
⊢ (9 · ;11) = ;99 | ||
Theorem | 9lt10 12223 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 9 < ;10 | ||
Theorem | 8lt10 12224 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 8 < ;10 | ||
Theorem | 7lt10 12225 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 7 < ;10 | ||
Theorem | 6lt10 12226 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 6 < ;10 | ||
Theorem | 5lt10 12227 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 5 < ;10 | ||
Theorem | 4lt10 12228 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 4 < ;10 | ||
Theorem | 3lt10 12229 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 3 < ;10 | ||
Theorem | 2lt10 12230 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 2 < ;10 | ||
Theorem | 1lt10 12231 | 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 12232 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) | ||
Theorem | decbin2 12233 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) | ||
Theorem | decbin3 12234 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) | ||
Theorem | halfthird 12235 | Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ ((1 / 2) − (1 / 3)) = (1 / 6) | ||
Theorem | 5recm6rec 12236 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) | ||
Syntax | cuz 12237 | Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". |
class ℤ≥ | ||
Definition | df-uz 12238* | 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 12239 for its value, uzssz 12258 for its relationship to ℤ, nnuz 12275 and nn0uz 12274 for its relationships to ℕ and ℕ0, and eluz1 12241 and eluz2 12243 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | ||
Theorem | uzval 12239* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) | ||
Theorem | uzf 12240 | 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 12241 | Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | ||
Theorem | eluzel2 12242 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | ||
Theorem | eluz2 12243 | 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 12244 | Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
Theorem | eluz1i 12245 | Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.) |
⊢ 𝑀 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | ||
Theorem | eluzuzle 12246 | 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 12247 | A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | ||
Theorem | eluzelre 12248 | A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | ||
Theorem | eluzelcn 12249 | A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) | ||
Theorem | eluzle 12250 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) | ||
Theorem | eluz 12251 | Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) | ||
Theorem | uzid 12252 | Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzidd 12253 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzn0 12254 | The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.) |
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅) | ||
Theorem | uztrn 12255 | Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.) |
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) | ||
Theorem | uztrn2 12256 | Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝐾) ⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) | ||
Theorem | uzneg 12257 | Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁)) | ||
Theorem | uzssz 12258 | 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 | uzss 12259 | Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀)) | ||
Theorem | uztric 12260 | Totality of the ordering relation on integers, stated in terms of upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jun-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ∨ 𝑀 ∈ (ℤ≥‘𝑁))) | ||
Theorem | uz11 12261 | The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.) |
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) | ||
Theorem | eluzp1m1 12262 | Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) | ||
Theorem | eluzp1l 12263 | Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) | ||
Theorem | eluzp1p1 12264 | Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1))) | ||
Theorem | eluzaddi 12265 | Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
Theorem | eluzsubi 12266 | Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | eluzadd 12267 | Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
Theorem | eluzsub 12268 | Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | subeluzsub 12269 | Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀 − 𝐾) ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
Theorem | uzm1 12270 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀))) | ||
Theorem | uznn0sub 12271 | The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0) | ||
Theorem | uzin 12272 | Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) | ||
Theorem | uzp1 12273 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) | ||
Theorem | nn0uz 12274 | Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
⊢ ℕ0 = (ℤ≥‘0) | ||
Theorem | nnuz 12275 | Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
⊢ ℕ = (ℤ≥‘1) | ||
Theorem | elnnuz 12276 | A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1)) | ||
Theorem | elnn0uz 12277 | A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0)) | ||
Theorem | eluz2nn 12278 | An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ) | ||
Theorem | eluz4eluz2 12279 | An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.) |
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ (ℤ≥‘2)) | ||
Theorem | eluz4nn 12280 | An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.) |
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ ℕ) | ||
Theorem | eluzge2nn0 12281 | If an integer is greater than or equal to 2, then it is a nonnegative integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV, 3-Nov-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ∈ ℕ0) | ||
Theorem | eluz2n0 12282 | An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0) | ||
Theorem | uzuzle23 12283 | An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝐴 ∈ (ℤ≥‘3) → 𝐴 ∈ (ℤ≥‘2)) | ||
Theorem | eluzge3nn 12284 | If an integer is greater than 3, then it is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℕ) | ||
Theorem | uz3m2nn 12285 | An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn 12317. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) | ||
Theorem | 1eluzge0 12286 | 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ 1 ∈ (ℤ≥‘0) | ||
Theorem | 2eluzge0 12287 | 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 2 ∈ (ℤ≥‘0) | ||
Theorem | 2eluzge1 12288 | 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ 2 ∈ (ℤ≥‘1) | ||
Theorem | uznnssnn 12289 | The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) |
⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ) | ||
Theorem | raluz 12290* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
Theorem | raluz2 12291* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
Theorem | rexuz 12292* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
Theorem | rexuz2 12293* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
Theorem | 2rexuz 12294* | Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.) |
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) | ||
Theorem | peano2uz 12295 | Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) | ||
Theorem | peano2uzs 12296 | Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) | ||
Theorem | peano2uzr 12297 | Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzaddcl 12298 | Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | nn0pzuz 12299 | The sum of a nonnegative integer and an integer is an integer greater than or equal to that integer. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑍 ∈ ℤ) → (𝑁 + 𝑍) ∈ (ℤ≥‘𝑍)) | ||
Theorem | uzind4 12300* | Induction on the upper set of integers that starts at an integer 𝑀. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005.) |
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |