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