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