| Metamath
Proof Explorer Theorem List (p. 130 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 | uzss 12901 | Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀)) | ||
| Theorem | uztric 12902 | 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 12903 | The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.) |
| ⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) | ||
| Theorem | eluzp1m1 12904 | Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | eluzp1l 12905 | Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) | ||
| Theorem | eluzp1p1 12906 | Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1))) | ||
| Theorem | eluzadd 12907 | Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by SN, 7-Feb-2025.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
| Theorem | eluzsub 12908 | Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by SN, 7-Feb-2025.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | eluzaddi 12909 | 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 12910 | Obsolete version of eluzaddi 12909 as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
| Theorem | eluzsubi 12911 | Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof shortened by SN, 7-Feb-2025.) |
| ⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | eluzsubiOLD 12912 | Obsolete version of eluzsubi 12911 as of 7-Feb-2025. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑀 ∈ ℤ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | eluzaddOLD 12913 | Obsolete version of eluzadd 12907 as of 7-Feb-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾))) | ||
| Theorem | eluzsubOLD 12914 | Obsolete version of eluzsub 12908 as of 7-Feb-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | subeluzsub 12915 | Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀 − 𝐾) ∈ (ℤ≥‘(𝑀 − 𝑁))) | ||
| Theorem | uzm1 12916 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀))) | ||
| Theorem | uznn0sub 12917 | The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0) | ||
| Theorem | uzin 12918 | Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) | ||
| Theorem | uzp1 12919 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) | ||
| Theorem | nn0uz 12920 | Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
| ⊢ ℕ0 = (ℤ≥‘0) | ||
| Theorem | nnuz 12921 | Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
| ⊢ ℕ = (ℤ≥‘1) | ||
| Theorem | elnnuz 12922 | A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
| ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1)) | ||
| Theorem | elnn0uz 12923 | A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
| ⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0)) | ||
| Theorem | eluz2nn 12924 | An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ) | ||
| Theorem | eluz4eluz2 12925 | 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 | eluz4eluz3 12926 | An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025.) |
| ⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ (ℤ≥‘3)) | ||
| Theorem | 5eluz3 12927 | 5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025.) |
| ⊢ 5 ∈ (ℤ≥‘3) | ||
| Theorem | eluz4nn 12928 | An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.) |
| ⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ ℕ) | ||
| Theorem | eluzge2nn0 12929 | 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 12930 | An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0) | ||
| Theorem | uzuzle23 12931 | 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 12932 | 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 12933 | An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn 12965. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
| ⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) | ||
| Theorem | 1eluzge0 12934 | 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
| ⊢ 1 ∈ (ℤ≥‘0) | ||
| Theorem | 2eluzge0 12935 | 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 12936 | 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
| ⊢ 2 ∈ (ℤ≥‘1) | ||
| Theorem | uznnssnn 12937 | The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) |
| ⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ) | ||
| Theorem | raluz 12938* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
| ⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
| Theorem | raluz2 12939* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
| ⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
| Theorem | rexuz 12940* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
| ⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
| Theorem | rexuz2 12941* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
| ⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
| Theorem | 2rexuz 12942* | Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.) |
| ⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) | ||
| Theorem | peano2uz 12943 | Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.) |
| ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | peano2uzs 12944 | Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) | ||
| Theorem | peano2uzr 12945 | Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) | ||
| Theorem | uzaddcl 12946 | Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀)) | ||
| Theorem | nn0pzuz 12947 | 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 12948* | 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 12949* | 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 12948 or uzind4ALT 12949 may be used; see comment for nnind 12284. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
| Theorem | uzind4s 12950* | 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 12951* | 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 12950 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.) |
| ⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) | ||
| Theorem | uzind4i 12952* | 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 12948 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 12883). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.) |
| ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
| Theorem | uzwo 12953* | Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) |
| ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) | ||
| Theorem | uzwo2 12954* | 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 12955* | 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 12956* | 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 12957* | Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦))) | ||
| Theorem | indstr 12958* | Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) | ||
| Theorem | eluznn0 12959 | Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0) | ||
| Theorem | eluznn 12960 | Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) | ||
| Theorem | eluz2b1 12961 | Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁)) | ||
| Theorem | eluz2gt1 12962 | An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁) | ||
| Theorem | eluz2b2 12963 | Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | ||
| Theorem | eluz2b3 12964 | Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) | ||
| Theorem | uz2m1nn 12965 | One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.) |
| ⊢ (𝑁 ∈ (ℤ≥‘2) → (𝑁 − 1) ∈ ℕ) | ||
| Theorem | 1nuz2 12966 | 1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.) |
| ⊢ ¬ 1 ∈ (ℤ≥‘2) | ||
| Theorem | elnn1uz2 12967 | A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
| ⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2))) | ||
| Theorem | uz2mulcl 12968 | Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.) |
| ⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2)) | ||
| Theorem | indstr2 12969* | Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012.) |
| ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜒 & ⊢ (𝑥 ∈ (ℤ≥‘2) → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) | ||
| Theorem | uzinfi 12970 | Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
| ⊢ 𝑀 ∈ ℤ ⇒ ⊢ inf((ℤ≥‘𝑀), ℝ, < ) = 𝑀 | ||
| Theorem | nninf 12971 | The infimum of the set of positive integers is one. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.) |
| ⊢ inf(ℕ, ℝ, < ) = 1 | ||
| Theorem | nn0inf 12972 | The infimum of the set of nonnegative integers is zero. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.) |
| ⊢ inf(ℕ0, ℝ, < ) = 0 | ||
| Theorem | infssuzle 12973 | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.) |
| ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝐴 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝐴) | ||
| Theorem | infssuzcl 12974 | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.) |
| ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → inf(𝑆, ℝ, < ) ∈ 𝑆) | ||
| Theorem | ublbneg 12975* | The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.) |
| ⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) | ||
| Theorem | eqreznegel 12976* | Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
| ⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴}) | ||
| Theorem | supminf 12977* | The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011.) ( Revised by AV, 13-Sep-2020.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) = -inf({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < )) | ||
| Theorem | lbzbi 12978* | If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.) |
| ⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | ||
| Theorem | zsupss 12979* | Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 11233.) (Contributed by Mario Carneiro, 21-Apr-2015.) |
| ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
| Theorem | suprzcl2 12980* | The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 12698 avoids ax-pre-sup 11233.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) |
| ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴) | ||
| Theorem | suprzub 12981* | The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) |
| ⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
| Theorem | uzsupss 12982* | Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 21-Apr-2015.) |
| ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ⊆ 𝑍 ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝑍 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝑍 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
| Theorem | nn01to3 12983 | A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ∧ 𝑁 ≤ 3) → (𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3)) | ||
| Theorem | nn0ge2m1nnALT 12984 | Alternate proof of nn0ge2m1nn 12596: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 12884, a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn 12596. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ) | ||
| Theorem | uzwo3 12985* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 12954 allows the lower bound 𝐵 to be any real number. See also nnwo 12955 and nnwos 12957. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.) |
| ⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
| Theorem | zmin 12986* | There is a unique smallest integer greater than or equal to a given real number. (Contributed by NM, 12-Nov-2004.) (Revised by Mario Carneiro, 13-Jun-2014.) |
| ⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ ∀𝑦 ∈ ℤ (𝐴 ≤ 𝑦 → 𝑥 ≤ 𝑦))) | ||
| Theorem | zmax 12987* | There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.) |
| ⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) | ||
| Theorem | zbtwnre 12988* | There is a unique integer between a real number and the number plus one. Exercise 5 of [Apostol] p. 28. (Contributed by NM, 13-Nov-2004.) |
| ⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝐴 ≤ 𝑥 ∧ 𝑥 < (𝐴 + 1))) | ||
| Theorem | rebtwnz 12989* | There is a unique greatest integer less than or equal to a real number. Exercise 4 of [Apostol] p. 28. (Contributed by NM, 15-Nov-2004.) |
| ⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ 𝐴 < (𝑥 + 1))) | ||
| Syntax | cq 12990 | Extend class notation to include the class of rationals. |
| class ℚ | ||
| Definition | df-q 12991 | Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 12992 for the relation "is rational". (Contributed by NM, 8-Jan-2002.) |
| ⊢ ℚ = ( / “ (ℤ × ℕ)) | ||
| Theorem | elq 12992* | Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.) |
| ⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) | ||
| Theorem | qmulz 12993* | If 𝐴 is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 22-Jul-2014.) |
| ⊢ (𝐴 ∈ ℚ → ∃𝑥 ∈ ℕ (𝐴 · 𝑥) ∈ ℤ) | ||
| Theorem | znq 12994 | The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) | ||
| Theorem | qre 12995 | A rational number is a real number. (Contributed by NM, 14-Nov-2002.) |
| ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) | ||
| Theorem | zq 12996 | An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.) |
| ⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) | ||
| Theorem | qred 12997 | A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℚ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
| Theorem | zssq 12998 | The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.) |
| ⊢ ℤ ⊆ ℚ | ||
| Theorem | nn0ssq 12999 | The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
| ⊢ ℕ0 ⊆ ℚ | ||
| Theorem | nnssq 13000 | The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
| ⊢ ℕ ⊆ ℚ | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |