![]() |
Metamath
Proof Explorer Theorem List (p. 265 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pilem1 26401 | Lemma for pire 26406, pigt2lt4 26404 and sinpi 26405. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (π΄ β (β+ β© (β‘sin β {0})) β (π΄ β β+ β§ (sinβπ΄) = 0)) | ||
Theorem | pilem2 26402 | Lemma for pire 26406, pigt2lt4 26404 and sinpi 26405. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
β’ (π β π΄ β (2(,)4)) & β’ (π β π΅ β β+) & β’ (π β (sinβπ΄) = 0) & β’ (π β (sinβπ΅) = 0) β β’ (π β ((Ο + π΄) / 2) β€ π΅) | ||
Theorem | pilem3 26403 | Lemma for pire 26406, pigt2lt4 26404 and sinpi 26405. Existence part. (Contributed by Paul Chapman, 23-Jan-2008.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) (Revised by AV, 14-Sep-2020.) (Proof shortened by BJ, 30-Jun-2022.) |
β’ (Ο β (2(,)4) β§ (sinβΟ) = 0) | ||
Theorem | pigt2lt4 26404 | Ο is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ (2 < Ο β§ Ο < 4) | ||
Theorem | sinpi 26405 | The sine of Ο is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (sinβΟ) = 0 | ||
Theorem | pire 26406 | Ο is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ Ο β β | ||
Theorem | picn 26407 | Ο is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
β’ Ο β β | ||
Theorem | pipos 26408 | Ο is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ 0 < Ο | ||
Theorem | pirp 26409 | Ο is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ Ο β β+ | ||
Theorem | negpicn 26410 | -Ο is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -Ο β β | ||
Theorem | sinhalfpilem 26411 | Lemma for sinhalfpi 26416 and coshalfpi 26417. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ ((sinβ(Ο / 2)) = 1 β§ (cosβ(Ο / 2)) = 0) | ||
Theorem | halfpire 26412 | Ο / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
β’ (Ο / 2) β β | ||
Theorem | neghalfpire 26413 | -Ο / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -(Ο / 2) β β | ||
Theorem | neghalfpirx 26414 | -Ο / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ -(Ο / 2) β β* | ||
Theorem | pidiv2halves 26415 | Adding Ο / 2 to itself gives Ο. See 2halves 12465. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ ((Ο / 2) + (Ο / 2)) = Ο | ||
Theorem | sinhalfpi 26416 | The sine of Ο / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (sinβ(Ο / 2)) = 1 | ||
Theorem | coshalfpi 26417 | The cosine of Ο / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (cosβ(Ο / 2)) = 0 | ||
Theorem | cosneghalfpi 26418 | The cosine of -Ο / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
β’ (cosβ-(Ο / 2)) = 0 | ||
Theorem | efhalfpi 26419 | The exponential of iΟ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (expβ(i Β· (Ο / 2))) = i | ||
Theorem | cospi 26420 | The cosine of Ο is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (cosβΟ) = -1 | ||
Theorem | efipi 26421 | The exponential of i Β· Ο is -1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (expβ(i Β· Ο)) = -1 | ||
Theorem | eulerid 26422 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ ((expβ(i Β· Ο)) + 1) = 0 | ||
Theorem | sin2pi 26423 | The sine of 2Ο is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (sinβ(2 Β· Ο)) = 0 | ||
Theorem | cos2pi 26424 | The cosine of 2Ο is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
β’ (cosβ(2 Β· Ο)) = 1 | ||
Theorem | ef2pi 26425 | The exponential of 2Οi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (expβ(i Β· (2 Β· Ο))) = 1 | ||
Theorem | ef2kpi 26426 | If πΎ is an integer, then the exponential of 2πΎΟi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
β’ (πΎ β β€ β (expβ((i Β· (2 Β· Ο)) Β· πΎ)) = 1) | ||
Theorem | efper 26427 | The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.) |
β’ ((π΄ β β β§ πΎ β β€) β (expβ(π΄ + ((i Β· (2 Β· Ο)) Β· πΎ))) = (expβπ΄)) | ||
Theorem | sinperlem 26428 | Lemma for sinper 26429 and cosper 26430. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (π΄ β β β (πΉβπ΄) = (((expβ(i Β· π΄))π(expβ(-i Β· π΄))) / π·)) & β’ ((π΄ + (πΎ Β· (2 Β· Ο))) β β β (πΉβ(π΄ + (πΎ Β· (2 Β· Ο)))) = (((expβ(i Β· (π΄ + (πΎ Β· (2 Β· Ο)))))π(expβ(-i Β· (π΄ + (πΎ Β· (2 Β· Ο)))))) / π·)) β β’ ((π΄ β β β§ πΎ β β€) β (πΉβ(π΄ + (πΎ Β· (2 Β· Ο)))) = (πΉβπ΄)) | ||
Theorem | sinper 26429 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ ((π΄ β β β§ πΎ β β€) β (sinβ(π΄ + (πΎ Β· (2 Β· Ο)))) = (sinβπ΄)) | ||
Theorem | cosper 26430 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ ((π΄ β β β§ πΎ β β€) β (cosβ(π΄ + (πΎ Β· (2 Β· Ο)))) = (cosβπ΄)) | ||
Theorem | sin2kpi 26431 | If πΎ is an integer, then the sine of 2πΎΟ is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (πΎ β β€ β (sinβ(πΎ Β· (2 Β· Ο))) = 0) | ||
Theorem | cos2kpi 26432 | If πΎ is an integer, then the cosine of 2πΎΟ is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (πΎ β β€ β (cosβ(πΎ Β· (2 Β· Ο))) = 1) | ||
Theorem | sin2pim 26433 | Sine of a number subtracted from 2 Β· Ο. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β β β (sinβ((2 Β· Ο) β π΄)) = -(sinβπ΄)) | ||
Theorem | cos2pim 26434 | Cosine of a number subtracted from 2 Β· Ο. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β β β (cosβ((2 Β· Ο) β π΄)) = (cosβπ΄)) | ||
Theorem | sinmpi 26435 | Sine of a number less Ο. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β β β (sinβ(π΄ β Ο)) = -(sinβπ΄)) | ||
Theorem | cosmpi 26436 | Cosine of a number less Ο. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β β β (cosβ(π΄ β Ο)) = -(cosβπ΄)) | ||
Theorem | sinppi 26437 | Sine of a number plus Ο. (Contributed by NM, 10-Aug-2008.) |
β’ (π΄ β β β (sinβ(π΄ + Ο)) = -(sinβπ΄)) | ||
Theorem | cosppi 26438 | Cosine of a number plus Ο. (Contributed by NM, 18-Aug-2008.) |
β’ (π΄ β β β (cosβ(π΄ + Ο)) = -(cosβπ΄)) | ||
Theorem | efimpi 26439 | The exponential function at i times a real number less Ο. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β β β (expβ(i Β· (π΄ β Ο))) = -(expβ(i Β· π΄))) | ||
Theorem | sinhalfpip 26440 | The sine of Ο / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (sinβ((Ο / 2) + π΄)) = (cosβπ΄)) | ||
Theorem | sinhalfpim 26441 | The sine of Ο / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (sinβ((Ο / 2) β π΄)) = (cosβπ΄)) | ||
Theorem | coshalfpip 26442 | The cosine of Ο / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ((Ο / 2) + π΄)) = -(sinβπ΄)) | ||
Theorem | coshalfpim 26443 | The cosine of Ο / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ((Ο / 2) β π΄)) = (sinβπ΄)) | ||
Theorem | ptolemy 26444 | Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 16143, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β) β§ ((π΄ + π΅) + (πΆ + π·)) = Ο) β (((sinβπ΄) Β· (sinβπ΅)) + ((sinβπΆ) Β· (sinβπ·))) = ((sinβ(π΅ + πΆ)) Β· (sinβ(π΄ + πΆ)))) | ||
Theorem | sincosq1lem 26445 | Lemma for sincosq1sgn 26446. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ ((π΄ β β β§ 0 < π΄ β§ π΄ < (Ο / 2)) β 0 < (sinβπ΄)) | ||
Theorem | sincosq1sgn 26446 | The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β (0(,)(Ο / 2)) β (0 < (sinβπ΄) β§ 0 < (cosβπ΄))) | ||
Theorem | sincosq2sgn 26447 | The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β ((Ο / 2)(,)Ο) β (0 < (sinβπ΄) β§ (cosβπ΄) < 0)) | ||
Theorem | sincosq3sgn 26448 | The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β (Ο(,)(3 Β· (Ο / 2))) β ((sinβπ΄) < 0 β§ (cosβπ΄) < 0)) | ||
Theorem | sincosq4sgn 26449 | The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β ((3 Β· (Ο / 2))(,)(2 Β· Ο)) β ((sinβπ΄) < 0 β§ 0 < (cosβπ΄))) | ||
Theorem | coseq00topi 26450 | Location of the zeroes of cosine in (0[,]Ο). (Contributed by David Moews, 28-Feb-2017.) |
β’ (π΄ β (0[,]Ο) β ((cosβπ΄) = 0 β π΄ = (Ο / 2))) | ||
Theorem | coseq0negpitopi 26451 | Location of the zeroes of cosine in (-Ο(,]Ο). (Contributed by David Moews, 28-Feb-2017.) |
β’ (π΄ β (-Ο(,]Ο) β ((cosβπ΄) = 0 β π΄ β {(Ο / 2), -(Ο / 2)})) | ||
Theorem | tanrpcl 26452 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) |
β’ (π΄ β (0(,)(Ο / 2)) β (tanβπ΄) β β+) | ||
Theorem | tangtx 26453 | The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.) |
β’ (π΄ β (0(,)(Ο / 2)) β π΄ < (tanβπ΄)) | ||
Theorem | tanabsge 26454 | The tangent function is greater than or equal to its argument in absolute value. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ (π΄ β (-(Ο / 2)(,)(Ο / 2)) β (absβπ΄) β€ (absβ(tanβπ΄))) | ||
Theorem | sinq12gt0 26455 | The sine of a number strictly between 0 and Ο is positive. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β (0(,)Ο) β 0 < (sinβπ΄)) | ||
Theorem | sinq12ge0 26456 | The sine of a number between 0 and Ο is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ (π΄ β (0[,]Ο) β 0 β€ (sinβπ΄)) | ||
Theorem | sinq34lt0t 26457 | The sine of a number strictly between Ο and 2 Β· Ο is negative. (Contributed by NM, 17-Aug-2008.) |
β’ (π΄ β (Ο(,)(2 Β· Ο)) β (sinβπ΄) < 0) | ||
Theorem | cosq14gt0 26458 | The cosine of a number strictly between -Ο / 2 and Ο / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ (π΄ β (-(Ο / 2)(,)(Ο / 2)) β 0 < (cosβπ΄)) | ||
Theorem | cosq14ge0 26459 | The cosine of a number between -Ο / 2 and Ο / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ (π΄ β (-(Ο / 2)[,](Ο / 2)) β 0 β€ (cosβπ΄)) | ||
Theorem | sincosq1eq 26460 | Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ (π΄ + π΅) = 1) β (sinβ(π΄ Β· (Ο / 2))) = (cosβ(π΅ Β· (Ο / 2)))) | ||
Theorem | sincos4thpi 26461 | The sine and cosine of Ο / 4. (Contributed by Paul Chapman, 25-Jan-2008.) |
β’ ((sinβ(Ο / 4)) = (1 / (ββ2)) β§ (cosβ(Ο / 4)) = (1 / (ββ2))) | ||
Theorem | tan4thpi 26462 | The tangent of Ο / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) |
β’ (tanβ(Ο / 4)) = 1 | ||
Theorem | sincos6thpi 26463 | The sine and cosine of Ο / 6. (Contributed by Paul Chapman, 25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.) |
β’ ((sinβ(Ο / 6)) = (1 / 2) β§ (cosβ(Ο / 6)) = ((ββ3) / 2)) | ||
Theorem | sincos3rdpi 26464 | The sine and cosine of Ο / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ ((sinβ(Ο / 3)) = ((ββ3) / 2) β§ (cosβ(Ο / 3)) = (1 / 2)) | ||
Theorem | pigt3 26465 | Ο is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ 3 < Ο | ||
Theorem | pige3 26466 | Ο is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ 3 β€ Ο | ||
Theorem | pige3ALT 26467 | Alternate proof of pige3 26466. This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2Ο. We translate this to algebra by looking at the function eβ(iπ₯) as π₯ goes from 0 to Ο / 3; it moves at unit speed and travels distance 1, hence 1 β€ Ο / 3. (Contributed by Mario Carneiro, 21-May-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ 3 β€ Ο | ||
Theorem | abssinper 26468 | The absolute value of sine has period Ο. (Contributed by NM, 17-Aug-2008.) |
β’ ((π΄ β β β§ πΎ β β€) β (absβ(sinβ(π΄ + (πΎ Β· Ο)))) = (absβ(sinβπ΄))) | ||
Theorem | sinkpi 26469 | The sine of an integer multiple of Ο is 0. (Contributed by NM, 11-Aug-2008.) |
β’ (πΎ β β€ β (sinβ(πΎ Β· Ο)) = 0) | ||
Theorem | coskpi 26470 | The absolute value of the cosine of an integer multiple of Ο is 1. (Contributed by NM, 19-Aug-2008.) |
β’ (πΎ β β€ β (absβ(cosβ(πΎ Β· Ο))) = 1) | ||
Theorem | sineq0 26471 | A complex number whose sine is zero is an integer multiple of Ο. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (π΄ β β β ((sinβπ΄) = 0 β (π΄ / Ο) β β€)) | ||
Theorem | coseq1 26472 | A complex number whose cosine is one is an integer multiple of 2Ο. (Contributed by Mario Carneiro, 12-May-2014.) |
β’ (π΄ β β β ((cosβπ΄) = 1 β (π΄ / (2 Β· Ο)) β β€)) | ||
Theorem | cos02pilt1 26473 | Cosine is less than one between zero and 2 Β· Ο. (Contributed by Jim Kingdon, 23-Mar-2024.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (cosβπ΄) < 1) | ||
Theorem | cosq34lt1 26474 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
β’ (π΄ β (Ο[,)(2 Β· Ο)) β (cosβπ΄) < 1) | ||
Theorem | efeq1 26475 | A complex number whose exponential is one is an integer multiple of 2Οi. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
β’ (π΄ β β β ((expβπ΄) = 1 β (π΄ / (i Β· (2 Β· Ο))) β β€)) | ||
Theorem | cosne0 26476 | The cosine function has no zeroes within the vertical strip of the complex plane between real part -Ο / 2 and Ο / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
β’ ((π΄ β β β§ (ββπ΄) β (-(Ο / 2)(,)(Ο / 2))) β (cosβπ΄) β 0) | ||
Theorem | cosordlem 26477 | Lemma for cosord 26478. (Contributed by Mario Carneiro, 10-May-2014.) |
β’ (π β π΄ β (0[,]Ο)) & β’ (π β π΅ β (0[,]Ο)) & β’ (π β π΄ < π΅) β β’ (π β (cosβπ΅) < (cosβπ΄)) | ||
Theorem | cosord 26478 | Cosine is decreasing over the closed interval from 0 to Ο. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.) |
β’ ((π΄ β (0[,]Ο) β§ π΅ β (0[,]Ο)) β (π΄ < π΅ β (cosβπ΅) < (cosβπ΄))) | ||
Theorem | cos0pilt1 26479 | Cosine is between minus one and one on the open interval between zero and Ο. (Contributed by Jim Kingdon, 7-May-2024.) |
β’ (π΄ β (0(,)Ο) β (cosβπ΄) β (-1(,)1)) | ||
Theorem | cos11 26480 | Cosine is one-to-one over the closed interval from 0 to Ο. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.) |
β’ ((π΄ β (0[,]Ο) β§ π΅ β (0[,]Ο)) β (π΄ = π΅ β (cosβπ΄) = (cosβπ΅))) | ||
Theorem | sinord 26481 | Sine is increasing over the closed interval from -(Ο / 2) to (Ο / 2). (Contributed by Mario Carneiro, 29-Jul-2014.) |
β’ ((π΄ β (-(Ο / 2)[,](Ο / 2)) β§ π΅ β (-(Ο / 2)[,](Ο / 2))) β (π΄ < π΅ β (sinβπ΄) < (sinβπ΅))) | ||
Theorem | recosf1o 26482 | The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) |
β’ (cos βΎ (0[,]Ο)):(0[,]Ο)β1-1-ontoβ(-1[,]1) | ||
Theorem | resinf1o 26483 | The sine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) |
β’ (sin βΎ (-(Ο / 2)[,](Ο / 2))):(-(Ο / 2)[,](Ο / 2))β1-1-ontoβ(-1[,]1) | ||
Theorem | tanord1 26484 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 26485.) (Contributed by Mario Carneiro, 29-Jul-2014.) Revised to replace an OLD theorem. (Revised by Wolf Lammen, 20-Sep-2020.) |
β’ ((π΄ β (0[,)(Ο / 2)) β§ π΅ β (0[,)(Ο / 2))) β (π΄ < π΅ β (tanβπ΄) < (tanβπ΅))) | ||
Theorem | tanord 26485 | The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ ((π΄ β (-(Ο / 2)(,)(Ο / 2)) β§ π΅ β (-(Ο / 2)(,)(Ο / 2))) β (π΄ < π΅ β (tanβπ΄) < (tanβπ΅))) | ||
Theorem | tanregt0 26486 | The real part of the tangent of a complex number with real part in the open interval (0(,)(Ο / 2)) is positive. (Contributed by Mario Carneiro, 5-Apr-2015.) |
β’ ((π΄ β β β§ (ββπ΄) β (0(,)(Ο / 2))) β 0 < (ββ(tanβπ΄))) | ||
Theorem | negpitopissre 26487 | The interval (-Ο(,]Ο) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
β’ (-Ο(,]Ο) β β | ||
Theorem | efgh 26488* | The exponential function of a scaled complex number is a group homomorphism from the group of complex numbers under addition to the set of complex numbers under multiplication. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 11-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
β’ πΉ = (π₯ β π β¦ (expβ(π΄ Β· π₯))) β β’ (((π΄ β β β§ π β (SubGrpββfld)) β§ π΅ β π β§ πΆ β π) β (πΉβ(π΅ + πΆ)) = ((πΉβπ΅) Β· (πΉβπΆ))) | ||
Theorem | efif1olem1 26489* | Lemma for efif1o 26493. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ ((π΄ β β β§ (π₯ β π· β§ π¦ β π·)) β (absβ(π₯ β π¦)) < (2 Β· Ο)) | ||
Theorem | efif1olem2 26490* | Lemma for efif1o 26493. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ ((π΄ β β β§ π§ β β) β βπ¦ β π· ((π§ β π¦) / (2 Β· Ο)) β β€) | ||
Theorem | efif1olem3 26491* | Lemma for efif1o 26493. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) & β’ πΆ = (β‘abs β {1}) β β’ ((π β§ π₯ β πΆ) β (ββ(ββπ₯)) β (-1[,]1)) | ||
Theorem | efif1olem4 26492* | The exponential function of an imaginary number maps any interval of length 2Ο one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.) |
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) & β’ πΆ = (β‘abs β {1}) & β’ (π β π· β β) & β’ ((π β§ (π₯ β π· β§ π¦ β π·)) β (absβ(π₯ β π¦)) < (2 Β· Ο)) & β’ ((π β§ π§ β β) β βπ¦ β π· ((π§ β π¦) / (2 Β· Ο)) β β€) & β’ π = (sin βΎ (-(Ο / 2)[,](Ο / 2))) β β’ (π β πΉ:π·β1-1-ontoβπΆ) | ||
Theorem | efif1o 26493* | The exponential function of an imaginary number maps any open-below, closed-above interval of length 2Ο one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) & β’ πΆ = (β‘abs β {1}) & β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ (π΄ β β β πΉ:π·β1-1-ontoβπΆ) | ||
Theorem | efifo 26494* | The exponential function of an imaginary number maps the reals onto the unit circle. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ πΉ = (π§ β β β¦ (expβ(i Β· π§))) & β’ πΆ = (β‘abs β {1}) β β’ πΉ:ββontoβπΆ | ||
Theorem | eff1olem 26495* | The exponential function maps the set π, of complex numbers with imaginary part in a real interval of length 2 Β· Ο, one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.) |
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) & β’ π = (β‘β β π·) & β’ (π β π· β β) & β’ ((π β§ (π₯ β π· β§ π¦ β π·)) β (absβ(π₯ β π¦)) < (2 Β· Ο)) & β’ ((π β§ π§ β β) β βπ¦ β π· ((π§ β π¦) / (2 Β· Ο)) β β€) β β’ (π β (exp βΎ π):πβ1-1-ontoβ(β β {0})) | ||
Theorem | eff1o 26496 | The exponential function maps the set π, of complex numbers with imaginary part in the closed-above, open-below interval from -Ο to Ο one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
β’ π = (β‘β β (-Ο(,]Ο)) β β’ (exp βΎ π):πβ1-1-ontoβ(β β {0}) | ||
Theorem | efabl 26497* | The image of a subgroup of the group +, under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
β’ πΉ = (π₯ β π β¦ (expβ(π΄ Β· π₯))) & β’ πΊ = ((mulGrpββfld) βΎs ran πΉ) & β’ (π β π΄ β β) & β’ (π β π β (SubGrpββfld)) β β’ (π β πΊ β Abel) | ||
Theorem | efsubm 26498* | The image of a subgroup of the group +, under the exponential function of a scaled complex number is a submonoid of the multiplicative group of βfld. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
β’ πΉ = (π₯ β π β¦ (expβ(π΄ Β· π₯))) & β’ πΊ = ((mulGrpββfld) βΎs ran πΉ) & β’ (π β π΄ β β) & β’ (π β π β (SubGrpββfld)) β β’ (π β ran πΉ β (SubMndβ(mulGrpββfld))) | ||
Theorem | circgrp 26499 | The circle group π is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by Mario Carneiro, 13-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
β’ πΆ = (β‘abs β {1}) & β’ π = ((mulGrpββfld) βΎs πΆ) β β’ π β Abel | ||
Theorem | circsubm 26500 | The circle group π is a submonoid of the multiplicative group of βfld. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
β’ πΆ = (β‘abs β {1}) & β’ π = ((mulGrpββfld) βΎs πΆ) β β’ πΆ β (SubMndβ(mulGrpββfld)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |