Home | Metamath
Proof Explorer Theorem List (p. 259 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coskpi 25801 | The absolute value of the cosine of an integer multiple of Ο is 1. (Contributed by NM, 19-Aug-2008.) |
β’ (πΎ β β€ β (absβ(cosβ(πΎ Β· Ο))) = 1) | ||
Theorem | sineq0 25802 | 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 25803 | 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 25804 | Cosine is less than one between zero and 2 Β· Ο. (Contributed by Jim Kingdon, 23-Mar-2024.) |
β’ (π΄ β (0(,)(2 Β· Ο)) β (cosβπ΄) < 1) | ||
Theorem | cosq34lt1 25805 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 23-Mar-2024.) |
β’ (π΄ β (Ο[,)(2 Β· Ο)) β (cosβπ΄) < 1) | ||
Theorem | efeq1 25806 | 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 25807 | 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 25808 | Lemma for cosord 25809. (Contributed by Mario Carneiro, 10-May-2014.) |
β’ (π β π΄ β (0[,]Ο)) & β’ (π β π΅ β (0[,]Ο)) & β’ (π β π΄ < π΅) β β’ (π β (cosβπ΅) < (cosβπ΄)) | ||
Theorem | cosord 25809 | 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 25810 | 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 25811 | 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 25812 | 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 25813 | 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 25814 | 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 25815 | The tangent function is strictly increasing on the nonnegative part of its principal domain. (Lemma for tanord 25816.) (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 25816 | 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 25817 | 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 25818 | The interval (-Ο(,]Ο) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
β’ (-Ο(,]Ο) β β | ||
Theorem | efgh 25819* | 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 25820* | Lemma for efif1o 25824. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ ((π΄ β β β§ (π₯ β π· β§ π¦ β π·)) β (absβ(π₯ β π¦)) < (2 Β· Ο)) | ||
Theorem | efif1olem2 25821* | Lemma for efif1o 25824. (Contributed by Mario Carneiro, 13-May-2014.) |
β’ π· = (π΄(,](π΄ + (2 Β· Ο))) β β’ ((π΄ β β β§ π§ β β) β βπ¦ β π· ((π§ β π¦) / (2 Β· Ο)) β β€) | ||
Theorem | efif1olem3 25822* | Lemma for efif1o 25824. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ πΉ = (π€ β π· β¦ (expβ(i Β· π€))) & β’ πΆ = (β‘abs β {1}) β β’ ((π β§ π₯ β πΆ) β (ββ(ββπ₯)) β (-1[,]1)) | ||
Theorem | efif1olem4 25823* | 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 25824* | 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 25825* | 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 25826* | 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 25827 | 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 25828* | 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 25829* | 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 25830 | 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 25831 | 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 25832 | Extend class notation with the natural logarithm function on complex numbers. |
class log | ||
Syntax | ccxp 25833 | Extend class notation with the complex power function. |
class βπ | ||
Definition | df-log 25834 | 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 25835* | 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 25836 | 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 25837 | Write out the property π΄ β ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ (π΄ β ran log β (π΄ β β β§ -Ο < (ββπ΄) β§ (ββπ΄) β€ Ο)) | ||
Theorem | dflog2 25838 | 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 25839 | 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 25840 | 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 25841 | 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 25842 | 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 25843 | 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 25844 | 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 25845 | Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0) β (logβπ΄) β ran log) | ||
Theorem | logcl 25846 | Closure of the natural logarithm function. (Contributed by NM, 21-Apr-2008.) (Revised by Mario Carneiro, 23-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β 0) β (logβπ΄) β β) | ||
Theorem | logimcl 25847 | 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 25848 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 25846. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (logβπ) β β) | ||
Theorem | logimcld 25849 | The imaginary part of the logarithm is in (-Ο(,]Ο). Deduction form of logimcl 25847. Compare logimclad 25850. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (-Ο < (ββ(logβπ)) β§ (ββ(logβπ)) β€ Ο)) | ||
Theorem | logimclad 25850 | The imaginary part of the logarithm is in (-Ο(,]Ο). Alternate form of logimcld 25849. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (ββ(logβπ)) β (-Ο(,]Ο)) | ||
Theorem | abslogimle 25851 | 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 25852 | 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 25853 | Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (π΄ β β+ β (logβπ΄) β β) | ||
Theorem | eflog 25854 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0) β (expβ(logβπ΄)) = π΄) | ||
Theorem | logeq0im1 25855 | 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 25856 | 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 25857 | 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 25858 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (π΄ β β+ β (expβ(logβπ΄)) = π΄) | ||
Theorem | logef 25859 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ (π΄ β ran log β (logβ(expβπ΄)) = π΄) | ||
Theorem | relogef 25860 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (π΄ β β β (logβ(expβπ΄)) = π΄) | ||
Theorem | logeftb 25861 | Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π΅ β ran log) β ((logβπ΄) = π΅ β (expβπ΅) = π΄)) | ||
Theorem | relogeftb 25862 | Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π΅ β β) β ((logβπ΄) = π΅ β (expβπ΅) = π΄)) | ||
Theorem | log1 25863 | 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 25864 | 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 | logneg 25865 | 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 25866 | 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 25867 | 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 25868 | Lemma for relogmul 25869 and relogdiv 25870. 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 25869 | 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βπ΅))) | ||
Theorem | relogdiv 25870 | The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π΅ β β+) β (logβ(π΄ / π΅)) = ((logβπ΄) β (logβπ΅))) | ||
Theorem | explog 25871 | Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β (π΄βπ) = (expβ(π Β· (logβπ΄)))) | ||
Theorem | reexplog 25872 | Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π β β€) β (π΄βπ) = (expβ(π Β· (logβπ΄)))) | ||
Theorem | relogexp 25873 | The natural logarithm of positive π΄ raised to an integer power. Property 4 of [Cohen] p. 301-302, restricted to natural logarithms and integer powers π. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π β β€) β (logβ(π΄βπ)) = (π Β· (logβπ΄))) | ||
Theorem | relog 25874 | Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β 0) β (ββ(logβπ΄)) = (logβ(absβπ΄))) | ||
Theorem | relogiso 25875 | The natural logarithm function on positive reals determines an isomorphism from the positive reals onto the reals. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (log βΎ β+) Isom < , < (β+, β) | ||
Theorem | reloggim 25876 | The natural logarithm is a group isomorphism from the group of positive reals under multiplication to the group of reals under addition. (Contributed by Mario Carneiro, 21-Jun-2015.) (Revised by Thierry Arnoux, 30-Jun-2019.) |
β’ π = ((mulGrpββfld) βΎs β+) β β’ (log βΎ β+) β (π GrpIso βfld) | ||
Theorem | logltb 25877 | The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ ((π΄ β β+ β§ π΅ β β+) β (π΄ < π΅ β (logβπ΄) < (logβπ΅))) | ||
Theorem | logfac 25878* | The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015.) |
β’ (π β β0 β (logβ(!βπ)) = Ξ£π β (1...π)(logβπ)) | ||
Theorem | eflogeq 25879* | Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β ((expβπ΄) = π΅ β βπ β β€ π΄ = ((logβπ΅) + ((i Β· (2 Β· Ο)) Β· π)))) | ||
Theorem | logleb 25880 | Natural logarithm preserves β€. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β+) β (π΄ β€ π΅ β (logβπ΄) β€ (logβπ΅))) | ||
Theorem | rplogcl 25881 | Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.) |
β’ ((π΄ β β β§ 1 < π΄) β (logβπ΄) β β+) | ||
Theorem | logge0 25882 | The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ 1 β€ π΄) β 0 β€ (logβπ΄)) | ||
Theorem | logcj 25883 | The natural logarithm distributes under conjugation away from the branch cut. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ (ββπ΄) β 0) β (logβ(ββπ΄)) = (ββ(logβπ΄))) | ||
Theorem | efiarg 25884 | The exponential of the "arg" function β β log. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ π΄ β 0) β (expβ(i Β· (ββ(logβπ΄)))) = (π΄ / (absβπ΄))) | ||
Theorem | cosargd 25885 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 25884. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β (cosβ(ββ(logβπ))) = ((ββπ) / (absβπ))) | ||
Theorem | cosarg0d 25886 | The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β 0) β β’ (π β ((cosβ(ββ(logβπ))) = 0 β (ββπ) = 0)) | ||
Theorem | argregt0 25887 | Closure of the argument of a complex number with positive real part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ 0 < (ββπ΄)) β (ββ(logβπ΄)) β (-(Ο / 2)(,)(Ο / 2))) | ||
Theorem | argrege0 25888 | Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015.) |
β’ ((π΄ β β β§ π΄ β 0 β§ 0 β€ (ββπ΄)) β (ββ(logβπ΄)) β (-(Ο / 2)[,](Ο / 2))) | ||
Theorem | argimgt0 25889 | Closure of the argument of a complex number with positive imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ 0 < (ββπ΄)) β (ββ(logβπ΄)) β (0(,)Ο)) | ||
Theorem | argimlt0 25890 | Closure of the argument of a complex number with negative imaginary part. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ (ββπ΄) < 0) β (ββ(logβπ΄)) β (-Ο(,)0)) | ||
Theorem | logimul 25891 | Multiplying a number by i increases the logarithm of the number by iΟ / 2. (Contributed by Mario Carneiro, 4-Apr-2015.) |
β’ ((π΄ β β β§ π΄ β 0 β§ 0 β€ (ββπ΄)) β (logβ(i Β· π΄)) = ((logβπ΄) + (i Β· (Ο / 2)))) | ||
Theorem | logneg2 25892 | The logarithm of the negative of a number with positive imaginary part is i Β· Ο less than the original. (Compare logneg 25865.) (Contributed by Mario Carneiro, 3-Apr-2015.) |
β’ ((π΄ β β β§ 0 < (ββπ΄)) β (logβ-π΄) = ((logβπ΄) β (i Β· Ο))) | ||
Theorem | logmul2 25893 | Generalization of relogmul 25869 to a complex left argument. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π΅ β β+) β (logβ(π΄ Β· π΅)) = ((logβπ΄) + (logβπ΅))) | ||
Theorem | logdiv2 25894 | Generalization of relogdiv 25870 to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π΅ β β+) β (logβ(π΄ / π΅)) = ((logβπ΄) β (logβπ΅))) | ||
Theorem | abslogle 25895 | Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017.) |
β’ ((π΄ β β β§ π΄ β 0) β (absβ(logβπ΄)) β€ ((absβ(logβ(absβπ΄))) + Ο)) | ||
Theorem | tanarg 25896 | The basic relation between the "arg" function β β log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015.) |
β’ ((π΄ β β β§ (ββπ΄) β 0) β (tanβ(ββ(logβπ΄))) = ((ββπ΄) / (ββπ΄))) | ||
Theorem | logdivlti 25897 | The logπ₯ / π₯ function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ e β€ π΄) β§ π΄ < π΅) β ((logβπ΅) / π΅) < ((logβπ΄) / π΄)) | ||
Theorem | logdivlt 25898 | The logπ₯ / π₯ function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.) |
β’ (((π΄ β β β§ e β€ π΄) β§ (π΅ β β β§ e β€ π΅)) β (π΄ < π΅ β ((logβπ΅) / π΅) < ((logβπ΄) / π΄))) | ||
Theorem | logdivle 25899 | The logπ₯ / π₯ function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 3-May-2016.) |
β’ (((π΄ β β β§ e β€ π΄) β§ (π΅ β β β§ e β€ π΅)) β (π΄ β€ π΅ β ((logβπ΅) / π΅) β€ ((logβπ΄) / π΄))) | ||
Theorem | relogcld 25900 | Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β+) β β’ (π β (logβπ΄) β β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |