![]() |
Metamath
Proof Explorer Theorem List (p. 129 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 9t5e45 12801 | 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 5) = ;45 | ||
Theorem | 9t6e54 12802 | 9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 6) = ;54 | ||
Theorem | 9t7e63 12803 | 9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 7) = ;63 | ||
Theorem | 9t8e72 12804 | 9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 8) = ;72 | ||
Theorem | 9t9e81 12805 | 9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 · 9) = ;81 | ||
Theorem | 9t11e99 12806 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
⊢ (9 · ;11) = ;99 | ||
Theorem | 9lt10 12807 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 9 < ;10 | ||
Theorem | 8lt10 12808 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 8 < ;10 | ||
Theorem | 7lt10 12809 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 7 < ;10 | ||
Theorem | 6lt10 12810 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 6 < ;10 | ||
Theorem | 5lt10 12811 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 5 < ;10 | ||
Theorem | 4lt10 12812 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 4 < ;10 | ||
Theorem | 3lt10 12813 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 3 < ;10 | ||
Theorem | 2lt10 12814 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
⊢ 2 < ;10 | ||
Theorem | 1lt10 12815 | 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 12816 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (4 · 𝐴) = (2 · (2 · 𝐴)) | ||
Theorem | decbin2 12817 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1)) | ||
Theorem | decbin3 12818 | Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1) | ||
Theorem | halfthird 12819 | Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ ((1 / 2) − (1 / 3)) = (1 / 6) | ||
Theorem | 5recm6rec 12820 | One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30) | ||
Syntax | cuz 12821 | Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". |
class ℤ≥ | ||
Definition | df-uz 12822* | 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 12823 for its value, uzssz 12842 for its relationship to ℤ, nnuz 12864 and nn0uz 12863 for its relationships to ℕ and ℕ0, and eluz1 12825 and eluz2 12827 for its membership relations. (Contributed by NM, 5-Sep-2005.) |
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | ||
Theorem | uzval 12823* | The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘}) | ||
Theorem | uzf 12824 | 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 12825 | Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | ||
Theorem | eluzel2 12826 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | ||
Theorem | eluz2 12827 | 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 12828 | Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
Theorem | eluz1i 12829 | Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.) |
⊢ 𝑀 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | ||
Theorem | eluzuzle 12830 | 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 12831 | A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | ||
Theorem | eluzelre 12832 | A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | ||
Theorem | eluzelcn 12833 | A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) | ||
Theorem | eluzle 12834 | Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) | ||
Theorem | eluz 12835 | Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) | ||
Theorem | uzid 12836 | Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzidd 12837 | Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzn0 12838 | The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.) |
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅) | ||
Theorem | uztrn 12839 | Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.) |
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁)) | ||
Theorem | uztrn2 12840 | Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝐾) ⇒ ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) | ||
Theorem | uzneg 12841 | Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁)) | ||
Theorem | uzssz 12842 | 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 12843 | An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (ℤ≥‘𝑀) ⊆ ℝ | ||
Theorem | uzss 12844 | Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀)) | ||
Theorem | uztric 12845 | 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 12846 | The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.) |
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) | ||
Theorem | eluzp1m1 12847 | Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) | ||
Theorem | eluzp1l 12848 | Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) | ||
Theorem | eluzp1p1 12849 | Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1))) | ||
Theorem | eluzadd 12850 | Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by SN, 7-Feb-2025.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
Theorem | eluzsub 12851 | Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by SN, 7-Feb-2025.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | eluzaddi 12852 | Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) Shorten and remove 𝑀 ∈ ℤ hypothesis. (Revised by SN, 7-Feb-2025.) |
⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
Theorem | eluzaddiOLD 12853 | Obsolete version of eluzaddi 12852 as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
Theorem | eluzsubi 12854 | Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof shortened by SN, 7-Feb-2025.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | eluzsubiOLD 12855 | Obsolete version of eluzsubi 12854 as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | eluzaddOLD 12856 | Obsolete version of eluzadd 12850 as of 7-Feb-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
Theorem | eluzsubOLD 12857 | Obsolete version of eluzsub 12851 as of 7-Feb-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | subeluzsub 12858 | Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀 − 𝐾) ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
Theorem | uzm1 12859 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀))) | ||
Theorem | uznn0sub 12860 | The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0) | ||
Theorem | uzin 12861 | Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) | ||
Theorem | uzp1 12862 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) | ||
Theorem | nn0uz 12863 | Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
⊢ ℕ0 = (ℤ≥‘0) | ||
Theorem | nnuz 12864 | Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
⊢ ℕ = (ℤ≥‘1) | ||
Theorem | elnnuz 12865 | A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1)) | ||
Theorem | elnn0uz 12866 | A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0)) | ||
Theorem | eluz2nn 12867 | An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ) | ||
Theorem | eluz4eluz2 12868 | 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 12869 | An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.) |
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ ℕ) | ||
Theorem | eluzge2nn0 12870 | 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 12871 | An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0) | ||
Theorem | uzuzle23 12872 | 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 12873 | 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 12874 | An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn 12906. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) | ||
Theorem | 1eluzge0 12875 | 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ 1 ∈ (ℤ≥‘0) | ||
Theorem | 2eluzge0 12876 | 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 12877 | 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ 2 ∈ (ℤ≥‘1) | ||
Theorem | uznnssnn 12878 | The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) |
⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ) | ||
Theorem | raluz 12879* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
Theorem | raluz2 12880* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
Theorem | rexuz 12881* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
Theorem | rexuz2 12882* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
Theorem | 2rexuz 12883* | Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.) |
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) | ||
Theorem | peano2uz 12884 | Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) | ||
Theorem | peano2uzs 12885 | Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) | ||
Theorem | peano2uzr 12886 | Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzaddcl 12887 | Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | nn0pzuz 12888 | 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 12889* | 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) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzind4ALT 12890* | Induction on the upper set of integers that starts at an integer 𝑀. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 12889 or uzind4ALT 12890 may be used; see comment for nnind 12229. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzind4s 12891* | Induction on the upper set of integers that starts at an integer 𝑀, using explicit substitution. The hypotheses are the basis and the induction step. (Contributed by NM, 4-Nov-2005.) |
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑘]𝜑) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜑 → [(𝑘 + 1) / 𝑘]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑘]𝜑) | ||
Theorem | uzind4s2 12892* | Induction on the upper set of integers that starts at an integer 𝑀, using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s 12891 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.) |
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) | ||
Theorem | uzind4i 12893* | Induction on the upper integers that start at 𝑀. The first four give us the substitution instances we need, and the last two are the basis and the induction step. This is a stronger version of uzind4 12889 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 12826). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.) |
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzwo 12894* | Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) |
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) | ||
Theorem | uzwo2 12895* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. (Contributed by NM, 8-Oct-2005.) |
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃!𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) | ||
Theorem | nnwo 12896* | Well-ordering principle: any nonempty set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) |
⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | nnwof 12897* | Well-ordering principle: any nonempty set of positive integers has a least element. This version allows 𝑥 and 𝑦 to be present in 𝐴 as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | nnwos 12898* | Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦))) | ||
Theorem | indstr 12899* | Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) | ||
Theorem | eluznn0 12900 | Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |