![]() |
Metamath
Proof Explorer Theorem List (p. 162 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tanval2 16101 | Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) = (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (i Β· ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) | ||
Theorem | tanval3 16102 | Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ ((expβ(2 Β· (i Β· π΄))) + 1) β 0) β (tanβπ΄) = (((expβ(2 Β· (i Β· π΄))) β 1) / (i Β· ((expβ(2 Β· (i Β· π΄))) + 1)))) | ||
Theorem | resinval 16103 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | recosval 16104 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | efi4p 16105* | Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β β β (expβ(i Β· π΄)) = (((1 β ((π΄β2) / 2)) + (i Β· (π΄ β ((π΄β3) / 6)))) + Ξ£π β (β€β₯β4)(πΉβπ))) | ||
Theorem | resin4p 16106* | Separate out the first four terms of the infinite series expansion of the sine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β β β (sinβπ΄) = ((π΄ β ((π΄β3) / 6)) + (ββΞ£π β (β€β₯β4)(πΉβπ)))) | ||
Theorem | recos4p 16107* | Separate out the first four terms of the infinite series expansion of the cosine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β β β (cosβπ΄) = ((1 β ((π΄β2) / 2)) + (ββΞ£π β (β€β₯β4)(πΉβπ)))) | ||
Theorem | resincl 16108 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | recoscl 16109 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | retancl 16110 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) β 0) β (tanβπ΄) β β) | ||
Theorem | resincld 16111 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | recoscld 16112 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | retancld 16113 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) β 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | sinneg 16114 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβ-π΄) = -(sinβπ΄)) | ||
Theorem | cosneg 16115 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβ-π΄) = (cosβπ΄)) | ||
Theorem | tanneg 16116 | 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 16117 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
β’ (sinβ0) = 0 | ||
Theorem | cos0 16118 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
β’ (cosβ0) = 1 | ||
Theorem | tan0 16119 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
β’ (tanβ0) = 0 | ||
Theorem | efival 16120 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) | ||
Theorem | efmival 16121 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
β’ (π΄ β β β (expβ(-i Β· π΄)) = ((cosβπ΄) β (i Β· (sinβπ΄)))) | ||
Theorem | sinhval 16122 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((sinβ(i Β· π΄)) / i) = (((expβπ΄) β (expβ-π΄)) / 2)) | ||
Theorem | coshval 16123 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) = (((expβπ΄) + (expβ-π΄)) / 2)) | ||
Theorem | resinhcl 16124 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((sinβ(i Β· π΄)) / i) β β) | ||
Theorem | rpcoshcl 16125 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) β β+) | ||
Theorem | recoshcl 16126 | The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β (cosβ(i Β· π΄)) β β) | ||
Theorem | retanhcl 16127 | The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ (π΄ β β β ((tanβ(i Β· π΄)) / i) β β) | ||
Theorem | tanhlt1 16128 | 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 16129 | 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 16130 | 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 16131 | 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 16132 | 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 16133 | 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 16134 | A useful intermediate step in tanadd 16135 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 16135 | 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 16136 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (sinβ(π΄ β π΅)) = (((sinβπ΄) Β· (cosβπ΅)) β ((cosβπ΄) Β· (sinβπ΅)))) | ||
Theorem | cossub 16137 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (cosβ(π΄ β π΅)) = (((cosβπ΄) Β· (cosβπ΅)) + ((sinβπ΄) Β· (sinβπ΅)))) | ||
Theorem | addsin 16138 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) + (sinβπ΅)) = (2 Β· ((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) | ||
Theorem | subsin 16139 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) β (sinβπ΅)) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) | ||
Theorem | sinmul 16140 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 16133 and cossub 16137. (Contributed by David A. Wheeler, 26-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (sinβπ΅)) = (((cosβ(π΄ β π΅)) β (cosβ(π΄ + π΅))) / 2)) | ||
Theorem | cosmul 16141 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 16133 and cossub 16137. (Contributed by David A. Wheeler, 26-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΄) Β· (cosβπ΅)) = (((cosβ(π΄ β π΅)) + (cosβ(π΄ + π΅))) / 2)) | ||
Theorem | addcos 16142 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΄) + (cosβπ΅)) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) | ||
Theorem | subcos 16143 | 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 16144 | 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 16145 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
β’ (π΄ β β β (sinβ(2 Β· π΄)) = (2 Β· ((sinβπ΄) Β· (cosβπ΄)))) | ||
Theorem | cos2t 16146 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ(2 Β· π΄)) = ((2 Β· ((cosβπ΄)β2)) β 1)) | ||
Theorem | cos2tsin 16147 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
β’ (π΄ β β β (cosβ(2 Β· π΄)) = (1 β (2 Β· ((sinβπ΄)β2)))) | ||
Theorem | sinbnd 16148 | 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 16149 | 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 16150 | 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 16151 | 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 16152* | Lemma for sin01bnd 16153 and cos01bnd 16154. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β (0(,]1) β (absβΞ£π β (β€β₯β4)(πΉβπ)) < ((π΄β4) / 6)) | ||
Theorem | sin01bnd 16153 | 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 16154 | 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 16155 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ ((1 / 3) < (cosβ1) β§ (cosβ1) < (2 / 3)) | ||
Theorem | cos2bnd 16156 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (-(7 / 9) < (cosβ2) β§ (cosβ2) < -(1 / 9)) | ||
Theorem | sinltx 16157 | The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014.) |
β’ (π΄ β β+ β (sinβπ΄) < π΄) | ||
Theorem | sin01gt0 16158 | 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 16159 | 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 16160 | 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 16161 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (0 < (sinβ1) β§ 0 < (cosβ1)) | ||
Theorem | sincos2sgn 16162 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (0 < (sinβ2) β§ (cosβ2) < 0) | ||
Theorem | sin4lt0 16163 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (sinβ4) < 0 | ||
Theorem | absefi 16164 | 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 16165 | 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 16166 | 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 16167 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
β’ ((π΄ β β β§ (expβ(i Β· π΄)) = 1) β π΄ β β) | ||
Theorem | demoivre 16168 | 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 16169 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
β’ ((π΄ β β β§ π β β€) β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) | ||
Theorem | demoivreALT 16169 | Alternate proof of demoivre 16168. 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 16170 | Extend class notation to include the constant tau, Ο = 6.28318.... |
class Ο | ||
Definition | df-tau 16171 | 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 16172* | Lemma for eirr 16173. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (1 / (!βπ))) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β e = (π / π)) β β’ Β¬ π | ||
Theorem | eirr 16173 | e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.) |
β’ e β β | ||
Theorem | egt2lt3 16174 | Euler's constant e = 2.71828... is strictly bounded below by 2 and above by 3. (Contributed by NM, 28-Nov-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ (2 < e β§ e < 3) | ||
Theorem | epos 16175 | Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
β’ 0 < e | ||
Theorem | epr 16176 | Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
β’ e β β+ | ||
Theorem | ene0 16177 | e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
β’ e β 0 | ||
Theorem | ene1 16178 | e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
β’ e β 1 | ||
Theorem | xpnnen 16179 | 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 16180 | 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 16181 | 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 16182* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β ((πΉβπ΄)βπ) = if(π β π΄, ((1 / 3)βπ), 0)) | ||
Theorem | rpnnen2lem2 16183* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ (π΄ β β β (πΉβπ΄):ββΆβ) | ||
Theorem | rpnnen2lem3 16184* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ seq1( + , (πΉββ)) β (1 / 2) | ||
Theorem | rpnnen2lem4 16185* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β π΅ β§ π΅ β β β§ π β β) β (0 β€ ((πΉβπ΄)βπ) β§ ((πΉβπ΄)βπ) β€ ((πΉβπ΅)βπ))) | ||
Theorem | rpnnen2lem5 16186* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β seqπ( + , (πΉβπ΄)) β dom β ) | ||
Theorem | rpnnen2lem6 16187* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) β β) | ||
Theorem | rpnnen2lem7 16188* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β π΅ β§ π΅ β β β§ π β β) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) β€ Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) | ||
Theorem | rpnnen2lem8 16189* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β Ξ£π β β ((πΉβπ΄)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΄)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) | ||
Theorem | rpnnen2lem9 16190* | Lemma for rpnnen2 16194. (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 16191* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β (π΄ β π΅)) & β’ (π β βπ β β (π < π β (π β π΄ β π β π΅))) & β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = Ξ£π β β ((πΉβπ΅)βπ)) β β’ ((π β§ π) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) = Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) | ||
Theorem | rpnnen2lem11 16192* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β (π΄ β π΅)) & β’ (π β βπ β β (π < π β (π β π΄ β π β π΅))) & β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = Ξ£π β β ((πΉβπ΅)βπ)) β β’ (π β Β¬ π) | ||
Theorem | rpnnen2lem12 16193* | Lemma for rpnnen2 16194. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ π« β βΌ (0[,]1) | ||
Theorem | rpnnen2 16194 |
The other half of rpnnen 16195, 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... 15851). 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 16182). This is an infinite sum of real numbers (rpnnen2lem2 16183), and since π΄ β π΅ implies (πΉβπ΄) β€ (πΉβπ΅) (rpnnen2lem4 16185) and (πΉββ) converges to 1 / 2 (rpnnen2lem3 16184) by geoisum1 15849, the sum is convergent to some real (rpnnen2lem5 16186 and rpnnen2lem6 16187) by the comparison test for convergence cvgcmp 15786. The comparison test also tells us that π΄ β π΅ implies Ξ£(πΉβπ΄) β€ Ξ£(πΉβπ΅) (rpnnen2lem7 16188). 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 16189) and cancel them (rpnnen2lem10 16191), 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 16190) and Ξ£(πΉβ{π}) = (3β-π), we establish that Ξ£(πΉβπ¦) < Ξ£(πΉβπ₯) (rpnnen2lem11 16192) so that they must be different. By contraposition (rpnnen2lem12 16193), 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 16195 | The cardinality of the continuum is the same as the powerset of Ο. This is a stronger statement than ruc 16211, which only asserts that β is uncountable, i.e. has a cardinality larger than Ο. The main proof is in two parts, rpnnen1 12989 and rpnnen2 16194, each showing an injection in one direction, and this last part uses sbth 9109 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 16196 | 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 10032 directly). (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) |
β’ (β Γ β) β β | ||
Theorem | cpnnen 16197 | The complex numbers are equinumerous to the powerset of the positive integers. (Contributed by Mario Carneiro, 16-Jun-2013.) |
β’ β β π« β | ||
Theorem | rucALT 16198 | Alternate proof of ruc 16211. This proof is a simple corollary of rpnnen 16195, which determines the exact cardinality of the reals. For an alternate proof discussed at mmcomplex.html#uncountable 16195, see ruc 16211. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 13-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β βΊ β | ||
Theorem | ruclem1 16199* | Lemma for ruc 16211 (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 16200* | Lemma for ruc 16211. Ordering property for the input to π·. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (1st β(β¨π΄, π΅β©π·π)) & β’ π = (2nd β(β¨π΄, π΅β©π·π)) & β’ (π β π΄ < π΅) β β’ (π β (π΄ β€ π β§ π < π β§ π β€ π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |