P. 159 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15801-15900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	efper 15801	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 15802	Lemma for sinper 15803 and cosper 15804. (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 15803	The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (sin‘(𝐴 + (𝐾 · (2 · π)))) = (sin‘𝐴))
Theorem	cosper 15804	The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (cos‘(𝐴 + (𝐾 · (2 · π)))) = (cos‘𝐴))
Theorem	sin2kpi 15805	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 15806	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 15807	Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((2 · π) − 𝐴)) = -(sin‘𝐴))
Theorem	cos2pim 15808	Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((2 · π) − 𝐴)) = (cos‘𝐴))
Theorem	sinmpi 15809	Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 − π)) = -(sin‘𝐴))
Theorem	cosmpi 15810	Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 − π)) = -(cos‘𝐴))
Theorem	sinppi 15811	Sine of a number plus π. (Contributed by NM, 10-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘(𝐴 + π)) = -(sin‘𝐴))
Theorem	cosppi 15812	Cosine of a number plus π. (Contributed by NM, 18-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘(𝐴 + π)) = -(cos‘𝐴))
Theorem	efimpi 15813	The exponential function at i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · (𝐴 − π))) = -(exp‘(i · 𝐴)))
Theorem	sinhalfpip 15814	The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) + 𝐴)) = (cos‘𝐴))
Theorem	sinhalfpim 15815	The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
Theorem	coshalfpip 15816	The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) + 𝐴)) = -(sin‘𝐴))
Theorem	coshalfpim 15817	The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ (𝐴 ∈ ℂ → (cos‘((π / 2) − 𝐴)) = (sin‘𝐴))
Theorem	ptolemy 15818	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 12458, 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 15819	Lemma for sincosq1sgn 15820. (Contributed by Paul Chapman, 24-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < (π / 2)) → 0 < (sin‘𝐴))
Theorem	sincosq1sgn 15820	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 15821	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 15822	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 15823	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	sinq12gt0 15824	The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ (𝐴 ∈ (0(,)π) → 0 < (sin‘𝐴))
Theorem	sinq34lt0t 15825	The sine of a number strictly between π and 2 · π is negative. (Contributed by NM, 17-Aug-2008.)
⊢ (𝐴 ∈ (π(,)(2 · π)) → (sin‘𝐴) < 0)
Theorem	cosq14gt0 15826	The cosine of a number strictly between -π / 2 and π / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ (𝐴 ∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘𝐴))
Theorem	cosq23lt0 15827	The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.)
⊢ (𝐴 ∈ ((π / 2)(,)(3 · (π / 2))) → (cos‘𝐴) < 0)
Theorem	coseq0q4123 15828	Location of the zeroes of cosine in (-(π / 2)(,)(3 · (π / 2))). (Contributed by Jim Kingdon, 14-Mar-2024.)
⊢ (𝐴 ∈ (-(π / 2)(,)(3 · (π / 2))) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq00topi 15829	Location of the zeroes of cosine in (0[,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (0[,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2)))
Theorem	coseq0negpitopi 15830	Location of the zeroes of cosine in (-π(,]π). (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝐴 ∈ (-π(,]π) → ((cos‘𝐴) = 0 ↔ 𝐴 ∈ {(π / 2), -(π / 2)}))
Theorem	tanrpcl 15831	Positive real closure of the tangent function. (Contributed by Mario Carneiro, 29-Jul-2014.)
⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
Theorem	tangtx 15832	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	sincosq1eq 15833	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 15834	The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.)
⊢ ((sin‘(π / 4)) = (1 / (√‘2)) ∧ (cos‘(π / 4)) = (1 / (√‘2)))
Theorem	tan4thpi 15835	The tangent of π / 4. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (tan‘(π / 4)) = 1
Theorem	sincos6thpi 15836	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 15837	The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
Theorem	pigt3 15838	π is greater than 3. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ 3 < π
Theorem	pige3 15839	π is greater than or equal to 3. (Contributed by Mario Carneiro, 21-May-2016.)
⊢ 3 ≤ π
Theorem	abssinper 15840	The absolute value of sine has period π. (Contributed by NM, 17-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (abs‘(sin‘(𝐴 + (𝐾 · π)))) = (abs‘(sin‘𝐴)))
Theorem	sinkpi 15841	The sine of an integer multiple of π is 0. (Contributed by NM, 11-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (sin‘(𝐾 · π)) = 0)
Theorem	coskpi 15842	The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.)
⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)
Theorem	cosordlem 15843	Cosine is decreasing over the closed interval from 0 to π. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝜑 → 𝐴 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]π))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (cos‘𝐵) < (cos‘𝐴))
Theorem	cosq34lt1 15844	Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.)
⊢ (𝐴 ∈ (π[,)(2 · π)) → (cos‘𝐴) < 1)
Theorem	cos02pilt1 15845	Cosine is less than one between zero and 2 · π. (Contributed by Jim Kingdon, 19-Mar-2024.)
⊢ (𝐴 ∈ (0(,)(2 · π)) → (cos‘𝐴) < 1)
Theorem	cos0pilt1 15846	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 15847	Cosine is one-to-one over the closed interval from 0 to π. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon, 6-May-2024.)
⊢ ((𝐴 ∈ (0[,]π) ∧ 𝐵 ∈ (0[,]π)) → (𝐴 = 𝐵 ↔ (cos‘𝐴) = (cos‘𝐵)))
Theorem	ioocosf1o 15848	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(,)π)):(0(,)π)–1-1-onto→(-1(,)1)
Theorem	negpitopissre 15849	The interval (-π(,]π) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.)
⊢ (-π(,]π) ⊆ ℝ
11.2.3  The natural logarithm on complex numbers
Syntax	clog 15850	Extend class notation with the natural logarithm function on complex numbers.
class log
Syntax	ccxp 15851	Extend class notation with the complex power function.
class ↑𝑐
Definition	df-relog 15852	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 ↾ ℝ)
Definition	df-rpcxp 15853*	Define the power function on complex numbers. Because df-relog 15852 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.)
⊢ ↑𝑐 = (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (exp‘(𝑦 · (log‘𝑥))))
Theorem	dfrelog 15854	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 15855	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	relogcl 15856	Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ∈ ℝ)
Theorem	reeflog 15857	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ+ → (exp‘(log‘𝐴)) = 𝐴)
Theorem	relogef 15858	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (𝐴 ∈ ℝ → (log‘(exp‘𝐴)) = 𝐴)
Theorem	relogeftb 15859	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → ((log‘𝐴) = 𝐵 ↔ (exp‘𝐵) = 𝐴))
Theorem	log1 15860	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 15861	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 15862	Lemma for relogmul 15863 and relogdiv 15864. 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 15863	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 15864	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	reexplog 15865	Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = (exp‘(𝑁 · (log‘𝐴))))
Theorem	relogexp 15866	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	relogiso 15867	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	logltb 15868	The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (log‘𝐴) < (log‘𝐵)))
Theorem	logleb 15869	Natural logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵)))
Theorem	logrpap0b 15870	The logarithm is apart from 0 if and only if its argument is apart from 1. (Contributed by Jim Kingdon, 3-Jul-2024.)
⊢ (𝐴 ∈ ℝ+ → (𝐴 # 1 ↔ (log‘𝐴) # 0))
Theorem	logrpap0 15871	The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 # 1) → (log‘𝐴) # 0)
Theorem	logrpap0d 15872	Deduction form of logrpap0 15871. (Contributed by Jim Kingdon, 3-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 # 1)    ⇒   ⊢ (𝜑 → (log‘𝐴) # 0)
Theorem	rplogcl 15873	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (log‘𝐴) ∈ ℝ+)
Theorem	logge0 15874	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴))
Theorem	logdivlti 15875	The log𝑥 / 𝑥 function is strictly decreasing on the reals greater than e. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴) ∧ 𝐴 < 𝐵) → ((log‘𝐵) / 𝐵) < ((log‘𝐴) / 𝐴))
Theorem	relogcld 15876	Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)
Theorem	reeflogd 15877	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴)
Theorem	relogmuld 15878	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.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (log‘(𝐴 · 𝐵)) = ((log‘𝐴) + (log‘𝐵)))
Theorem	relogdivd 15879	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.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (log‘(𝐴 / 𝐵)) = ((log‘𝐴) − (log‘𝐵)))
Theorem	logled 15880	Natural logarithm preserves ≤. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (log‘𝐴) ≤ (log‘𝐵)))
Theorem	relogefd 15881	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (log‘(exp‘𝐴)) = 𝐴)
Theorem	rplogcld 15882	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    ⇒   ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+)
Theorem	logge0d 15883	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ (log‘𝐴))
Theorem	logge0b 15884	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → (0 ≤ (log‘𝐴) ↔ 1 ≤ 𝐴))
Theorem	loggt0b 15885	The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
Theorem	logle1b 15886	The logarithm of a number is less than or equal to 1 iff the number is less than or equal to Euler's constant. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) ≤ 1 ↔ 𝐴 ≤ e))
Theorem	loglt1b 15887	The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
Theorem	rpcxpef 15888	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴))))
Theorem	cxpexprp 15889	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵))
Theorem	cxpexpnn 15890	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴↑𝑐𝐵) = (𝐴↑𝐵))
Theorem	logcxp 15891	Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	rpcxp0 15892	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
⊢ (𝐴 ∈ ℝ+ → (𝐴↑𝑐0) = 1)
Theorem	rpcxp1 15893	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝐴↑𝑐1) = 𝐴)
Theorem	1cxp 15894	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (1↑𝑐𝐴) = 1)
Theorem	ecxp 15895	Write the exponential function as an exponent to the power e. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (𝐴 ∈ ℂ → (e↑𝑐𝐴) = (exp‘𝐴))
Theorem	rpcncxpcl 15896	Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ)
Theorem	rpcxpcl 15897	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+)
Theorem	cxpap0 15898	Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) # 0)
Theorem	rpcxpadd 15899	Sum of exponents law for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 13-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 𝐶)) = ((𝐴↑𝑐𝐵) · (𝐴↑𝑐𝐶)))
Theorem	rpcxpp1 15900	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴))