Home | Intuitionistic Logic Explorer Theorem List (p. 115 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efgt1p2 11401 | 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.) |
Theorem | efgt1p 11402 | 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.) |
Theorem | efgt1 11403 | 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.) |
Theorem | efltim 11404 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 20-Dec-2022.) |
Theorem | efler 11405 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 20-Dec-2022.) |
Theorem | reef11 11406 | The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.) |
Theorem | reeff1 11407 | 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.) |
Theorem | eflegeo 11408 | The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.) |
Theorem | sinval 11409 | Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
Theorem | cosval 11410 | Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.) |
Theorem | sinf 11411 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | cosf 11412 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | sincl 11413 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | coscl 11414 | Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | tanvalap 11415 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
# | ||
Theorem | tanclap 11416 | 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.) |
# | ||
Theorem | sincld 11417 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | coscld 11418 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | tanclapd 11419 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
Theorem | tanval2ap 11420 | Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
Theorem | tanval3ap 11421 | Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
Theorem | resinval 11422 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
Theorem | recosval 11423 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
Theorem | efi4p 11424* | 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.) |
Theorem | resin4p 11425* | 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.) |
Theorem | recos4p 11426* | 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.) |
Theorem | resincl 11427 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
Theorem | recoscl 11428 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
Theorem | retanclap 11429 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
# | ||
Theorem | resincld 11430 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | recoscld 11431 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | retanclapd 11432 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
# | ||
Theorem | sinneg 11433 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
Theorem | cosneg 11434 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
Theorem | tannegap 11435 | The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.) |
# | ||
Theorem | sin0 11436 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
Theorem | cos0 11437 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
Theorem | tan0 11438 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
Theorem | efival 11439 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
Theorem | efmival 11440 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
Theorem | efeul 11441 | Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.) |
Theorem | efieq 11442 | The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.) |
Theorem | sinadd 11443 | Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | cosadd 11444 | Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Theorem | tanaddaplem 11445 | A useful intermediate step in tanaddap 11446 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) (Revised by Jim Kingdon, 25-Dec-2022.) |
# # # # | ||
Theorem | tanaddap 11446 | Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.) |
# # # | ||
Theorem | sinsub 11447 | Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | cossub 11448 | Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | addsin 11449 | Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | subsin 11450 | Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | sinmul 11451 | Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 11444 and cossub 11448. (Contributed by David A. Wheeler, 26-May-2015.) |
Theorem | cosmul 11452 | Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 11444 and cossub 11448. (Contributed by David A. Wheeler, 26-May-2015.) |
Theorem | addcos 11453 | Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) |
Theorem | subcos 11454 | Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.) |
Theorem | sincossq 11455 | 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.) |
Theorem | sin2t 11456 | Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.) |
Theorem | cos2t 11457 | Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.) |
Theorem | cos2tsin 11458 | Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.) |
Theorem | sinbnd 11459 | The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
Theorem | cosbnd 11460 | The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.) |
Theorem | sinbnd2 11461 | The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
Theorem | cosbnd2 11462 | The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.) |
Theorem | ef01bndlem 11463* | Lemma for sin01bnd 11464 and cos01bnd 11465. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | sin01bnd 11464 | 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.) |
Theorem | cos01bnd 11465 | 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.) |
Theorem | cos1bnd 11466 | Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | cos2bnd 11467 | Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | sin01gt0 11468 | 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.) |
Theorem | cos01gt0 11469 | The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | sin02gt0 11470 | The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | sincos1sgn 11471 | The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | sincos2sgn 11472 | The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | sin4lt0 11473 | The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.) |
Theorem | cos12dec 11474 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
Theorem | absefi 11475 | 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.) |
Theorem | absef 11476 | The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007.) |
Theorem | absefib 11477 | A complex number is real iff the exponential of its product with has absolute value one. (Contributed by NM, 21-Aug-2008.) |
Theorem | efieq1re 11478 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
Theorem | demoivre 11479 | 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 11480 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
Theorem | demoivreALT 11480 | Alternate proof of demoivre 11479. 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.) |
Syntax | ctau 11481 | Extend class notation to include the constant tau, = 6.28318.... |
Definition | df-tau 11482 | 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 . 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 | ||
Theorem | eirraplem 11483* | Lemma for eirrap 11484. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.) |
# | ||
Theorem | eirrap 11484 | is irrational. That is, for any rational number, is apart from it. In the absence of excluded middle, we can distinguish between this and saying that is not rational, which is eirr 11485. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# | ||
Theorem | eirr 11485 | is not rational. In the absence of excluded middle, we can distinguish between this and saying that is irrational in the sense of being apart from any rational number, which is eirrap 11484. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.) |
Theorem | egt2lt3 11486 | Euler's constant = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.) |
Theorem | epos 11487 | Euler's constant is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
Theorem | epr 11488 | Euler's constant is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
Theorem | ene0 11489 | is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
Theorem | eap0 11490 | is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
Theorem | ene1 11491 | is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
Theorem | eap1 11492 | is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Syntax | cdvds 11493 | Extend the definition of a class to include the divides relation. See df-dvds 11494. |
Definition | df-dvds 11494* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divides 11495* | Define the divides relation. means divides into with no remainder. For example, (ex-dvds 12942). As proven in dvdsval3 11497, . See divides 11495 and dvdsval2 11496 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsval2 11496 | One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.) |
Theorem | dvdsval3 11497 | 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.) |
Theorem | dvdszrcl 11498 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Theorem | nndivdvds 11499 | Strong form of dvdsval2 11496 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
Theorem | nndivides 11500* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |