![]() |
Metamath
Proof Explorer Theorem List (p. 266 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efcn 26501 | The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.) |
⊢ exp ∈ (ℂ–cn→ℂ) | ||
Theorem | sincn 26502 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ sin ∈ (ℂ–cn→ℂ) | ||
Theorem | coscn 26503 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 3-Sep-2014.) |
⊢ cos ∈ (ℂ–cn→ℂ) | ||
Theorem | reeff1olem 26504* | Lemma for reeff1o 26505. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) | ||
Theorem | reeff1o 26505 | The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.) |
⊢ (exp ↾ ℝ):ℝ–1-1-onto→ℝ+ | ||
Theorem | reefiso 26506 | The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.) |
⊢ (exp ↾ ℝ) Isom < , < (ℝ, ℝ+) | ||
Theorem | efcvx 26507 | The exponential function on the reals is a strictly convex function. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0(,)1)) → (exp‘((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵))) < ((𝑇 · (exp‘𝐴)) + ((1 − 𝑇) · (exp‘𝐵)))) | ||
Theorem | reefgim 26508 | The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑃 = ((mulGrp‘ℂfld) ↾s ℝ+) ⇒ ⊢ (exp ↾ ℝ) ∈ (ℝfld GrpIso 𝑃) | ||
Theorem | pilem1 26509 | Lemma for pire 26514, pigt2lt4 26512 and sinpi 26513. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (𝐴 ∈ (ℝ+ ∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0)) | ||
Theorem | pilem2 26510 | Lemma for pire 26514, pigt2lt4 26512 and sinpi 26513. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ (2(,)4)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (sin‘𝐴) = 0) & ⊢ (𝜑 → (sin‘𝐵) = 0) ⇒ ⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵) | ||
Theorem | pilem3 26511 | Lemma for pire 26514, pigt2lt4 26512 and sinpi 26513. 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 26512 | π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ (2 < π ∧ π < 4) | ||
Theorem | sinpi 26513 | The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘π) = 0 | ||
Theorem | pire 26514 | π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ π ∈ ℝ | ||
Theorem | picn 26515 | π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ π ∈ ℂ | ||
Theorem | pipos 26516 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ 0 < π | ||
Theorem | pirp 26517 | π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ π ∈ ℝ+ | ||
Theorem | negpicn 26518 | -π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -π ∈ ℂ | ||
Theorem | sinhalfpilem 26519 | Lemma for sinhalfpi 26524 and coshalfpi 26525. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0) | ||
Theorem | halfpire 26520 | π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (π / 2) ∈ ℝ | ||
Theorem | neghalfpire 26521 | -π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ | ||
Theorem | neghalfpirx 26522 | -π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -(π / 2) ∈ ℝ* | ||
Theorem | pidiv2halves 26523 | Adding π / 2 to itself gives π. See 2halves 12491. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ((π / 2) + (π / 2)) = π | ||
Theorem | sinhalfpi 26524 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(π / 2)) = 1 | ||
Theorem | coshalfpi 26525 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(π / 2)) = 0 | ||
Theorem | cosneghalfpi 26526 | The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (cos‘-(π / 2)) = 0 | ||
Theorem | efhalfpi 26527 | The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (π / 2))) = i | ||
Theorem | cospi 26528 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘π) = -1 | ||
Theorem | efipi 26529 | 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 26530 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
⊢ ((exp‘(i · π)) + 1) = 0 | ||
Theorem | sin2pi 26531 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (sin‘(2 · π)) = 0 | ||
Theorem | cos2pi 26532 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
⊢ (cos‘(2 · π)) = 1 | ||
Theorem | ef2pi 26533 | The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
⊢ (exp‘(i · (2 · π))) = 1 | ||
Theorem | ef2kpi 26534 | 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 26535 | 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 26536 | Lemma for sinper 26537 and cosper 26538. (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 26537 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴)) | ||
Theorem | cosper 26538 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴)) | ||
Theorem | sin2kpi 26539 | 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 26540 | 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 26541 | Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴)) | ||
Theorem | cos2pim 26542 | Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinmpi 26543 | Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴)) | ||
Theorem | cosmpi 26544 | Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴)) | ||
Theorem | sinppi 26545 | Sine of a number plus π. (Contributed by NM, 10-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) | ||
Theorem | cosppi 26546 | Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) | ||
Theorem | efimpi 26547 | The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴))) | ||
Theorem | sinhalfpip 26548 | The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴)) | ||
Theorem | sinhalfpim 26549 | The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴)) | ||
Theorem | coshalfpip 26550 | The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴)) | ||
Theorem | coshalfpim 26551 | The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴)) | ||
Theorem | ptolemy 26552 | 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 16204, 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 26553 | Lemma for sincosq1sgn 26554. (Contributed by Paul Chapman, 24-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴)) | ||
Theorem | sincosq1sgn 26554 | 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 26555 | 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 26556 | 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 26557 | 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 26558 | Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) | ||
Theorem | coseq0negpitopi 26559 | Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)})) | ||
Theorem | tanrpcl 26560 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) |
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+) | ||
Theorem | tangtx 26561 | 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 26562 | 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 26563 | The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.) |
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴)) | ||
Theorem | sinq12ge0 26564 | The sine of a number between 0 and π is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ (𝐴 ∈ (0[,]π) → 0 ≤ (sin‘𝐴)) | ||
Theorem | sinq34lt0t 26565 | The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.) |
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0) | ||
Theorem | cosq14gt0 26566 | 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 26567 | The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴)) | ||
Theorem | sincosq1eq 26568 | 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 26569 | The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.) |
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2))) | ||
Theorem | tan4thpi 26570 | The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) (Proof shortened by SN, 2-Sep-2025.) |
⊢ (tan‘(π / 4)) = 1 | ||
Theorem | tan4thpiOLD 26571 | Obsolete version of tan4thpi 26570 as of 2-Sep-2025. (Contributed by Mario Carneiro, 5-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (tan‘(π / 4)) = 1 | ||
Theorem | sincos6thpi 26572 | 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 26573 | The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2)) | ||
Theorem | pigt3 26574 | π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ 3 < π | ||
Theorem | pige3 26575 | π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
⊢ 3 ≤ π | ||
Theorem | pige3ALT 26576 | Alternate proof of pige3 26575. 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 26577 | The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴))) | ||
Theorem | sinkpi 26578 | The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0) | ||
Theorem | coskpi 26579 | The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.) |
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1) | ||
Theorem | sineq0 26580 | 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 26581 | 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 26582 | Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | cosq34lt1 26583 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1) | ||
Theorem | efeq1 26584 | 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 26585 | 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 26586 | Lemma for cosord 26587. (Contributed by Mario Carneiro, 10-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) | ||
Theorem | cosord 26587 | 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 26588 | 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 26589 | 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 26590 | 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 26591 | 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 26592 | 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 26593 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 26594.) (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 26594 | 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 26595 | 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 26596 | The interval (-π(,]π) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (-π(,]π) ⊆ ℝ | ||
Theorem | efgh 26597* | 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 26598* | Lemma for efif1o 26602. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) | ||
Theorem | efif1olem2 26599* | Lemma for efif1o 26602. (Contributed by Mario Carneiro, 13-May-2014.) |
⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ) | ||
Theorem | efif1olem3 26600* | Lemma for efif1o 26602. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |