![]() |
Metamath
Proof Explorer Theorem List (p. 265 of 482) | < 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-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sinhalfpip 26401 | The sine of Ο / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (sinβ((Ο / 2) + π΄)) = (cosβπ΄)) | ||
Theorem | sinhalfpim 26402 | The sine of Ο / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (sinβ((Ο / 2) β π΄)) = (cosβπ΄)) | ||
Theorem | coshalfpip 26403 | The cosine of Ο / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ((Ο / 2) + π΄)) = -(sinβπ΄)) | ||
Theorem | coshalfpim 26404 | The cosine of Ο / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ (π΄ β β β (cosβ((Ο / 2) β π΄)) = (sinβπ΄)) | ||
Theorem | ptolemy 26405 | 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 16134, 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 26406 | Lemma for sincosq1sgn 26407. (Contributed by Paul Chapman, 24-Jan-2008.) |
β’ ((π΄ β β β§ 0 < π΄ β§ π΄ < (Ο / 2)) β 0 < (sinβπ΄)) | ||
Theorem | sincosq1sgn 26407 | 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 26408 | 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 26409 | 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 26410 | 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 26411 | Location of the zeroes of cosine in (0[,]Ο). (Contributed by David Moews, 28-Feb-2017.) |
β’ (π΄ β (0[,]Ο) β ((cosβπ΄) = 0 β π΄ = (Ο / 2))) | ||
Theorem | coseq0negpitopi 26412 | Location of the zeroes of cosine in (-Ο(,]Ο). (Contributed by David Moews, 28-Feb-2017.) |
β’ (π΄ β (-Ο(,]Ο) β ((cosβπ΄) = 0 β π΄ β {(Ο / 2), -(Ο / 2)})) | ||
Theorem | tanrpcl 26413 | Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.) |
β’ (π΄ β (0(,)(Ο / 2)) β (tanβπ΄) β β+) | ||
Theorem | tangtx 26414 | 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 26415 | 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 26416 | The sine of a number strictly between 0 and Ο is positive. (Contributed by Paul Chapman, 15-Mar-2008.) |
β’ (π΄ β (0(,)Ο) β 0 < (sinβπ΄)) | ||
Theorem | sinq12ge0 26417 | The sine of a number between 0 and Ο is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ (π΄ β (0[,]Ο) β 0 β€ (sinβπ΄)) | ||
Theorem | sinq34lt0t 26418 | The sine of a number strictly between Ο and 2 Β· Ο is negative. (Contributed by NM, 17-Aug-2008.) |
β’ (π΄ β (Ο(,)(2 Β· Ο)) β (sinβπ΄) < 0) | ||
Theorem | cosq14gt0 26419 | 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 26420 | The cosine of a number between -Ο / 2 and Ο / 2 is nonnegative. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ (π΄ β (-(Ο / 2)[,](Ο / 2)) β 0 β€ (cosβπ΄)) | ||
Theorem | sincosq1eq 26421 | 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 26422 | The sine and cosine of Ο / 4. (Contributed by Paul Chapman, 25-Jan-2008.) |
β’ ((sinβ(Ο / 4)) = (1 / (ββ2)) β§ (cosβ(Ο / 4)) = (1 / (ββ2))) | ||
Theorem | tan4thpi 26423 | The tangent of Ο / 4. (Contributed by Mario Carneiro, 5-Apr-2015.) |
β’ (tanβ(Ο / 4)) = 1 | ||
Theorem | sincos6thpi 26424 | 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 26425 | The sine and cosine of Ο / 3. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ ((sinβ(Ο / 3)) = ((ββ3) / 2) β§ (cosβ(Ο / 3)) = (1 / 2)) | ||
Theorem | pigt3 26426 | Ο is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.) |
β’ 3 < Ο | ||
Theorem | pige3 26427 | Ο is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ 3 β€ Ο | ||
Theorem | pige3ALT 26428 | Alternate proof of pige3 26427. 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 26429 | The absolute value of sine has period Ο. (Contributed by NM, 17-Aug-2008.) |
β’ ((π΄ β β β§ πΎ β β€) β (absβ(sinβ(π΄ + (πΎ Β· Ο)))) = (absβ(sinβπ΄))) | ||
Theorem | sinkpi 26430 | The sine of an integer multiple of Ο is 0. (Contributed by NM, 11-Aug-2008.) |
β’ (πΎ β β€ β (sinβ(πΎ Β· Ο)) = 0) | ||
Theorem | coskpi 26431 | The absolute value of the cosine of an integer multiple of Ο is 1. (Contributed by NM, 19-Aug-2008.) |
β’ (πΎ β β€ β (absβ(cosβ(πΎ Β· Ο))) = 1) | ||
Theorem | sineq0 26432 | 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 26433 | 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 26434 | Cosine is less than one between zero and 2 Β· Ο. (Contributed by Jim Kingdon, 23-Mar-2024.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (cosβπ΄) < 1) | ||
Theorem | cosq34lt1 26435 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
β’ (π΄ β (Ο[,)(2 Β· Ο)) β (cosβπ΄) < 1) | ||
Theorem | efeq1 26436 | 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 26437 | 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 26438 | Lemma for cosord 26439. (Contributed by Mario Carneiro, 10-May-2014.) |
β’ (π β π΄ β (0[,]Ο)) & β’ (π β π΅ β (0[,]Ο)) & β’ (π β π΄ < π΅) β β’ (π β (cosβπ΅) < (cosβπ΄)) | ||
Theorem | cosord 26439 | 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 26440 | 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 26441 | 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 26442 | 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 26443 | 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 26444 | 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 26445 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 26446.) (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 26446 | 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 26447 | 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 26448 | The interval (-Ο(,]Ο) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
β’ (-Ο(,]Ο) β β | ||
Theorem | efgh 26449* | 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 26450* | Lemma for efif1o 26454. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ ((π΄ β β β§ (π₯ β π· β§ π¦ β π·)) β (absβ(π₯ β π¦)) < (2 Β· Ο)) | ||
Theorem | efif1olem2 26451* | Lemma for efif1o 26454. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ ((π΄ β β β§ π§ β β) β βπ¦ β π· ((π§ β π¦) / (2 Β· Ο)) β β€) | ||
Theorem | efif1olem3 26452* | Lemma for efif1o 26454. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) & β’ πΆ = (β‘abs β {1}) β β’ ((π β§ π₯ β πΆ) β (ββ(ββπ₯)) β (-1[,]1)) | ||
Theorem | efif1olem4 26453* | 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 26454* | 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 26455* | 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 26456* | 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 26457 | 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 26458* | 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 26459* | 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 26460 | 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 26461 | 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 26462 | Extend class notation with the natural logarithm function on complex numbers. |
class log | ||
Syntax | ccxp 26463 | Extend class notation with the complex power function. |
class βπ | ||
Definition | df-log 26464 | 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 26465* | 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 26466 | 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 = (β‘β β (-Ο(,]Ο)) | ||
Theorem | ellogrn 26467 | Write out the property π΄ β ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ (π΄ β ran log β (π΄ β β β§ -Ο < (ββπ΄) β§ (ββπ΄) β€ Ο)) | ||
Theorem | dflog2 26468 | The natural logarithm function in terms of the exponential function restricted to its principal domain. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ log = β‘(exp βΎ ran log) | ||
Theorem | relogrn 26469 | The range of the natural logarithm function includes the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 1-Apr-2015.) |
β’ (π΄ β β β π΄ β ran log) | ||
Theorem | logrncn 26470 | The range of the natural logarithm function is a subset of the complex numbers. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ (π΄ β ran log β π΄ β β) | ||
Theorem | eff1o2 26471 | The exponential function restricted to its principal domain maps one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
β’ (exp βΎ ran log):ran logβ1-1-ontoβ(β β {0}) | ||
Theorem | logf1o 26472 | The natural logarithm function maps the nonzero complex numbers one-to-one onto its range. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ log:(β β {0})β1-1-ontoβran log | ||
Theorem | dfrelog 26473 | The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ (log βΎ β+) = β‘(exp βΎ β) | ||
Theorem | relogf1o 26474 | The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ (log βΎ β+):β+β1-1-ontoββ | ||
Theorem | logrncl 26475 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0) β (logβπ΄) β ran log) | ||
Theorem | logcl 26476 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β 0) β (logβπ΄) β β) | ||
Theorem | logimcl 26477 | Closure of the imaginary part of the logarithm function. (Contributed by Mario Carneiro, 23-Sep-2014.) (Revised by Mario Carneiro, 1-Apr-2015.) |
β’ ((π΄ β β β§ π΄ β 0) β (-Ο < (ββ(logβπ΄)) β§ (ββ(logβπ΄)) β€ Ο)) | ||
Theorem | logcld 26478 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 26476. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (logβπ) β β) | ||
Theorem | logimcld 26479 | The imaginary part of the logarithm is in (-Ο(,]Ο). Deduction form of logimcl 26477. Compare logimclad 26480. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (-Ο < (ββ(logβπ)) β§ (ββ(logβπ)) β€ Ο)) | ||
Theorem | logimclad 26480 | The imaginary part of the logarithm is in (-Ο(,]Ο). Alternate form of logimcld 26479. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (ββ(logβπ)) β (-Ο(,]Ο)) | ||
Theorem | abslogimle 26481 | The imaginary part of the logarithm function has absolute value less than pi. (Contributed by Mario Carneiro, 3-Jul-2017.) |
β’ ((π΄ β β β§ π΄ β 0) β (absβ(ββ(logβπ΄))) β€ Ο) | ||
Theorem | logrnaddcl 26482 | The range of the natural logarithm is closed under addition with reals. (Contributed by Mario Carneiro, 3-Apr-2015.) |
β’ ((π΄ β ran log β§ π΅ β β) β (π΄ + π΅) β ran log) | ||
Theorem | relogcl 26483 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (π΄ β β+ β (logβπ΄) β β) | ||
Theorem | eflog 26484 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0) β (expβ(logβπ΄)) = π΄) | ||
Theorem | logeq0im1 26485 | If the logarithm of a number is 0, the number must be 1. (Contributed by David A. Wheeler, 22-Jul-2017.) |
β’ ((π΄ β β β§ π΄ β 0 β§ (logβπ΄) = 0) β π΄ = 1) | ||
Theorem | logccne0 26486 | The logarithm isn't 0 if its argument isn't 0 or 1. (Contributed by David A. Wheeler, 17-Jul-2017.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π΄ β 1) β (logβπ΄) β 0) | ||
Theorem | logne0 26487 | Logarithm of a non-1 positive real number is not zero and thus suitable as a divisor. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Proof shortened by AV, 14-Jun-2020.) |
β’ ((π΄ β β+ β§ π΄ β 1) β (logβπ΄) β 0) | ||
Theorem | reeflog 26488 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (π΄ β β+ β (expβ(logβπ΄)) = π΄) | ||
Theorem | logef 26489 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ (π΄ β ran log β (logβ(expβπ΄)) = π΄) | ||
Theorem | relogef 26490 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (π΄ β β β (logβ(expβπ΄)) = π΄) | ||
Theorem | logeftb 26491 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π΅ β ran log) β ((logβπ΄) = π΅ β (expβπ΅) = π΄)) | ||
Theorem | relogeftb 26492 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π΅ β β) β ((logβπ΄) = π΅ β (expβπ΅) = π΄)) | ||
Theorem | log1 26493 | The natural logarithm of 1. One case of Property 1a of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (logβ1) = 0 | ||
Theorem | loge 26494 | The natural logarithm of e. One case of Property 1b of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (logβe) = 1 | ||
Theorem | logi 26495 | The natural logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
β’ (logβi) = (i Β· (Ο / 2)) | ||
Theorem | logneg 26496 | The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014.) (Revised by Mario Carneiro, 3-Apr-2015.) |
β’ (π΄ β β+ β (logβ-π΄) = ((logβπ΄) + (i Β· Ο))) | ||
Theorem | logm1 26497 | The natural logarithm of negative 1. (Contributed by Paul Chapman, 21-Apr-2008.) (Revised by Mario Carneiro, 13-May-2014.) |
β’ (logβ-1) = (i Β· Ο) | ||
Theorem | lognegb 26498 | If a number has imaginary part equal to Ο, then it is on the negative real axis and vice-versa. (Contributed by Mario Carneiro, 23-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β 0) β (-π΄ β β+ β (ββ(logβπ΄)) = Ο)) | ||
Theorem | relogoprlem 26499 | Lemma for relogmul 26500 and relogdiv 26501. Remark of [Cohen] p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2"). (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (((logβπ΄) β β β§ (logβπ΅) β β) β (expβ((logβπ΄)πΉ(logβπ΅))) = ((expβ(logβπ΄))πΊ(expβ(logβπ΅)))) & β’ (((logβπ΄) β β β§ (logβπ΅) β β) β ((logβπ΄)πΉ(logβπ΅)) β β) β β’ ((π΄ β β+ β§ π΅ β β+) β (logβ(π΄πΊπ΅)) = ((logβπ΄)πΉ(logβπ΅))) | ||
Theorem | relogmul 26500 | The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π΅ β β+) β (logβ(π΄ Β· π΅)) = ((logβπ΄) + (logβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |