Home | Metamath
Proof Explorer Theorem List (p. 124 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 | uzind4ALT 12301* | 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 12300 or uzind4ALT 12301 may be used; see comment for nnind 11650. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑀 ∈ ℤ → 𝜓) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) & ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzind4s 12302* | 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 12303* | 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 12302 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.) |
⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑) & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) | ||
Theorem | uzind4i 12304* | 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 12300 assuming that 𝜓 holds unconditionally. Notice that 𝑁 ∈ (ℤ≥‘𝑀) implies that the lower bound 𝑀 is an integer (𝑀 ∈ ℤ, see eluzel2 12242). (Contributed by NM, 4-Sep-2005.) (Revised by AV, 13-Jul-2022.) |
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝜒 → 𝜃)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝜏) | ||
Theorem | uzwo 12305* | Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) |
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ 𝑆 ≠ ∅) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) | ||
Theorem | uzwo2 12306* | 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 12307* | 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 12308* | 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 12309* | Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ℕ 𝜑 → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦))) | ||
Theorem | indstr 12310* | Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)) ⇒ ⊢ (𝑥 ∈ ℕ → 𝜑) | ||
Theorem | eluznn0 12311 | Membership in a nonnegative upper set of integers implies membership in ℕ0. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ0) | ||
Theorem | eluznn 12312 | Membership in a positive upper set of integers implies membership in ℕ. (Contributed by JJ, 1-Oct-2018.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ ℕ) | ||
Theorem | eluz2b1 12313 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℤ ∧ 1 < 𝑁)) | ||
Theorem | eluz2gt1 12314 | An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → 1 < 𝑁) | ||
Theorem | eluz2b2 12315 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | ||
Theorem | eluz2b3 12316 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
⊢ (𝑁 ∈ (ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 𝑁 ≠ 1)) | ||
Theorem | uz2m1nn 12317 | 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 12318 | 1 is not in (ℤ≥‘2). (Contributed by Paul Chapman, 21-Nov-2012.) |
⊢ ¬ 1 ∈ (ℤ≥‘2) | ||
Theorem | elnn1uz2 12319 | A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 = 1 ∨ 𝑁 ∈ (ℤ≥‘2))) | ||
Theorem | uz2mulcl 12320 | Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑀 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑀 · 𝑁) ∈ (ℤ≥‘2)) | ||
Theorem | indstr2 12321* | 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 12322 | 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 12323 | 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 12324 | 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 12325 | 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 12326 | 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 12327* | The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}𝑥 ≤ 𝑦) | ||
Theorem | eqreznegel 12328* | Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝐴 ⊆ ℤ → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} = {𝑧 ∈ ℤ ∣ -𝑧 ∈ 𝐴}) | ||
Theorem | supminf 12329* | 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 12330* | If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝐴 ⊆ ℝ → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)) | ||
Theorem | zsupss 12331* | Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 10609.) (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | suprzcl2 12332* | The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 12056 avoids ax-pre-sup 10609.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴) | ||
Theorem | suprzub 12333* | 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 12334* | 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 12335 | 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 12336 | Alternate proof of nn0ge2m1nn 11958: 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 12243, 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 11958. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ) | ||
Theorem | uzwo3 12337* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 12306 allows the lower bound 𝐵 to be any real number. See also nnwo 12307 and nnwos 12309. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.) |
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | zmin 12338* | 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 12339* | There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℤ (𝑥 ≤ 𝐴 ∧ ∀𝑦 ∈ ℤ (𝑦 ≤ 𝐴 → 𝑦 ≤ 𝑥))) | ||
Theorem | zbtwnre 12340* | 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 12341* | 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 12342 | Extend class notation to include the class of rationals. |
class ℚ | ||
Definition | df-q 12343 | Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 12344 for the relation "is rational." (Contributed by NM, 8-Jan-2002.) |
⊢ ℚ = ( / “ (ℤ × ℕ)) | ||
Theorem | elq 12344* | Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.) |
⊢ (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) | ||
Theorem | qmulz 12345* | 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 12346 | The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) | ||
Theorem | qre 12347 | A rational number is a real number. (Contributed by NM, 14-Nov-2002.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℝ) | ||
Theorem | zq 12348 | An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.) |
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℚ) | ||
Theorem | zssq 12349 | The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.) |
⊢ ℤ ⊆ ℚ | ||
Theorem | nn0ssq 12350 | The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
⊢ ℕ0 ⊆ ℚ | ||
Theorem | nnssq 12351 | The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
⊢ ℕ ⊆ ℚ | ||
Theorem | qssre 12352 | The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.) |
⊢ ℚ ⊆ ℝ | ||
Theorem | qsscn 12353 | The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
⊢ ℚ ⊆ ℂ | ||
Theorem | qex 12354 | The set of rational numbers exists. See also qexALT 12357. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ ℚ ∈ V | ||
Theorem | nnq 12355 | A positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℚ) | ||
Theorem | qcn 12356 | A rational number is a complex number. (Contributed by NM, 2-Aug-2004.) |
⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) | ||
Theorem | qexALT 12357 | Alternate proof of qex 12354. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℚ ∈ V | ||
Theorem | qaddcl 12358 | Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ ℚ) | ||
Theorem | qnegcl 12359 | Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → -𝐴 ∈ ℚ) | ||
Theorem | qmulcl 12360 | Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℚ) | ||
Theorem | qsubcl 12361 | Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → (𝐴 − 𝐵) ∈ ℚ) | ||
Theorem | qreccl 12362 | Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℚ) | ||
Theorem | qdivcl 12363 | Closure of division of rationals. (Contributed by NM, 3-Aug-2004.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℚ) | ||
Theorem | qrevaddcl 12364 | Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.) |
⊢ (𝐵 ∈ ℚ → ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℚ) ↔ 𝐴 ∈ ℚ)) | ||
Theorem | nnrecq 12365 | The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
⊢ (𝐴 ∈ ℕ → (1 / 𝐴) ∈ ℚ) | ||
Theorem | irradd 12366 | The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.) |
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ) → (𝐴 + 𝐵) ∈ (ℝ ∖ ℚ)) | ||
Theorem | irrmul 12367 | The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.) |
⊢ ((𝐴 ∈ (ℝ ∖ ℚ) ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐴 · 𝐵) ∈ (ℝ ∖ ℚ)) | ||
Theorem | elpq 12368* | A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.) |
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) | ||
Theorem | elpqb 12369* | A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022.) |
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)) | ||
Theorem | rpnnen1lem2 12370* | Lemma for rpnnen1 12376. (Contributed by Mario Carneiro, 12-May-2013.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ ((𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ) → sup(𝑇, ℝ, < ) ∈ ℤ) | ||
Theorem | rpnnen1lem1 12371* | Lemma for rpnnen1 12376. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) ∈ (ℚ ↑m ℕ)) | ||
Theorem | rpnnen1lem3 12372* | Lemma for rpnnen1 12376. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → ∀𝑛 ∈ ran (𝐹‘𝑥)𝑛 ≤ 𝑥) | ||
Theorem | rpnnen1lem4 12373* | Lemma for rpnnen1 12376. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) ∈ ℝ) | ||
Theorem | rpnnen1lem5 12374* | Lemma for rpnnen1 12376. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ (𝑥 ∈ ℝ → sup(ran (𝐹‘𝑥), ℝ, < ) = 𝑥) | ||
Theorem | rpnnen1lem6 12375* | Lemma for rpnnen1 12376. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) & ⊢ ℕ ∈ V & ⊢ ℚ ∈ V ⇒ ⊢ ℝ ≼ (ℚ ↑m ℕ) | ||
Theorem | rpnnen1 12376 | One half of rpnnen 15574, 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 12375) 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 11638 and qex 12354, or nnexALT 11634 and qexALT 12357. 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 ⇒ ⊢ ℝ ≼ (ℚ ↑m ℕ) | ||
Theorem | reexALT 12377 | Alternate proof of reex 10622. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℝ ∈ V | ||
Theorem | cnref1o 12378* | There is a natural one-to-one mapping from (ℝ × ℝ) to ℂ, where we map 〈𝑥, 𝑦〉 to (𝑥 + (i · 𝑦)). In our construction of the complex numbers, this is in fact our definition of ℂ (see df-c 10537), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→ℂ | ||
Theorem | cnexALT 12379 | The set of complex numbers exists. This theorem shows that ax-cnex 10587 is redundant if we assume ax-rep 5182. See also ax-cnex 10587. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | xrex 12380 | The set of extended reals exists. (Contributed by NM, 24-Dec-2006.) |
⊢ ℝ* ∈ V | ||
Theorem | addex 12381 | The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ + ∈ V | ||
Theorem | mulex 12382 | The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ · ∈ V | ||
Syntax | crp 12383 | Extend class notation to include the class of positive reals. |
class ℝ+ | ||
Definition | df-rp 12384 | Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | ||
Theorem | elrp 12385 | Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | elrpii 12386 | Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈ ℝ+ | ||
Theorem | 1rp 12387 | 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.) |
⊢ 1 ∈ ℝ+ | ||
Theorem | 2rp 12388 | 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ 2 ∈ ℝ+ | ||
Theorem | 3rp 12389 | 3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 3 ∈ ℝ+ | ||
Theorem | rpssre 12390 | The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.) |
⊢ ℝ+ ⊆ ℝ | ||
Theorem | rpre 12391 | A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | ||
Theorem | rpxr 12392 | A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) | ||
Theorem | rpcn 12393 | A positive real is a complex number. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ) | ||
Theorem | nnrp 12394 | A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+) | ||
Theorem | rpgt0 12395 | A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.) |
⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | ||
Theorem | rpge0 12396 | A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.) |
⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴) | ||
Theorem | rpregt0 12397 | A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | rprege0 12398 | A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | ||
Theorem | rpne0 12399 | A positive real is nonzero. (Contributed by NM, 18-Jul-2008.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0) | ||
Theorem | rprene0 12400 | A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |