Home | Metamath
Proof Explorer Theorem List (p. 156 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tanneg 15501 | The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘-𝐴) = -(tan‘𝐴)) | ||
Theorem | sin0 15502 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
⊢ (sin‘0) = 0 | ||
Theorem | cos0 15503 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
⊢ (cos‘0) = 1 | ||
Theorem | tan0 15504 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
⊢ (tan‘0) = 0 | ||
Theorem | efival 15505 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) | ||
Theorem | efmival 15506 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴)))) | ||
Theorem | sinhval 15507 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → ((sin‘(i · 𝐴)) / i) = (((exp‘𝐴) − (exp‘-𝐴)) / 2)) | ||
Theorem | coshval 15508 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(i · 𝐴)) = (((exp‘𝐴) + (exp‘-𝐴)) / 2)) | ||
Theorem | resinhcl 15509 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → ((sin‘(i · 𝐴)) / i) ∈ ℝ) | ||
Theorem | rpcoshcl 15510 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ+) | ||
Theorem | recoshcl 15511 | The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ) | ||
Theorem | retanhcl 15512 | The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ ℝ) | ||
Theorem | tanhlt1 15513 | The hyperbolic tangent of a real number is upper bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) < 1) | ||
Theorem | tanhbnd 15514 | The hyperbolic tangent of a real number is bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ (-1(,)1)) | ||
Theorem | efeul 15515 | Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.) |
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = ((exp‘(ℜ‘𝐴)) · ((cos‘(ℑ‘𝐴)) + (i · (sin‘(ℑ‘𝐴)))))) | ||
Theorem | efieq 15516 | The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((exp‘(i · 𝐴)) = (exp‘(i · 𝐵)) ↔ ((cos‘𝐴) = (cos‘𝐵) ∧ (sin‘𝐴) = (sin‘𝐵)))) | ||
Theorem | sinadd 15517 | Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) | ||
Theorem | cosadd 15518 | Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) | ||
Theorem | tanaddlem 15519 | A useful intermediate step in tanadd 15520 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) ≠ 0 ∧ (cos‘𝐵) ≠ 0)) → ((cos‘(𝐴 + 𝐵)) ≠ 0 ↔ ((tan‘𝐴) · (tan‘𝐵)) ≠ 1)) | ||
Theorem | tanadd 15520 | Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) ≠ 0 ∧ (cos‘𝐵) ≠ 0 ∧ (cos‘(𝐴 + 𝐵)) ≠ 0)) → (tan‘(𝐴 + 𝐵)) = (((tan‘𝐴) + (tan‘𝐵)) / (1 − ((tan‘𝐴) · (tan‘𝐵))))) | ||
Theorem | sinsub 15521 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵)))) | ||
Theorem | cossub 15522 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵)))) | ||
Theorem | addsin 15523 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 · ((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | subsin 15524 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | sinmul 15525 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 15518 and cossub 15522. (Contributed by David A. Wheeler, 26-May-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2)) | ||
Theorem | cosmul 15526 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 15518 and cossub 15522. (Contributed by David A. Wheeler, 26-May-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2)) | ||
Theorem | addcos 15527 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) + (cos‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | subcos 15528 | Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐵) − (cos‘𝐴)) = (2 · ((sin‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) | ||
Theorem | sincossq 15529 | Sine squared plus cosine squared is 1. Equation 17 of [Gleason] p. 311. Note that this holds for non-real arguments, even though individually each term is unbounded. (Contributed by NM, 15-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1) | ||
Theorem | sin2t 15530 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(2 · 𝐴)) = (2 · ((sin‘𝐴) · (cos‘𝐴)))) | ||
Theorem | cos2t 15531 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = ((2 · ((cos‘𝐴)↑2)) − 1)) | ||
Theorem | cos2tsin 15532 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = (1 − (2 · ((sin‘𝐴)↑2)))) | ||
Theorem | sinbnd 15533 | The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → (-1 ≤ (sin‘𝐴) ∧ (sin‘𝐴) ≤ 1)) | ||
Theorem | cosbnd 15534 | The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → (-1 ≤ (cos‘𝐴) ∧ (cos‘𝐴) ≤ 1)) | ||
Theorem | sinbnd2 15535 | The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ (-1[,]1)) | ||
Theorem | cosbnd2 15536 | The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ (-1[,]1)) | ||
Theorem | ef01bndlem 15537* | Lemma for sin01bnd 15538 and cos01bnd 15539. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ (0(,]1) → (abs‘Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)) < ((𝐴↑4) / 6)) | ||
Theorem | sin01bnd 15538 | Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝐴 ∈ (0(,]1) → ((𝐴 − ((𝐴↑3) / 3)) < (sin‘𝐴) ∧ (sin‘𝐴) < 𝐴)) | ||
Theorem | cos01bnd 15539 | Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝐴 ∈ (0(,]1) → ((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) / 3)))) | ||
Theorem | cos1bnd 15540 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ ((1 / 3) < (cos‘1) ∧ (cos‘1) < (2 / 3)) | ||
Theorem | cos2bnd 15541 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (-(7 / 9) < (cos‘2) ∧ (cos‘2) < -(1 / 9)) | ||
Theorem | sinltx 15542 | The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014.) |
⊢ (𝐴 ∈ ℝ+ → (sin‘𝐴) < 𝐴) | ||
Theorem | sin01gt0 15543 | The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Wolf Lammen, 25-Sep-2020.) |
⊢ (𝐴 ∈ (0(,]1) → 0 < (sin‘𝐴)) | ||
Theorem | cos01gt0 15544 | The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (𝐴 ∈ (0(,]1) → 0 < (cos‘𝐴)) | ||
Theorem | sin02gt0 15545 | The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (𝐴 ∈ (0(,]2) → 0 < (sin‘𝐴)) | ||
Theorem | sincos1sgn 15546 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (0 < (sin‘1) ∧ 0 < (cos‘1)) | ||
Theorem | sincos2sgn 15547 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (0 < (sin‘2) ∧ (cos‘2) < 0) | ||
Theorem | sin4lt0 15548 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
⊢ (sin‘4) < 0 | ||
Theorem | absefi 15549 | The absolute value of the exponential of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.) |
⊢ (𝐴 ∈ ℝ → (abs‘(exp‘(i · 𝐴))) = 1) | ||
Theorem | absef 15550 | The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007.) |
⊢ (𝐴 ∈ ℂ → (abs‘(exp‘𝐴)) = (exp‘(ℜ‘𝐴))) | ||
Theorem | absefib 15551 | A complex number is real iff the exponential of its product with i has absolute value one. (Contributed by NM, 21-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (abs‘(exp‘(i · 𝐴))) = 1)) | ||
Theorem | efieq1re 15552 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ (exp‘(i · 𝐴)) = 1) → 𝐴 ∈ ℝ) | ||
Theorem | demoivre 15553 | De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 15554 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) | ||
Theorem | demoivreALT 15554 | Alternate proof of demoivre 15553. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) | ||
Syntax | ctau 15555 | Extend class notation to include the constant tau, τ = 6.28318.... |
class τ | ||
Definition | df-tau 15556 | Define the circle constant tau, τ = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including τ, a three-legged variant of π, or 2π. Note the difference between this constant τ and the formula variable 𝜏. Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.) |
⊢ τ = inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < ) | ||
Theorem | eirrlem 15557* | Lemma for eirr 15558. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛))) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℕ) & ⊢ (𝜑 → e = (𝑃 / 𝑄)) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | eirr 15558 | e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.) |
⊢ e ∉ ℚ | ||
Theorem | egt2lt3 15559 | Euler's constant e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
⊢ (2 < e ∧ e < 3) | ||
Theorem | epos 15560 | Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
⊢ 0 < e | ||
Theorem | epr 15561 | Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
⊢ e ∈ ℝ+ | ||
Theorem | ene0 15562 | e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
⊢ e ≠ 0 | ||
Theorem | ene1 15563 | e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
⊢ e ≠ 1 | ||
Theorem | xpnnen 15564 | The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
⊢ (ℕ × ℕ) ≈ ℕ | ||
Theorem | znnen 15565 | The set of integers and the set of positive integers are equinumerous. Exercise 1 of [Gleason] p. 140. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.) |
⊢ ℤ ≈ ℕ | ||
Theorem | qnnen 15566 | The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set (ℤ × ℕ) is numerable. Exercise 2 of [Enderton] p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 3-Mar-2013.) |
⊢ ℚ ≈ ℕ | ||
Theorem | rpnnen2lem1 15567* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝐴)‘𝑁) = if(𝑁 ∈ 𝐴, ((1 / 3)↑𝑁), 0)) | ||
Theorem | rpnnen2lem2 15568* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ (𝐴 ⊆ ℕ → (𝐹‘𝐴):ℕ⟶ℝ) | ||
Theorem | rpnnen2lem3 15569* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ seq1( + , (𝐹‘ℕ)) ⇝ (1 / 2) | ||
Theorem | rpnnen2lem4 15570* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → (0 ≤ ((𝐹‘𝐴)‘𝑘) ∧ ((𝐹‘𝐴)‘𝑘) ≤ ((𝐹‘𝐵)‘𝑘))) | ||
Theorem | rpnnen2lem5 15571* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → seq𝑀( + , (𝐹‘𝐴)) ∈ dom ⇝ ) | ||
Theorem | rpnnen2lem6 15572* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘) ∈ ℝ) | ||
Theorem | rpnnen2lem7 15573* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐵)‘𝑘)) | ||
Theorem | rpnnen2lem8 15574* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = (Σ𝑘 ∈ (1...(𝑀 − 1))((𝐹‘𝐴)‘𝑘) + Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘))) | ||
Theorem | rpnnen2lem9 15575* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = (0 + (((1 / 3)↑(𝑀 + 1)) / (1 − (1 / 3))))) | ||
Theorem | rpnnen2lem10 15576* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝐵 ⊆ ℕ) & ⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵))) & ⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘)) | ||
Theorem | rpnnen2lem11 15577* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) & ⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → 𝐵 ⊆ ℕ) & ⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵)) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵))) & ⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | rpnnen2lem12 15578* | Lemma for rpnnen2 15579. (Contributed by Mario Carneiro, 13-May-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0))) ⇒ ⊢ 𝒫 ℕ ≼ (0[,]1) | ||
Theorem | rpnnen2 15579 |
The other half of rpnnen 15580, where we show an injection from sets of
positive integers to real numbers. The obvious choice for this is
binary expansion, but it has the unfortunate property that it does not
produce an injection on numbers which end with all 0's or all 1's (the
more well-known decimal version of this is 0.999... 15237). Instead, we
opt for a ternary expansion, which produces (a scaled version of) the
Cantor set. Since the Cantor set is riddled with gaps, we can show that
any two sequences that are not equal must differ somewhere, and when
they do, they are placed a finite distance apart, thus ensuring that the
map is injective.
Our map assigns to each subset 𝐴 of the positive integers the number Σ𝑘 ∈ 𝐴(3↑-𝑘) = Σ𝑘 ∈ ℕ((𝐹‘𝐴)‘𝑘), where ((𝐹‘𝐴)‘𝑘) = if(𝑘 ∈ 𝐴, (3↑-𝑘), 0)) (rpnnen2lem1 15567). This is an infinite sum of real numbers (rpnnen2lem2 15568), and since 𝐴 ⊆ 𝐵 implies (𝐹‘𝐴) ≤ (𝐹‘𝐵) (rpnnen2lem4 15570) and (𝐹‘ℕ) converges to 1 / 2 (rpnnen2lem3 15569) by geoisum1 15235, the sum is convergent to some real (rpnnen2lem5 15571 and rpnnen2lem6 15572) by the comparison test for convergence cvgcmp 15171. The comparison test also tells us that 𝐴 ⊆ 𝐵 implies Σ(𝐹‘𝐴) ≤ Σ(𝐹‘𝐵) (rpnnen2lem7 15573). Putting it all together, if we have two sets 𝑥 ≠ 𝑦, there must differ somewhere, and so there must be an 𝑚 such that ∀𝑛 < 𝑚(𝑛 ∈ 𝑥 ↔ 𝑛 ∈ 𝑦) but 𝑚 ∈ (𝑥 ∖ 𝑦) or vice versa. In this case, we split off the first 𝑚 − 1 terms (rpnnen2lem8 15574) and cancel them (rpnnen2lem10 15576), since these are the same for both sets. For the remaining terms, we use the subset property to establish that Σ(𝐹‘𝑦) ≤ Σ(𝐹‘(ℕ ∖ {𝑚})) and Σ(𝐹‘{𝑚}) ≤ Σ(𝐹‘𝑥) (where these sums are only over (ℤ≥‘𝑚)), and since Σ(𝐹‘(ℕ ∖ {𝑚})) = (3↑-𝑚) / 2 (rpnnen2lem9 15575) and Σ(𝐹‘{𝑚}) = (3↑-𝑚), we establish that Σ(𝐹‘𝑦) < Σ(𝐹‘𝑥) (rpnnen2lem11 15577) so that they must be different. By contraposition (rpnnen2lem12 15578), we find that this map is an injection. (Contributed by Mario Carneiro, 13-May-2013.) (Proof shortened by Mario Carneiro, 30-Apr-2014.) (Revised by NM, 17-Aug-2021.) |
⊢ 𝒫 ℕ ≼ (0[,]1) | ||
Theorem | rpnnen 15580 | The cardinality of the continuum is the same as the powerset of ω. This is a stronger statement than ruc 15596, which only asserts that ℝ is uncountable, i.e. has a cardinality larger than ω. The main proof is in two parts, rpnnen1 12383 and rpnnen2 15579, each showing an injection in one direction, and this last part uses sbth 8637 to prove that the sets are equinumerous. By constructing explicit injections, we avoid the use of AC. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ℝ ≈ 𝒫 ℕ | ||
Theorem | rexpen 15581 | The real numbers are equinumerous to their own Cartesian product, even though it is not necessarily true that ℝ is well-orderable (so we cannot use infxpidm2 9443 directly). (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) |
⊢ (ℝ × ℝ) ≈ ℝ | ||
Theorem | cpnnen 15582 | The complex numbers are equinumerous to the powerset of the positive integers. (Contributed by Mario Carneiro, 16-Jun-2013.) |
⊢ ℂ ≈ 𝒫 ℕ | ||
Theorem | rucALT 15583 | Alternate proof of ruc 15596. This proof is a simple corollary of rpnnen 15580, which determines the exact cardinality of the reals. For an alternate proof discussed at mmcomplex.html#uncountable 15580, see ruc 15596. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 13-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℕ ≺ ℝ | ||
Theorem | ruclem1 15584* | Lemma for ruc 15596 (the reals are uncountable). Substitutions for the function 𝐷. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Fan Zheng, 6-Jun-2016.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ 𝑋 = (1st ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ 𝑌 = (2nd ‘(〈𝐴, 𝐵〉𝐷𝑀)) ⇒ ⊢ (𝜑 → ((〈𝐴, 𝐵〉𝐷𝑀) ∈ (ℝ × ℝ) ∧ 𝑋 = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) ∧ 𝑌 = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵))) | ||
Theorem | ruclem2 15585* | Lemma for ruc 15596. Ordering property for the input to 𝐷. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ 𝑋 = (1st ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ 𝑌 = (2nd ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝑋 ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ 𝐵)) | ||
Theorem | ruclem3 15586* | Lemma for ruc 15596. The constructed interval [𝑋, 𝑌] always excludes 𝑀. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ 𝑋 = (1st ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ 𝑌 = (2nd ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝑀 < 𝑋 ∨ 𝑌 < 𝑀)) | ||
Theorem | ruclem4 15587* | Lemma for ruc 15596. Initial value of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) ⇒ ⊢ (𝜑 → (𝐺‘0) = 〈0, 1〉) | ||
Theorem | ruclem6 15588* | Lemma for ruc 15596. Domain and range of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) ⇒ ⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ × ℝ)) | ||
Theorem | ruclem7 15589* | Lemma for ruc 15596. Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) = ((𝐺‘𝑁)𝐷(𝐹‘(𝑁 + 1)))) | ||
Theorem | ruclem8 15590* | Lemma for ruc 15596. The intervals of the 𝐺 sequence are all nonempty. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁))) | ||
Theorem | ruclem9 15591* | Lemma for ruc 15596. The first components of the 𝐺 sequence are increasing, and the second components are decreasing. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑁)) ∧ (2nd ‘(𝐺‘𝑁)) ≤ (2nd ‘(𝐺‘𝑀)))) | ||
Theorem | ruclem10 15592* | Lemma for ruc 15596. Every first component of the 𝐺 sequence is less than every second component. That is, the sequences form a chain a1 < a2 <... < b2 < b1, where ai are the first components and bi are the second components. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (1st ‘(𝐺‘𝑀)) < (2nd ‘(𝐺‘𝑁))) | ||
Theorem | ruclem11 15593* | Lemma for ruc 15596. Closure lemmas for supremum. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) ⇒ ⊢ (𝜑 → (ran (1st ∘ 𝐺) ⊆ ℝ ∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1)) | ||
Theorem | ruclem12 15594* | Lemma for ruc 15596. The supremum of the increasing sequence 1st ∘ 𝐺 is a real number that is not in the range of 𝐹. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ 𝐶 = ({〈0, 〈0, 1〉〉} ∪ 𝐹) & ⊢ 𝐺 = seq0(𝐷, 𝐶) & ⊢ 𝑆 = sup(ran (1st ∘ 𝐺), ℝ, < ) ⇒ ⊢ (𝜑 → 𝑆 ∈ (ℝ ∖ ran 𝐹)) | ||
Theorem | ruclem13 15595 | Lemma for ruc 15596. There is no function that maps ℕ onto ℝ. (Use nex 1801 if you want this in the form ¬ ∃𝑓𝑓:ℕ–onto→ℝ.) (Contributed by NM, 14-Oct-2004.) (Proof shortened by Fan Zheng, 6-Jun-2016.) |
⊢ ¬ 𝐹:ℕ–onto→ℝ | ||
Theorem | ruc 15596 | The set of positive integers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 15584 through ruclem13 15595 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 15595 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable 15595. For an alternate proof see rucALT 15583. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.) |
⊢ ℕ ≺ ℝ | ||
Theorem | resdomq 15597 | The set of rationals is strictly less equinumerous than the set of reals (ℝ strictly dominates ℚ). (Contributed by NM, 18-Dec-2004.) |
⊢ ℚ ≺ ℝ | ||
Theorem | aleph1re 15598 | There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.) |
⊢ (ℵ‘1o) ≼ ℝ | ||
Theorem | aleph1irr 15599 | There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.) |
⊢ (ℵ‘1o) ≼ (ℝ ∖ ℚ) | ||
Theorem | cnso 15600 | The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ ∃𝑥 𝑥 Or ℂ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |