Home | Metamath
Proof Explorer Theorem List (p. 161 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ef01bndlem 16001* | Lemma for sin01bnd 16002 and cos01bnd 16003. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β (0(,]1) β (absβΞ£π β (β€β₯β4)(πΉβπ)) < ((π΄β4) / 6)) | ||
Theorem | sin01bnd 16002 | 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 16003 | 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 16004 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ ((1 / 3) < (cosβ1) β§ (cosβ1) < (2 / 3)) | ||
Theorem | cos2bnd 16005 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (-(7 / 9) < (cosβ2) β§ (cosβ2) < -(1 / 9)) | ||
Theorem | sinltx 16006 | The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014.) |
β’ (π΄ β β+ β (sinβπ΄) < π΄) | ||
Theorem | sin01gt0 16007 | 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 16008 | 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 16009 | 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 16010 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (0 < (sinβ1) β§ 0 < (cosβ1)) | ||
Theorem | sincos2sgn 16011 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (0 < (sinβ2) β§ (cosβ2) < 0) | ||
Theorem | sin4lt0 16012 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (sinβ4) < 0 | ||
Theorem | absefi 16013 | 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 16014 | 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 16015 | 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 16016 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
β’ ((π΄ β β β§ (expβ(i Β· π΄)) = 1) β π΄ β β) | ||
Theorem | demoivre 16017 | 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 16018 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
β’ ((π΄ β β β§ π β β€) β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) | ||
Theorem | demoivreALT 16018 | Alternate proof of demoivre 16017. 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 16019 | Extend class notation to include the constant tau, Ο = 6.28318.... |
class Ο | ||
Definition | df-tau 16020 | 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 16021* | Lemma for eirr 16022. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ (1 / (!βπ))) & β’ (π β π β β€) & β’ (π β π β β) & β’ (π β e = (π / π)) β β’ Β¬ π | ||
Theorem | eirr 16022 | e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.) |
β’ e β β | ||
Theorem | egt2lt3 16023 | 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 16024 | Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
β’ 0 < e | ||
Theorem | epr 16025 | Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
β’ e β β+ | ||
Theorem | ene0 16026 | e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
β’ e β 0 | ||
Theorem | ene1 16027 | e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
β’ e β 1 | ||
Theorem | xpnnen 16028 | 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 16029 | 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 16030 | 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 16031* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β ((πΉβπ΄)βπ) = if(π β π΄, ((1 / 3)βπ), 0)) | ||
Theorem | rpnnen2lem2 16032* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ (π΄ β β β (πΉβπ΄):ββΆβ) | ||
Theorem | rpnnen2lem3 16033* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ seq1( + , (πΉββ)) β (1 / 2) | ||
Theorem | rpnnen2lem4 16034* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β π΅ β§ π΅ β β β§ π β β) β (0 β€ ((πΉβπ΄)βπ) β§ ((πΉβπ΄)βπ) β€ ((πΉβπ΅)βπ))) | ||
Theorem | rpnnen2lem5 16035* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β seqπ( + , (πΉβπ΄)) β dom β ) | ||
Theorem | rpnnen2lem6 16036* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) β β) | ||
Theorem | rpnnen2lem7 16037* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β π΅ β§ π΅ β β β§ π β β) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) β€ Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) | ||
Theorem | rpnnen2lem8 16038* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ ((π΄ β β β§ π β β) β Ξ£π β β ((πΉβπ΄)βπ) = (Ξ£π β (1...(π β 1))((πΉβπ΄)βπ) + Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ))) | ||
Theorem | rpnnen2lem9 16039* | Lemma for rpnnen2 16043. (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 16040* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β (π΄ β π΅)) & β’ (π β βπ β β (π < π β (π β π΄ β π β π΅))) & β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = Ξ£π β β ((πΉβπ΅)βπ)) β β’ ((π β§ π) β Ξ£π β (β€β₯βπ)((πΉβπ΄)βπ) = Ξ£π β (β€β₯βπ)((πΉβπ΅)βπ)) | ||
Theorem | rpnnen2lem11 16041* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β (π΄ β π΅)) & β’ (π β βπ β β (π < π β (π β π΄ β π β π΅))) & β’ (π β Ξ£π β β ((πΉβπ΄)βπ) = Ξ£π β β ((πΉβπ΅)βπ)) β β’ (π β Β¬ π) | ||
Theorem | rpnnen2lem12 16042* | Lemma for rpnnen2 16043. (Contributed by Mario Carneiro, 13-May-2013.) |
β’ πΉ = (π₯ β π« β β¦ (π β β β¦ if(π β π₯, ((1 / 3)βπ), 0))) β β’ π« β βΌ (0[,]1) | ||
Theorem | rpnnen2 16043 |
The other half of rpnnen 16044, 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... 15701). 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 16031). This is an infinite sum of real numbers (rpnnen2lem2 16032), and since π΄ β π΅ implies (πΉβπ΄) β€ (πΉβπ΅) (rpnnen2lem4 16034) and (πΉββ) converges to 1 / 2 (rpnnen2lem3 16033) by geoisum1 15699, the sum is convergent to some real (rpnnen2lem5 16035 and rpnnen2lem6 16036) by the comparison test for convergence cvgcmp 15636. The comparison test also tells us that π΄ β π΅ implies Ξ£(πΉβπ΄) β€ Ξ£(πΉβπ΅) (rpnnen2lem7 16037). 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 16038) and cancel them (rpnnen2lem10 16040), 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 16039) and Ξ£(πΉβ{π}) = (3β-π), we establish that Ξ£(πΉβπ¦) < Ξ£(πΉβπ₯) (rpnnen2lem11 16041) so that they must be different. By contraposition (rpnnen2lem12 16042), 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 16044 | The cardinality of the continuum is the same as the powerset of Ο. This is a stronger statement than ruc 16060, which only asserts that β is uncountable, i.e. has a cardinality larger than Ο. The main proof is in two parts, rpnnen1 12837 and rpnnen2 16043, each showing an injection in one direction, and this last part uses sbth 8971 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 16045 | 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 9887 directly). (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) |
β’ (β Γ β) β β | ||
Theorem | cpnnen 16046 | The complex numbers are equinumerous to the powerset of the positive integers. (Contributed by Mario Carneiro, 16-Jun-2013.) |
β’ β β π« β | ||
Theorem | rucALT 16047 | Alternate proof of ruc 16060. This proof is a simple corollary of rpnnen 16044, which determines the exact cardinality of the reals. For an alternate proof discussed at mmcomplex.html#uncountable 16044, see ruc 16060. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 13-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β βΊ β | ||
Theorem | ruclem1 16048* | Lemma for ruc 16060 (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 16049* | Lemma for ruc 16060. 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 16050* | Lemma for ruc 16060. The constructed interval [π, π] always excludes π. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (1st β(β¨π΄, π΅β©π·π)) & β’ π = (2nd β(β¨π΄, π΅β©π·π)) & β’ (π β π΄ < π΅) β β’ (π β (π < π β¨ π < π)) | ||
Theorem | ruclem4 16051* | Lemma for ruc 16060. 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 16052* | Lemma for ruc 16060. Domain and codomain 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 16053* | Lemma for ruc 16060. 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 16054* | Lemma for ruc 16060. 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 16055* | Lemma for ruc 16060. 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 16056* | Lemma for ruc 16060. 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 16057* | Lemma for ruc 16060. 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 16058* | Lemma for ruc 16060. 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 16059 | Lemma for ruc 16060. There is no function that maps β onto β. (Use nex 1803 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 16060 | 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 16048 through ruclem13 16059 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 16059 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable 16059. For an alternate proof see rucALT 16047. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.) |
β’ β βΊ β | ||
Theorem | resdomq 16061 | The set of rationals is strictly less equinumerous than the set of reals (β strictly dominates β). (Contributed by NM, 18-Dec-2004.) |
β’ β βΊ β | ||
Theorem | aleph1re 16062 | There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.) |
β’ (β΅β1o) βΌ β | ||
Theorem | aleph1irr 16063 | There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.) |
β’ (β΅β1o) βΌ (β β β) | ||
Theorem | cnso 16064 | The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ βπ₯ π₯ Or β | ||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Theorem | sqrt2irrlem 16065 | Lemma for sqrt2irr 16066. This is the core of the proof: if π΄ / π΅ = β(2), then π΄ and π΅ are even, so π΄ / 2 and π΅ / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). This is Metamath 100 proof #1. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) (Proof shortened by JV, 4-Jan-2022.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β) & β’ (π β (ββ2) = (π΄ / π΅)) β β’ (π β ((π΄ / 2) β β€ β§ (π΅ / 2) β β)) | ||
Theorem | sqrt2irr 16066 | The square root of 2 is irrational. See zsqrtelqelz 16568 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 16065, which shows that if π΄ / π΅ = β(2), then π΄ and π΅ are even, so π΄ / 2 and π΅ / 2 are smaller representatives, which is absurd. An older version of this proof was included in The Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on his Formalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/ 16065. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ (ββ2) β β | ||
Theorem | sqrt2re 16067 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
β’ (ββ2) β β | ||
Theorem | sqrt2irr0 16068 | The square root of 2 is an irrational number. (Contributed by AV, 23-Dec-2022.) |
β’ (ββ2) β (β β β) | ||
Theorem | nthruc 16069 | The sequence β, β€, β, β, and β forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to β€ but not β, one-half belongs to β but not β€, the square root of 2 belongs to β but not β, and finally that the imaginary number i belongs to β but not β. See nthruz 16070 for a further refinement. (Contributed by NM, 12-Jan-2002.) |
β’ ((β β β€ β§ β€ β β) β§ (β β β β§ β β β)) | ||
Theorem | nthruz 16070 | The sequence β, β0, and β€ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to β0 but not β and minus one belongs to β€ but not β0. This theorem refines the chain of proper subsets nthruc 16069. (Contributed by NM, 9-May-2004.) |
β’ (β β β0 β§ β0 β β€) | ||
Syntax | cdvds 16071 | Extend the definition of a class to include the divides relation. See df-dvds 16072. |
class β₯ | ||
Definition | df-dvds 16072* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ β₯ = {β¨π₯, π¦β© β£ ((π₯ β β€ β§ π¦ β β€) β§ βπ β β€ (π Β· π₯) = π¦)} | ||
Theorem | divides 16073* | Define the divides relation. π β₯ π means π divides into π with no remainder. For example, 3 β₯ 6 (ex-dvds 29186). As proven in dvdsval3 16075, π β₯ π β (π mod π) = 0. See divides 16073 and dvdsval2 16074 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β βπ β β€ (π Β· π) = π)) | ||
Theorem | dvdsval2 16074 | One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.) |
β’ ((π β β€ β§ π β 0 β§ π β β€) β (π β₯ π β (π / π) β β€)) | ||
Theorem | dvdsval3 16075 | One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.) |
β’ ((π β β β§ π β β€) β (π β₯ π β (π mod π) = 0)) | ||
Theorem | dvdszrcl 16076 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ (π β₯ π β (π β β€ β§ π β β€)) | ||
Theorem | dvdsmod0 16077 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
β’ ((π β β β§ π β₯ π) β (π mod π) = 0) | ||
Theorem | p1modz1 16078 | If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022.) |
β’ ((π β₯ π΄ β§ 1 < π) β ((π΄ + 1) mod π) = 1) | ||
Theorem | dvdsmodexp 16079 | If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl 16591). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.) |
β’ ((π β β β§ π΅ β β β§ π β₯ π΄) β ((π΄βπ΅) mod π) = (π΄ mod π)) | ||
Theorem | nndivdvds 16080 | Strong form of dvdsval2 16074 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΅ β₯ π΄ β (π΄ / π΅) β β)) | ||
Theorem | nndivides 16081* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
β’ ((π β β β§ π β β) β (π β₯ π β βπ β β (π Β· π) = π)) | ||
Theorem | moddvds 16082 | Two ways to say π΄β‘π΅ (mod π), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ π΅ β β€) β ((π΄ mod π) = (π΅ mod π) β π β₯ (π΄ β π΅))) | ||
Theorem | modm1div 16083 | An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.) |
β’ ((π β (β€β₯β2) β§ π΄ β β€) β ((π΄ mod π) = 1 β π β₯ (π΄ β 1))) | ||
Theorem | dvds0lem 16084 | A lemma to assist theorems of β₯ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ (πΎ Β· π) = π) β π β₯ π) | ||
Theorem | dvds1lem 16085* | A lemma to assist theorems of β₯ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β (π½ β β€ β§ πΎ β β€)) & β’ (π β (π β β€ β§ π β β€)) & β’ ((π β§ π₯ β β€) β π β β€) & β’ ((π β§ π₯ β β€) β ((π₯ Β· π½) = πΎ β (π Β· π) = π)) β β’ (π β (π½ β₯ πΎ β π β₯ π)) | ||
Theorem | dvds2lem 16086* | A lemma to assist theorems of β₯ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β (πΌ β β€ β§ π½ β β€)) & β’ (π β (πΎ β β€ β§ πΏ β β€)) & β’ (π β (π β β€ β§ π β β€)) & β’ ((π β§ (π₯ β β€ β§ π¦ β β€)) β π β β€) & β’ ((π β§ (π₯ β β€ β§ π¦ β β€)) β (((π₯ Β· πΌ) = π½ β§ (π¦ Β· πΎ) = πΏ) β (π Β· π) = π)) β β’ (π β ((πΌ β₯ π½ β§ πΎ β₯ πΏ) β π β₯ π)) | ||
Theorem | iddvds 16087 | An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β π β₯ π) | ||
Theorem | 1dvds 16088 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β 1 β₯ π) | ||
Theorem | dvds0 16089 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β π β₯ 0) | ||
Theorem | negdvdsb 16090 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β -π β₯ π)) | ||
Theorem | dvdsnegb 16091 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ -π)) | ||
Theorem | absdvdsb 16092 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (absβπ) β₯ π)) | ||
Theorem | dvdsabsb 16093 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (absβπ))) | ||
Theorem | 0dvds 16094 | Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β (0 β₯ π β π = 0)) | ||
Theorem | dvdsmul1 16095 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) | ||
Theorem | dvdsmul2 16096 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) | ||
Theorem | iddvdsexp 16097 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
β’ ((π β β€ β§ π β β) β π β₯ (πβπ)) | ||
Theorem | muldvds1 16098 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ Β· π) β₯ π β πΎ β₯ π)) | ||
Theorem | muldvds2 16099 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ Β· π) β₯ π β π β₯ π)) | ||
Theorem | dvdscmul 16100 | Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in [ApostolNT] p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (π β₯ π β (πΎ Β· π) β₯ (πΎ Β· π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |