![]() |
Intuitionistic Logic Explorer Theorem List (p. 118 of 149) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eft0val 11701 | The value of the first term of the series expansion of the exponential function is 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 29-Apr-2014.) |
β’ (π΄ β β β ((π΄β0) / (!β0)) = 1) | ||
Theorem | ef4p 11702* | 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, 29-Apr-2014.) |
β’ πΉ = (π β β0 β¦ ((π΄βπ) / (!βπ))) β β’ (π΄ β β β (expβπ΄) = ((((1 + π΄) + ((π΄β2) / 2)) + ((π΄β3) / 6)) + Ξ£π β (β€β₯β4)(πΉβπ))) | ||
Theorem | efgt1p2 11703 | The exponential of a positive real number is greater than the sum of the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (π΄ β β+ β ((1 + π΄) + ((π΄β2) / 2)) < (expβπ΄)) | ||
Theorem | efgt1p 11704 | The exponential of a positive real number is greater than 1 plus that number. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β+ β (1 + π΄) < (expβπ΄)) | ||
Theorem | efgt1 11705 | The exponential of a positive real number is greater than 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β+ β 1 < (expβπ΄)) | ||
Theorem | efltim 11706 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 20-Dec-2022.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β (expβπ΄) < (expβπ΅))) | ||
Theorem | reef11 11707 | The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.) |
β’ ((π΄ β β β§ π΅ β β) β ((expβπ΄) = (expβπ΅) β π΄ = π΅)) | ||
Theorem | reeff1 11708 | The exponential function maps real arguments one-to-one to positive reals. (Contributed by Steve Rodriguez, 25-Aug-2007.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (exp βΎ β):ββ1-1ββ+ | ||
Theorem | eflegeo 11709 | The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΄ < 1) β β’ (π β (expβπ΄) β€ (1 / (1 β π΄))) | ||
Theorem | sinval 11710 | Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (sinβπ΄) = (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i))) | ||
Theorem | cosval 11711 | Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
β’ (π΄ β β β (cosβπ΄) = (((expβ(i Β· π΄)) + (expβ(-i Β· π΄))) / 2)) | ||
Theorem | sinf 11712 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ sin:ββΆβ | ||
Theorem | cosf 11713 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ cos:ββΆβ | ||
Theorem | sincl 11714 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | coscl 11715 | Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | tanvalap 11716 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
β’ ((π΄ β β β§ (cosβπ΄) # 0) β (tanβπ΄) = ((sinβπ΄) / (cosβπ΄))) | ||
Theorem | tanclap 11717 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
β’ ((π΄ β β β§ (cosβπ΄) # 0) β (tanβπ΄) β β) | ||
Theorem | sincld 11718 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | coscld 11719 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | tanclapd 11720 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) # 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | tanval2ap 11721 | Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
β’ ((π΄ β β β§ (cosβπ΄) # 0) β (tanβπ΄) = (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (i Β· ((expβ(i Β· π΄)) + (expβ(-i Β· π΄)))))) | ||
Theorem | tanval3ap 11722 | Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
β’ ((π΄ β β β§ ((expβ(2 Β· (i Β· π΄))) + 1) # 0) β (tanβπ΄) = (((expβ(2 Β· (i Β· π΄))) β 1) / (i Β· ((expβ(2 Β· (i Β· π΄))) + 1)))) | ||
Theorem | resinval 11723 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | recosval 11724 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) = (ββ(expβ(i Β· π΄)))) | ||
Theorem | efi4p 11725* | 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 11726* | 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 11727* | 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 11728 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβπ΄) β β) | ||
Theorem | recoscl 11729 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβπ΄) β β) | ||
Theorem | retanclap 11730 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
β’ ((π΄ β β β§ (cosβπ΄) # 0) β (tanβπ΄) β β) | ||
Theorem | resincld 11731 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (sinβπ΄) β β) | ||
Theorem | recoscld 11732 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (cosβπ΄) β β) | ||
Theorem | retanclapd 11733 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (cosβπ΄) # 0) β β’ (π β (tanβπ΄) β β) | ||
Theorem | sinneg 11734 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (sinβ-π΄) = -(sinβπ΄)) | ||
Theorem | cosneg 11735 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (cosβ-π΄) = (cosβπ΄)) | ||
Theorem | tannegap 11736 | 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 11737 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
β’ (sinβ0) = 0 | ||
Theorem | cos0 11738 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
β’ (cosβ0) = 1 | ||
Theorem | tan0 11739 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
β’ (tanβ0) = 0 | ||
Theorem | efival 11740 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (expβ(i Β· π΄)) = ((cosβπ΄) + (i Β· (sinβπ΄)))) | ||
Theorem | efmival 11741 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
β’ (π΄ β β β (expβ(-i Β· π΄)) = ((cosβπ΄) β (i Β· (sinβπ΄)))) | ||
Theorem | efeul 11742 | 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 11743 | 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 11744 | 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 11745 | 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 | tanaddaplem 11746 | A useful intermediate step in tanaddap 11747 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) (Revised by Jim Kingdon, 25-Dec-2022.) |
β’ (((π΄ β β β§ π΅ β β) β§ ((cosβπ΄) # 0 β§ (cosβπ΅) # 0)) β ((cosβ(π΄ + π΅)) # 0 β ((tanβπ΄) Β· (tanβπ΅)) # 1)) | ||
Theorem | tanaddap 11747 | 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 11748 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (sinβ(π΄ β π΅)) = (((sinβπ΄) Β· (cosβπ΅)) β ((cosβπ΄) Β· (sinβπ΅)))) | ||
Theorem | cossub 11749 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (cosβ(π΄ β π΅)) = (((cosβπ΄) Β· (cosβπ΅)) + ((sinβπ΄) Β· (sinβπ΅)))) | ||
Theorem | addsin 11750 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) + (sinβπ΅)) = (2 Β· ((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) | ||
Theorem | subsin 11751 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) β (sinβπ΅)) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) | ||
Theorem | sinmul 11752 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 11745 and cossub 11749. (Contributed by David A. Wheeler, 26-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((sinβπ΄) Β· (sinβπ΅)) = (((cosβ(π΄ β π΅)) β (cosβ(π΄ + π΅))) / 2)) | ||
Theorem | cosmul 11753 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 11745 and cossub 11749. (Contributed by David A. Wheeler, 26-May-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΄) Β· (cosβπ΅)) = (((cosβ(π΄ β π΅)) + (cosβ(π΄ + π΅))) / 2)) | ||
Theorem | addcos 11754 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((cosβπ΄) + (cosβπ΅)) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) | ||
Theorem | subcos 11755 | 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 11756 | 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 11757 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
β’ (π΄ β β β (sinβ(2 Β· π΄)) = (2 Β· ((sinβπ΄) Β· (cosβπ΄)))) | ||
Theorem | cos2t 11758 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ(2 Β· π΄)) = ((2 Β· ((cosβπ΄)β2)) β 1)) | ||
Theorem | cos2tsin 11759 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
β’ (π΄ β β β (cosβ(2 Β· π΄)) = (1 β (2 Β· ((sinβπ΄)β2)))) | ||
Theorem | sinbnd 11760 | 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 11761 | 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 11762 | 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 11763 | 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 11764* | Lemma for sin01bnd 11765 and cos01bnd 11766. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ πΉ = (π β β0 β¦ (((i Β· π΄)βπ) / (!βπ))) β β’ (π΄ β (0(,]1) β (absβΞ£π β (β€β₯β4)(πΉβπ)) < ((π΄β4) / 6)) | ||
Theorem | sin01bnd 11765 | 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 11766 | 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 11767 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ ((1 / 3) < (cosβ1) β§ (cosβ1) < (2 / 3)) | ||
Theorem | cos2bnd 11768 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (-(7 / 9) < (cosβ2) β§ (cosβ2) < -(1 / 9)) | ||
Theorem | sin01gt0 11769 | 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 11770 | 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 11771 | 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 11772 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (0 < (sinβ1) β§ 0 < (cosβ1)) | ||
Theorem | sincos2sgn 11773 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (0 < (sinβ2) β§ (cosβ2) < 0) | ||
Theorem | sin4lt0 11774 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
β’ (sinβ4) < 0 | ||
Theorem | cos12dec 11775 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
β’ ((π΄ β (1[,]2) β§ π΅ β (1[,]2) β§ π΄ < π΅) β (cosβπ΅) < (cosβπ΄)) | ||
Theorem | absefi 11776 | 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 11777 | 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 11778 | 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 11779 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
β’ ((π΄ β β β§ (expβ(i Β· π΄)) = 1) β π΄ β β) | ||
Theorem | demoivre 11780 | 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 11781 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
β’ ((π΄ β β β§ π β β€) β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) | ||
Theorem | demoivreALT 11781 | Alternate proof of demoivre 11780. 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 11782 | Extend class notation to include the constant tau, Ο = 6.28318.... |
class Ο | ||
Definition | df-tau 11783 | 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 | eirraplem 11784* | Lemma for eirrap 11785. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.) |
β’ πΉ = (π β β0 β¦ (1 / (!βπ))) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β e # (π / π)) | ||
Theorem | eirrap 11785 | e is irrational. That is, for any rational number, e is apart from it. In the absence of excluded middle, we can distinguish between this and saying that e is not rational, which is eirr 11786. (Contributed by Jim Kingdon, 6-Jan-2023.) |
β’ (π β β β e # π) | ||
Theorem | eirr 11786 | e is not rational. In the absence of excluded middle, we can distinguish between this and saying that e is irrational in the sense of being apart from any rational number, which is eirrap 11785. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.) |
β’ e β β | ||
Theorem | egt2lt3 11787 | Euler's constant e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.) |
β’ (2 < e β§ e < 3) | ||
Theorem | epos 11788 | Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
β’ 0 < e | ||
Theorem | epr 11789 | Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
β’ e β β+ | ||
Theorem | ene0 11790 | e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
β’ e β 0 | ||
Theorem | eap0 11791 | e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.) |
β’ e # 0 | ||
Theorem | ene1 11792 | e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
β’ e β 1 | ||
Theorem | eap1 11793 | e is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.) |
β’ e # 1 | ||
This part introduces elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Syntax | cdvds 11794 | Extend the definition of a class to include the divides relation. See df-dvds 11795. |
class β₯ | ||
Definition | df-dvds 11795* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ β₯ = {β¨π₯, π¦β© β£ ((π₯ β β€ β§ π¦ β β€) β§ βπ β β€ (π Β· π₯) = π¦)} | ||
Theorem | divides 11796* | Define the divides relation. π β₯ π means π divides into π with no remainder. For example, 3 β₯ 6 (ex-dvds 14485). As proven in dvdsval3 11798, π β₯ π β (π mod π) = 0. See divides 11796 and dvdsval2 11797 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β βπ β β€ (π Β· π) = π)) | ||
Theorem | dvdsval2 11797 | 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 11798 | 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 11799 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ (π β₯ π β (π β β€ β§ π β β€)) | ||
Theorem | dvdsmod0 11800 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
β’ ((π β β β§ π β₯ π) β (π mod π) = 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |