| Metamath
Proof Explorer Theorem List (p. 266 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | picn 26501 | π is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.) |
| ⊢ π ∈ ℂ | ||
| Theorem | pipos 26502 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
| ⊢ 0 < π | ||
| Theorem | pirp 26503 | π is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ π ∈ ℝ+ | ||
| Theorem | negpicn 26504 | -π is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -π ∈ ℂ | ||
| Theorem | sinhalfpilem 26505 | Lemma for sinhalfpi 26510 and coshalfpi 26511. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ ((sin‘(π / 2)) = 1 ∧ (cos‘(π / 2)) = 0) | ||
| Theorem | halfpire 26506 | π / 2 is real. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (π / 2) ∈ ℝ | ||
| Theorem | neghalfpire 26507 | -π / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -(π / 2) ∈ ℝ | ||
| Theorem | neghalfpirx 26508 | -π / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ -(π / 2) ∈ ℝ* | ||
| Theorem | pidiv2halves 26509 | Adding π / 2 to itself gives π. See 2halves 12494. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ ((π / 2) + (π / 2)) = π | ||
| Theorem | sinhalfpi 26510 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin‘(π / 2)) = 1 | ||
| Theorem | coshalfpi 26511 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos‘(π / 2)) = 0 | ||
| Theorem | cosneghalfpi 26512 | The cosine of -π / 2 is zero. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (cos‘-(π / 2)) = 0 | ||
| Theorem | efhalfpi 26513 | The exponential of iπ / 2 is i. (Contributed by Mario Carneiro, 9-May-2014.) |
| ⊢ (exp‘(i · (π / 2))) = i | ||
| Theorem | cospi 26514 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos‘π) = -1 | ||
| Theorem | efipi 26515 | 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 26516 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
| ⊢ ((exp‘(i · π)) + 1) = 0 | ||
| Theorem | sin2pi 26517 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin‘(2 · π)) = 0 | ||
| Theorem | cos2pi 26518 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos‘(2 · π)) = 1 | ||
| Theorem | ef2pi 26519 | The exponential of 2πi is 1. (Contributed by Mario Carneiro, 9-May-2014.) |
| ⊢ (exp‘(i · (2 · π))) = 1 | ||
| Theorem | ef2kpi 26520 | 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 26521 | 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 26522 | Lemma for sinper 26523 and cosper 26524. (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 26523 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴)) | ||
| Theorem | cosper 26524 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴)) | ||
| Theorem | sin2kpi 26525 | 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 26526 | 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 26527 | Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴)) | ||
| Theorem | cos2pim 26528 | Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴)) | ||
| Theorem | sinmpi 26529 | Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴)) | ||
| Theorem | cosmpi 26530 | Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴)) | ||
| Theorem | sinppi 26531 | Sine of a number plus π. (Contributed by NM, 10-Aug-2008.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴)) | ||
| Theorem | cosppi 26532 | Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴)) | ||
| Theorem | efimpi 26533 | The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴))) | ||
| Theorem | sinhalfpip 26534 | The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴)) | ||
| Theorem | sinhalfpim 26535 | The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴)) | ||
| Theorem | coshalfpip 26536 | The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴)) | ||
| Theorem | coshalfpim 26537 | The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴)) | ||
| Theorem | ptolemy 26538 | 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 16208, 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 26539 | Lemma for sincosq1sgn 26540. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴)) | ||
| Theorem | sincosq1sgn 26540 | 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 26541 | 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 26542 | 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 26543 | 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 26544 | Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) | ||
| Theorem | coseq0negpitopi 26545 | Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)})) | ||
| Theorem | tanrpcl 26546 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) |
| ⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+) | ||
| Theorem | tangtx 26547 | 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 26548 | 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 26549 | The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴)) | ||
| Theorem | sinq12ge0 26550 | The sine of a number between 0 and π is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
| ⊢ (𝐴 ∈ (0[,]π) → 0 ≤ (sin‘𝐴)) | ||
| Theorem | sinq34lt0t 26551 | The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.) |
| ⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0) | ||
| Theorem | cosq14gt0 26552 | 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 26553 | The cosine of a number between -π / 2 and π / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
| ⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → 0 ≤ (cos‘𝐴)) | ||
| Theorem | sincosq1eq 26554 | 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 26555 | The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.) |
| ⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2))) | ||
| Theorem | tan4thpi 26556 | The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) (Proof shortened by SN, 2-Sep-2025.) |
| ⊢ (tan‘(π / 4)) = 1 | ||
| Theorem | tan4thpiOLD 26557 | Obsolete version of tan4thpi 26556 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 26558 | 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 26559 | The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2)) | ||
| Theorem | pigt3 26560 | π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
| ⊢ 3 < π | ||
| Theorem | pige3 26561 | π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
| ⊢ 3 ≤ π | ||
| Theorem | pige3ALT 26562 | Alternate proof of pige3 26561. 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 26563 | The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴))) | ||
| Theorem | sinkpi 26564 | The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.) |
| ⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0) | ||
| Theorem | coskpi 26565 | The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.) |
| ⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1) | ||
| Theorem | sineq0 26566 | 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 26567 | 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 26568 | Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 23-Mar-2024.) |
| ⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1) | ||
| Theorem | cosq34lt1 26569 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
| ⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1) | ||
| Theorem | efeq1 26570 | 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 26571 | 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 26572 | Lemma for cosord 26573. (Contributed by Mario Carneiro, 10-May-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]π)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴)) | ||
| Theorem | cosord 26573 | 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 26574 | 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 26575 | 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 26576 | 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 26577 | 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 26578 | 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 26579 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 26580.) (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 26580 | 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 26581 | 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 26582 | The interval (-π(,]π) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (-π(,]π) ⊆ ℝ | ||
| Theorem | efgh 26583* | 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 26584* | Lemma for efif1o 26588. (Contributed by Mario Carneiro, 13-May-2014.) |
| ⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (abs‘(𝑥 − 𝑦)) < (2 · π)) | ||
| Theorem | efif1olem2 26585* | Lemma for efif1o 26588. (Contributed by Mario Carneiro, 13-May-2014.) |
| ⊢ 𝐷 = (𝐴(,](𝐴 + (2 · π))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ∃𝑦 ∈ 𝐷 ((𝑧 − 𝑦) / (2 · π)) ∈ ℤ) | ||
| Theorem | efif1olem3 26586* | Lemma for efif1o 26588. (Contributed by Mario Carneiro, 8-May-2015.) |
| ⊢ 𝐹 = (𝑤 ∈ 𝐷 ↦ (exp‘(i · 𝑤))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (ℑ‘(√‘𝑥)) ∈ (-1[,]1)) | ||
| Theorem | efif1olem4 26587* | 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 26588* | 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 26589* | 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 26590* | 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 26591 | 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 26592* | 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 26593* | 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 26594 | 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 26595 | 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)) | ||
| Syntax | clog 26596 | Extend class notation with the natural logarithm function on complex numbers. |
| class log | ||
| Syntax | ccxp 26597 | Extend class notation with the complex power function. |
| class ↑𝑐 | ||
| Definition | df-log 26598 | Define the natural logarithm function on complex numbers. It is defined as the principal value, that is, the inverse of the exponential whose imaginary part lies in the interval (-pi, pi]. See http://en.wikipedia.org/wiki/Natural_logarithm and https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Paul Chapman, 21-Apr-2008.) |
| ⊢ log = ◡(exp ↾ (◡ℑ “ (-π(,]π))) | ||
| Definition | df-cxp 26599* | Define the power function on complex numbers. Note that the value of this function when 𝑥 = 0 and (ℜ‘𝑦) ≤ 0, 𝑦 ≠ 0 should properly be undefined, but defining it by convention this way simplifies the domain. (Contributed by Mario Carneiro, 2-Aug-2014.) |
| ⊢ ↑𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))) | ||
| Theorem | logrn 26600 | The range of the natural logarithm function, also the principal domain of the exponential function. This allows to write the longer class expression as simply ran log. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
| ⊢ ran log = (◡ℑ “ (-π(,]π)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |