P. 153 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15201-15300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	picn 15201	pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- pi e. CC
Theorem	pipos 15202	pi is positive. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- 0 < pi
Theorem	pirp 15203	pi is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- pi e. RR+
Theorem	negpicn 15204	-u pi is a real number. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u pi e. CC
Theorem	sinhalfpilem 15205	Lemma for sinhalfpi 15210 and coshalfpi 15211. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( ( sin ` ( pi / 2 ) ) = 1 /\ ( cos ` ( pi / 2 ) ) = 0 )
Theorem	halfpire 15206	pi / 2 is real. (Contributed by David Moews, 28-Feb-2017.)
|- ( pi / 2 ) e. RR
Theorem	neghalfpire 15207	-u pi / 2 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR
Theorem	neghalfpirx 15208	-u pi / 2 is an extended real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -u ( pi / 2 ) e. RR*
Theorem	pidiv2halves 15209	Adding pi / 2 to itself gives pi. See 2halves 9265. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ( pi / 2 ) + ( pi / 2 ) ) = pi
Theorem	sinhalfpi 15210	The sine of pi / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( pi / 2 ) ) = 1
Theorem	coshalfpi 15211	The cosine of pi / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( pi / 2 ) ) = 0
Theorem	cosneghalfpi 15212	The cosine of -u pi / 2 is zero. (Contributed by David Moews, 28-Feb-2017.)
|- ( cos ` -u ( pi / 2 ) ) = 0
Theorem	efhalfpi 15213	The exponential of _i pi / 2 is _i. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( pi / 2 ) ) ) = _i
Theorem	cospi 15214	The cosine of pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` pi ) = -u 1
Theorem	efipi 15215	The exponential of _i x. pi is -u 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( exp ` ( _i x. pi ) ) = -u 1
Theorem	eulerid 15216	Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( ( exp ` ( _i x. pi ) ) + 1 ) = 0
Theorem	sin2pi 15217	The sine of 2 pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( sin ` ( 2 x. pi ) ) = 0
Theorem	cos2pi 15218	The cosine of 2 pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
|- ( cos ` ( 2 x. pi ) ) = 1
Theorem	ef2pi 15219	The exponential of 2 pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( exp ` ( _i x. ( 2 x. pi ) ) ) = 1
Theorem	ef2kpi 15220	If K is an integer, then the exponential of 2 K pi _i is 1. (Contributed by Mario Carneiro, 9-May-2014.)
|- ( K e. ZZ -> ( exp ` ( ( _i x. ( 2 x. pi ) ) x. K ) ) = 1 )
Theorem	efper 15221	The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( exp ` ( A + ( ( _i x. ( 2 x. pi ) ) x. K ) ) ) = ( exp ` A ) )
Theorem	sinperlem 15222	Lemma for sinper 15223 and cosper 15224. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( A e. CC -> ( F ` A ) = ( ( ( exp ` ( _i x. A ) ) O ( exp ` ( -u _i x. A ) ) ) / D ) )   &    |- ( ( A + ( K x. ( 2 x. pi ) ) ) e. CC -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( ( ( exp ` ( _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) O ( exp ` ( -u _i x. ( A + ( K x. ( 2 x. pi ) ) ) ) ) ) / D ) )   =>    |- ( ( A e. CC /\ K e. ZZ ) -> ( F ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( F ` A ) )
Theorem	sinper 15223	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( sin ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( sin ` A ) )
Theorem	cosper 15224	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( cos ` ( A + ( K x. ( 2 x. pi ) ) ) ) = ( cos ` A ) )
Theorem	sin2kpi 15225	If K is an integer, then the sine of 2 K pi is 0. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( sin ` ( K x. ( 2 x. pi ) ) ) = 0 )
Theorem	cos2kpi 15226	If K is an integer, then the cosine of 2 K pi is 1. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( K e. ZZ -> ( cos ` ( K x. ( 2 x. pi ) ) ) = 1 )
Theorem	sin2pim 15227	Sine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( ( 2 x. pi ) - A ) ) = -u ( sin ` A ) )
Theorem	cos2pim 15228	Cosine of a number subtracted from 2 x. pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( ( 2 x. pi ) - A ) ) = ( cos ` A ) )
Theorem	sinmpi 15229	Sine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( sin ` ( A - pi ) ) = -u ( sin ` A ) )
Theorem	cosmpi 15230	Cosine of a number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( cos ` ( A - pi ) ) = -u ( cos ` A ) )
Theorem	sinppi 15231	Sine of a number plus pi. (Contributed by NM, 10-Aug-2008.)
|- ( A e. CC -> ( sin ` ( A + pi ) ) = -u ( sin ` A ) )
Theorem	cosppi 15232	Cosine of a number plus pi. (Contributed by NM, 18-Aug-2008.)
|- ( A e. CC -> ( cos ` ( A + pi ) ) = -u ( cos ` A ) )
Theorem	efimpi 15233	The exponential function at _i times a real number less pi. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. CC -> ( exp ` ( _i x. ( A - pi ) ) ) = -u ( exp ` ( _i x. A ) ) )
Theorem	sinhalfpip 15234	The sine of pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( sin ` ( ( pi / 2 ) + A ) ) = ( cos ` A ) )
Theorem	sinhalfpim 15235	The sine of pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( sin ` ( ( pi / 2 ) - A ) ) = ( cos ` A ) )
Theorem	coshalfpip 15236	The cosine of pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( ( pi / 2 ) + A ) ) = -u ( sin ` A ) )
Theorem	coshalfpim 15237	The cosine of pi / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( ( pi / 2 ) - A ) ) = ( sin ` A ) )
Theorem	ptolemy 15238	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 11997, 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.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ ( ( A + B ) + ( C + D ) ) = pi ) -> ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` C ) x. ( sin ` D ) ) ) = ( ( sin ` ( B + C ) ) x. ( sin ` ( A + C ) ) ) )
Theorem	sincosq1lem 15239	Lemma for sincosq1sgn 15240. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( ( A e. RR /\ 0 < A /\ A < ( pi / 2 ) ) -> 0 < ( sin ` A ) )
Theorem	sincosq1sgn 15240	The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> ( 0 < ( sin ` A ) /\ 0 < ( cos ` A ) ) )
Theorem	sincosq2sgn 15241	The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( ( pi / 2 ) (,) pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )
Theorem	sincosq3sgn 15242	The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( pi (,) ( 3 x. ( pi / 2 ) ) ) -> ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) )
Theorem	sincosq4sgn 15243	The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. ( ( 3 x. ( pi / 2 ) ) (,) ( 2 x. pi ) ) -> ( ( sin ` A ) < 0 /\ 0 < ( cos ` A ) ) )
Theorem	sinq12gt0 15244	The sine of a number strictly between 0 and pi is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( A e. ( 0 (,) pi ) -> 0 < ( sin ` A ) )
Theorem	sinq34lt0t 15245	The sine of a number strictly between pi and 2 x. pi is negative. (Contributed by NM, 17-Aug-2008.)
|- ( A e. ( pi (,) ( 2 x. pi ) ) -> ( sin ` A ) < 0 )
Theorem	cosq14gt0 15246	The cosine of a number strictly between -u pi / 2 and pi / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( A e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) -> 0 < ( cos ` A ) )
Theorem	cosq23lt0 15247	The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.)
|- ( A e. ( ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ) -> ( cos ` A ) < 0 )
Theorem	coseq0q4123 15248	Location of the zeroes of cosine in ( -u ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ). (Contributed by Jim Kingdon, 14-Mar-2024.)
|- ( A e. ( -u ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ) -> ( ( cos ` A ) = 0 <-> A = ( pi / 2 ) ) )
Theorem	coseq00topi 15249	Location of the zeroes of cosine in ( 0 [,] pi ). (Contributed by David Moews, 28-Feb-2017.)
|- ( A e. ( 0 [,] pi ) -> ( ( cos ` A ) = 0 <-> A = ( pi / 2 ) ) )
Theorem	coseq0negpitopi 15250	Location of the zeroes of cosine in ( -u pi (,] pi ). (Contributed by David Moews, 28-Feb-2017.)
|- ( A e. ( -u pi (,] pi ) -> ( ( cos ` A ) = 0 <-> A e. { ( pi / 2 ) , -u ( pi / 2 ) } ) )
Theorem	tanrpcl 15251	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> ( tan ` A ) e. RR+ )
Theorem	tangtx 15252	The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. ( 0 (,) ( pi / 2 ) ) -> A < ( tan ` A ) )
Theorem	sincosq1eq 15253	Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( A e. CC /\ B e. CC /\ ( A + B ) = 1 ) -> ( sin ` ( A x. ( pi / 2 ) ) ) = ( cos ` ( B x. ( pi / 2 ) ) ) )
Theorem	sincos4thpi 15254	The sine and cosine of pi / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
|- ( ( sin ` ( pi / 4 ) ) = ( 1 / ( sqr ` 2 ) ) /\ ( cos ` ( pi / 4 ) ) = ( 1 / ( sqr ` 2 ) ) )
Theorem	tan4thpi 15255	The tangent of pi / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( tan ` ( pi / 4 ) ) = 1
Theorem	sincos6thpi 15256	The sine and cosine of pi / 6. (Contributed by Paul Chapman, 25-Jan-2008.) (Revised by Wolf Lammen, 24-Sep-2020.)
|- ( ( sin ` ( pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( pi / 6 ) ) = ( ( sqr ` 3 ) / 2 ) )
Theorem	sincos3rdpi 15257	The sine and cosine of pi / 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- ( ( sin ` ( pi / 3 ) ) = ( ( sqr ` 3 ) / 2 ) /\ ( cos ` ( pi / 3 ) ) = ( 1 / 2 ) )
Theorem	pigt3 15258	pi is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
|- 3 < pi
Theorem	pige3 15259	pi is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
|- 3 <_ pi
Theorem	abssinper 15260	The absolute value of sine has period pi. (Contributed by NM, 17-Aug-2008.)
|- ( ( A e. CC /\ K e. ZZ ) -> ( abs ` ( sin ` ( A + ( K x. pi ) ) ) ) = ( abs ` ( sin ` A ) ) )
Theorem	sinkpi 15261	The sine of an integer multiple of pi is 0. (Contributed by NM, 11-Aug-2008.)
|- ( K e. ZZ -> ( sin ` ( K x. pi ) ) = 0 )
Theorem	coskpi 15262	The absolute value of the cosine of an integer multiple of pi is 1. (Contributed by NM, 19-Aug-2008.)
|- ( K e. ZZ -> ( abs ` ( cos ` ( K x. pi ) ) ) = 1 )
Theorem	cosordlem 15263	Cosine is decreasing over the closed interval from 0 to pi. (Contributed by Mario Carneiro, 10-May-2014.)
|- ( ph -> A e. ( 0 [,] pi ) )   &    |- ( ph -> B e. ( 0 [,] pi ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( cos ` B ) < ( cos ` A ) )
Theorem	cosq34lt1 15264	Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.)
|- ( A e. ( pi [,) ( 2 x. pi ) ) -> ( cos ` A ) < 1 )
Theorem	cos02pilt1 15265	Cosine is less than one between zero and 2 x. pi. (Contributed by Jim Kingdon, 19-Mar-2024.)
|- ( A e. ( 0 (,) ( 2 x. pi ) ) -> ( cos ` A ) < 1 )
Theorem	cos0pilt1 15266	Cosine is between minus one and one on the open interval between zero and pi. (Contributed by Jim Kingdon, 7-May-2024.)
|- ( A e. ( 0 (,) pi ) -> ( cos ` A ) e. ( -u 1 (,) 1 ) )
Theorem	cos11 15267	Cosine is one-to-one over the closed interval from 0 to pi. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon, 6-May-2024.)
|- ( ( A e. ( 0 [,] pi ) /\ B e. ( 0 [,] pi ) ) -> ( A = B <-> ( cos ` A ) = ( cos ` B ) ) )
Theorem	ioocosf1o 15268	The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Jim Kingdon, 7-May-2024.)
|- ( cos |` ( 0 (,) pi ) ) : ( 0 (,) pi ) -1-1-onto-> ( -u 1 (,) 1 )
Theorem	negpitopissre 15269	The interval ( -u pi (,] pi ) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
|- ( -u pi (,] pi ) C_ RR
11.2.3  The natural logarithm on complex numbers
Syntax	clog 15270	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 15271	Extend class notation with the complex power function.
class ^c
Definition	df-relog 15272	Define the natural logarithm function. Defining the logarithm on complex numbers is similar to square root - there are ways to define it but they tend to make use of excluded middle. Therefore, we merely define logarithms on positive reals. See http://en.wikipedia.org/wiki/Natural_logarithm and https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Jim Kingdon, 14-May-2024.)
|- log = `' ( exp |` RR )
Definition	df-rpcxp 15273*	Define the power function on complex numbers. Because df-relog 15272 is only defined on positive reals, this definition only allows for a base which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.)
|- ^c = ( x e. RR+ , y e. CC |-> ( exp ` ( y x. ( log ` x ) ) ) )
Theorem	dfrelog 15274	The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( log |` RR+ ) = `' ( exp |` RR )
Theorem	relogf1o 15275	The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR
Theorem	relogcl 15276	Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR+ -> ( log ` A ) e. RR )
Theorem	reeflog 15277	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
Theorem	relogef 15278	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR -> ( log ` ( exp ` A ) ) = A )
Theorem	relogeftb 15279	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
Theorem	log1 15280	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 15281	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	relogoprlem 15282	Lemma for relogmul 15283 and relogdiv 15284. 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 ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) F ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) )   &    |- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) F ( log ` B ) ) e. RR )   =>    |- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A G B ) ) = ( ( log ` A ) F ( log ` B ) ) )
Theorem	relogmul 15283	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.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	relogdiv 15284	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.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	reexplog 15285	Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
Theorem	relogexp 15286	The natural logarithm of positive A raised to an integer power. Property 4 of [Cohen] p. 301-302, restricted to natural logarithms and integer powers N. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( A ^ N ) ) = ( N x. ( log ` A ) ) )
Theorem	relogiso 15287	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 |` RR+ ) Isom < , < ( RR+ , RR )
Theorem	logltb 15288	The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )
Theorem	logleb 15289	Natural logarithm preserves <_. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
Theorem	logrpap0b 15290	The logarithm is apart from 0 if and only if its argument is apart from 1. (Contributed by Jim Kingdon, 3-Jul-2024.)
|- ( A e. RR+ -> ( A # 1 <-> ( log ` A ) # 0 ) )
Theorem	logrpap0 15291	The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.)
|- ( ( A e. RR+ /\ A # 1 ) -> ( log ` A ) # 0 )
Theorem	logrpap0d 15292	Deduction form of logrpap0 15291. (Contributed by Jim Kingdon, 3-Jul-2024.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> A # 1 )   =>    |- ( ph -> ( log ` A ) # 0 )
Theorem	rplogcl 15293	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )
Theorem	logge0 15294	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 1 <_ A ) -> 0 <_ ( log ` A ) )
Theorem	logdivlti 15295	The log x / x function is strictly decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) )
Theorem	relogcld 15296	Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( log ` A ) e. RR )
Theorem	reeflogd 15297	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( exp ` ( log ` A ) ) = A )
Theorem	relogmuld 15298	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 Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	relogdivd 15299	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 Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	logled 15300	Natural logarithm preserves <_. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )