Home | Metamath
Proof Explorer Theorem List (p. 117 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elnn0uz 11601 | A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0)) | ||
Theorem | eluz2nn 11602 | An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ) | ||
Theorem | eluzge2nn0 11603 | 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 11604 | An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → 𝑁 ≠ 0) | ||
Theorem | uzuzle23 11605 | 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 11606 | 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 11607 | An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn 11639. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) | ||
Theorem | 1eluzge0 11608 | 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ 1 ∈ (ℤ≥‘0) | ||
Theorem | 2eluzge0 11609 | 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 11610 | 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ 2 ∈ (ℤ≥‘1) | ||
Theorem | uznnssnn 11611 | The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) |
⊢ (𝑁 ∈ ℕ → (ℤ≥‘𝑁) ⊆ ℕ) | ||
Theorem | raluz 11612* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
Theorem | raluz2 11613* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (∀𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ → ∀𝑛 ∈ ℤ (𝑀 ≤ 𝑛 → 𝜑))) | ||
Theorem | rexuz 11614* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
Theorem | rexuz2 11615* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
⊢ (∃𝑛 ∈ (ℤ≥‘𝑀)𝜑 ↔ (𝑀 ∈ ℤ ∧ ∃𝑛 ∈ ℤ (𝑀 ≤ 𝑛 ∧ 𝜑))) | ||
Theorem | 2rexuz 11616* | Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.) |
⊢ (∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)𝜑 ↔ ∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ (𝑚 ≤ 𝑛 ∧ 𝜑)) | ||
Theorem | peano2uz 11617 | Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀)) | ||
Theorem | peano2uzs 11618 | Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) | ||
Theorem | peano2uzr 11619 | Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) | ||
Theorem | uzaddcl 11620 | Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.) |
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℕ0) → (𝑁 + 𝐾) ∈ (ℤ≥‘𝑀)) | ||
Theorem | nn0pzuz 11621 | 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 11622* | 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 11623* | 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 11622 or uzind4ALT 11623 may be used; see comment for nnind 10915. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzind4s 11624* | 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 11625* | 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 11624 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.) |
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) | ||
Theorem | uzind4i 11626* | Induction on the upper integers that start at 𝑀. The first hypothesis specifies the lower bound, the next four give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 4-Sep-2005.) |
⊢ 𝑀 ∈ ℤ & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzwo 11627* | Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by NM, 8-Oct-2005.) |
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) | ||
Theorem | uzwo2 11628* | 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 11629* | 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 11630* | 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 11631* | Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦))) | ||
Theorem | indstr 11632* | Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) | ||
Theorem | eluznn0 11633 | Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0) | ||
Theorem | eluznn 11634 | Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) | ||
Theorem | eluz2b1 11635 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁)) | ||
Theorem | eluz2gt1 11636 | An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁) | ||
Theorem | eluz2b2 11637 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | ||
Theorem | eluz2b3 11638 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) | ||
Theorem | uz2m1nn 11639 | 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 11640 | 1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.) |
⊢ ¬ 1 ∈ (ℤ≥‘2) | ||
Theorem | elnn1uz2 11641 | A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2))) | ||
Theorem | uz2mulcl 11642 | Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2)) | ||
Theorem | indstr2 11643* | 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 11644 | 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 11645 | 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 11646 | 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 11647 | 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 11648 | 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 11649* | The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) | ||
Theorem | eqreznegel 11650* | Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴}) | ||
Theorem | supminf 11651* | 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 11652* | If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | ||
Theorem | zsupss 11653* | Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 9893.) (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | suprzcl2 11654* | The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 11333 avoids ax-pre-sup 9893.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴) | ||
Theorem | suprzub 11655* | 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 11656* | 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 11657 | 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 11658 | Alternate proof of nn0ge2m1nn 11237: 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 11569, 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 11237. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ) | ||
Theorem | uzwo3 11659* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 11628 allows the lower bound 𝐵 to be any real number. See also nnwo 11629 and nnwos 11631. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.) |
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | zmin 11660* | 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 11661* | There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) | ||
Theorem | zbtwnre 11662* | 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 11663* | 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 11664 | Extend class notation to include the class of rationals. |
class ℚ | ||
Definition | df-q 11665 | Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 11666 for the relation "is rational." (Contributed by NM, 8-Jan-2002.) |
⊢ ℚ = ( / “ (ℤ × ℕ)) | ||
Theorem | elq 11666* | Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.) |
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) | ||
Theorem | qmulz 11667* | 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 11668 | The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) | ||
Theorem | qre 11669 | A rational number is a real number. (Contributed by NM, 14-Nov-2002.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) | ||
Theorem | zq 11670 | An integer is a rational number. (Contributed by NM, 9-Jan-2002.) |
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) | ||
Theorem | zssq 11671 | The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.) |
⊢ ℤ ⊆ ℚ | ||
Theorem | nn0ssq 11672 | The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
⊢ ℕ0 ⊆ ℚ | ||
Theorem | nnssq 11673 | The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
⊢ ℕ ⊆ ℚ | ||
Theorem | qssre 11674 | The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.) |
⊢ ℚ ⊆ ℝ | ||
Theorem | qsscn 11675 | The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
⊢ ℚ ⊆ ℂ | ||
Theorem | qex 11676 | The set of rational numbers exists. See also qexALT 11679. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ℚ ∈ V | ||
Theorem | nnq 11677 | A positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) | ||
Theorem | qcn 11678 | A rational number is a complex number. (Contributed by NM, 2-Aug-2004.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) | ||
Theorem | qexALT 11679 | Alternate proof of qex 11676. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℚ ∈ V | ||
Theorem | qaddcl 11680 | Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) | ||
Theorem | qnegcl 11681 | Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ) | ||
Theorem | qmulcl 11682 | Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) | ||
Theorem | qsubcl 11683 | Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) | ||
Theorem | qreccl 11684 | Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) | ||
Theorem | qdivcl 11685 | Closure of division of rationals. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) | ||
Theorem | qrevaddcl 11686 | Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.) |
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) | ||
Theorem | nnrecq 11687 | The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ) | ||
Theorem | irradd 11688 | The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.) |
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ)) | ||
Theorem | irrmul 11689 | The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.) |
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ)) | ||
Theorem | rpnnen1lem2 11690* | Lemma for rpnnen1 11696. (Contributed by Mario Carneiro, 12-May-2013.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(𝑇, ℝ, < ) ∈ ℤ) | ||
Theorem | rpnnen1lem1 11691* | Lemma for rpnnen1 11696. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑𝑚 ℕ)) | ||
Theorem | rpnnen1lem3 11692* | Lemma for rpnnen1 11696. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥) | ||
Theorem | rpnnen1lem4 11693* | Lemma for rpnnen1 11696. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ) | ||
Theorem | rpnnen1lem5 11694* | Lemma for rpnnen1 11696. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥) | ||
Theorem | rpnnen1lem6 11695* | Lemma for rpnnen1 11696. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ ℝ ≼ (ℚ ↑𝑚 ℕ) | ||
Theorem | rpnnen1 11696 | One half of rpnnen 14795, where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number 𝑥 to the sequence (𝐹‘𝑥):ℕ⟶ℚ (see rpnnen1lem6 11695) such that ((𝐹‘𝑥)‘𝑘) is the largest rational number with denominator 𝑘 that is strictly less than 𝑥. In this manner, we get a monotonically increasing sequence that converges to 𝑥, and since each sequence converges to a unique real number, this mapping from reals to sequences of rational numbers is injective. Note: The ℕ and ℚ existence hypotheses provide for use with either nnex 10903 and qex 11676, or nnexALT 10899 and qexALT 11679. The proof should not be modified to use any of those 4 theorems. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 16-Jun-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.) |
⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ ℝ ≼ (ℚ ↑𝑚 ℕ) | ||
Theorem | rpnnen1lem1OLD 11697* | Lemma for rpnnen1OLD 11701. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem1 11691 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑𝑚 ℕ)) | ||
Theorem | rpnnen1lem3OLD 11698* | Lemma for rpnnen1OLD 11701. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem3 11692 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥) | ||
Theorem | rpnnen1lem4OLD 11699* | Lemma for rpnnen1OLD 11701. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem4 11693 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ) | ||
Theorem | rpnnen1lem5OLD 11700* | Lemma for rpnnen1OLD 11701. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem5 11694 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |