P. 161 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16001-16100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eftval 16001*	The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐹‘𝑁) = ((𝐴↑𝑁) / (!‘𝑁)))
Theorem	efcllem 16002*	Lemma for efcl 16007. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15808 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) (Proof shortened by AV, 9-Jul-2022.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )
Theorem	ef0lem 16003*	The series defining the exponential function converges in the (trivial) case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 = 0 → seq0( + , 𝐹) ⇝ 1)
Theorem	efval 16004*	Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘)))
Theorem	esum 16005	Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘))
Theorem	eff 16006	Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
⊢ exp:ℂ⟶ℂ
Theorem	efcl 16007	Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ)
Theorem	efcld 16008	Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℂ)
Theorem	efval2 16009*	Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘))
Theorem	efcvg 16010*	The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ⇝ (exp‘𝐴))
Theorem	efcvgfsum 16011*	Exponential function convergence in terms of a sequence of partial finite sums. (Contributed by NM, 10-Jan-2006.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ Σ𝑘 ∈ (0...𝑛)((𝐴↑𝑘) / (!‘𝑘)))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (exp‘𝐴))
Theorem	reefcl 16012	The exponential function is real if its argument is real. (Contributed by NM, 27-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ)
Theorem	reefcld 16013	The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ)
Theorem	ere 16014	Euler's constant e = 2.71828... is a real number. (Contributed by NM, 19-Mar-2005.) (Revised by Steve Rodriguez, 8-Mar-2006.)
⊢ e ∈ ℝ
Theorem	ege2le3 16015	Lemma for egt2lt3 16133. (Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))    ⇒   ⊢ (2 ≤ e ∧ e ≤ 3)
Theorem	ef0 16016	Value of the exponential function at 0. Equation 2 of [Gleason] p. 308. (Contributed by Steve Rodriguez, 27-Jun-2006.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ (exp‘0) = 1
Theorem	efcj 16017	The exponential of a complex conjugate. Equation 3 of [Gleason] p. 308. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (exp‘(∗‘𝐴)) = (∗‘(exp‘𝐴)))
Theorem	efaddlem 16018*	Lemma for efadd 16019 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Theorem	efadd 16019	Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Theorem	fprodefsum 16020*	Move the exponential function from inside a finite product to outside a finite sum. (Contributed by Scott Fenton, 26-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)(exp‘𝐴) = (exp‘Σ𝑘 ∈ (𝑀...𝑁)𝐴))
Theorem	efcan 16021	Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1)
Theorem	efne0d 16022	The exponential of a complex number is nonzero, deduction form. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 29-Apr-2014.) (Revised by SN, 25-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ≠ 0)
Theorem	efne0 16023	The exponential of a complex number is nonzero. Corollary 15-4.3 of [Gleason] p. 309. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 29-Apr-2014.) (Proof shortened by TA, 14-Nov-2025.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ≠ 0)
Theorem	efne0OLD 16024	Obsolete version of efne0 16023 as of 14-Nov-2025. The exponential of a complex number is nonzero. Corollary 15-4.3 of [Gleason] p. 309. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 29-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ≠ 0)
Theorem	efneg 16025	The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴)))
Theorem	eff2 16026	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
⊢ exp:ℂ⟶(ℂ ∖ {0})
Theorem	efsub 16027	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	efexp 16028	The exponential of an integer power. Corollary 15-4.4 of [Gleason] p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (exp‘(𝑁 · 𝐴)) = ((exp‘𝐴)↑𝑁))
Theorem	efzval 16029	Value of the exponential function for integers. Special case of efval 16004. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁))
Theorem	efgt0 16030	The exponential of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℝ → 0 < (exp‘𝐴))
Theorem	rpefcl 16031	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ+)
Theorem	rpefcld 16032	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ+)
Theorem	eftlcvg 16033*	The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	eftlcl 16034*	Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℂ)
Theorem	reeftlcl 16035*	Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘) ∈ ℝ)
Theorem	eftlub 16036*	An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ (((abs‘𝐴)↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ ((((abs‘𝐴)↑𝑀) / (!‘𝑀)) · ((1 / (𝑀 + 1))↑𝑛)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐴) ≤ 1)    ⇒   ⊢ (𝜑 → (abs‘Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘)) ≤ (((abs‘𝐴)↑𝑀) · ((𝑀 + 1) / ((!‘𝑀) · 𝑀))))
Theorem	efsep 16037*	Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (exp‘𝐴) = (𝐵 + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐹‘𝑘)))    &   ⊢ (𝜑 → (𝐵 + ((𝐴↑𝑀) / (!‘𝑀))) = 𝐷)    ⇒   ⊢ (𝜑 → (exp‘𝐴) = (𝐷 + Σ𝑘 ∈ (ℤ≥‘𝑁)(𝐹‘𝑘)))
Theorem	effsumlt 16038*	The partial sums of the series expansion of the exponential function at a positive real number are bounded by the value of the function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (seq0( + , 𝐹)‘𝑁) < (exp‘𝐴))
Theorem	eft0val 16039	The value of the first term of the series expansion of the exponential function is 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ (𝐴 ∈ ℂ → ((𝐴↑0) / (!‘0)) = 1)
Theorem	ef4p 16040*	Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = ((((1 + 𝐴) + ((𝐴↑2) / 2)) + ((𝐴↑3) / 6)) + Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)))
Theorem	efgt1p2 16041	The exponential of a positive real number is greater than the sum of the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → ((1 + 𝐴) + ((𝐴↑2) / 2)) < (exp‘𝐴))
Theorem	efgt1p 16042	The exponential of a positive real number is greater than 1 plus that number. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℝ+ → (1 + 𝐴) < (exp‘𝐴))
Theorem	efgt1 16043	The exponential of a positive real number is greater than 1. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℝ+ → 1 < (exp‘𝐴))
Theorem	eflt 16044	The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (exp‘𝐴) < (exp‘𝐵)))
Theorem	efle 16045	The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵)))
Theorem	reef11 16046	The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((exp‘𝐴) = (exp‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	reeff1 16047	The exponential function maps real arguments one-to-one to positive reals. (Contributed by Steve Rodriguez, 25-Aug-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (exp ↾ ℝ):ℝ–1-1→ℝ+
Theorem	eflegeo 16048	The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 < 1)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ≤ (1 / (1 − 𝐴)))
Theorem	sinval 16049	Value of the sine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)))
Theorem	cosval 16050	Value of the cosine function. (Contributed by NM, 14-Mar-2005.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2))
Theorem	sinf 16051	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ sin:ℂ⟶ℂ
Theorem	cosf 16052	Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ cos:ℂ⟶ℂ
Theorem	sincl 16053	Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
Theorem	coscl 16054	Closure of the cosine function with a complex argument. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
Theorem	tanval 16055	Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
Theorem	tancl 16056	The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
Theorem	sincld 16057	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ)
Theorem	coscld 16058	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)
Theorem	tancld 16059	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (cos‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ)
Theorem	tanval2 16060	Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i · ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))))))
Theorem	tanval3 16061	Express the tangent function directly in terms of exp. (Contributed by Mario Carneiro, 25-Feb-2015.)
⊢ ((𝐴 ∈ ℂ ∧ ((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (tan‘𝐴) = (((exp‘(2 · (i · 𝐴))) − 1) / (i · ((exp‘(2 · (i · 𝐴))) + 1))))
Theorem	resinval 16062	The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴))))
Theorem	recosval 16063	The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴))))
Theorem	efi4p 16064*	Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = (((1 − ((𝐴↑2) / 2)) + (i · (𝐴 − ((𝐴↑3) / 6)))) + Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘)))
Theorem	resin4p 16065*	Separate out the first four terms of the infinite series expansion of the sine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = ((𝐴 − ((𝐴↑3) / 6)) + (ℑ‘Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘))))
Theorem	recos4p 16066*	Separate out the first four terms of the infinite series expansion of the cosine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (((i · 𝐴)↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = ((1 − ((𝐴↑2) / 2)) + (ℜ‘Σ𝑘 ∈ (ℤ≥‘4)(𝐹‘𝑘))))
Theorem	resincl 16067	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ)
Theorem	recoscl 16068	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ)
Theorem	retancl 16069	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℝ)
Theorem	resincld 16070	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ)
Theorem	recoscld 16071	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ)
Theorem	retancld 16072	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (cos‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ)
Theorem	sinneg 16073	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
Theorem	cosneg 16074	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
Theorem	tanneg 16075	The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘-𝐴) = -(tan‘𝐴))
Theorem	sin0 16076	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
⊢ (sin‘0) = 0
Theorem	cos0 16077	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
⊢ (cos‘0) = 1
Theorem	tan0 16078	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
⊢ (tan‘0) = 0
Theorem	efival 16079	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
Theorem	efmival 16080	The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
Theorem	sinhval 16081	Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℂ → ((sin‘(i · 𝐴)) / i) = (((exp‘𝐴) − (exp‘-𝐴)) / 2))
Theorem	coshval 16082	Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (cos‘(i · 𝐴)) = (((exp‘𝐴) + (exp‘-𝐴)) / 2))
Theorem	resinhcl 16083	The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((sin‘(i · 𝐴)) / i) ∈ ℝ)
Theorem	rpcoshcl 16084	The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ+)
Theorem	recoshcl 16085	The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ)
Theorem	retanhcl 16086	The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ ℝ)
Theorem	tanhlt1 16087	The hyperbolic tangent of a real number is upper bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) < 1)
Theorem	tanhbnd 16088	The hyperbolic tangent of a real number is bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ (-1(,)1))
Theorem	efeul 16089	Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = ((exp‘(ℜ‘𝐴)) · ((cos‘(ℑ‘𝐴)) + (i · (sin‘(ℑ‘𝐴))))))
Theorem	efieq 16090	The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((exp‘(i · 𝐴)) = (exp‘(i · 𝐵)) ↔ ((cos‘𝐴) = (cos‘𝐵) ∧ (sin‘𝐴) = (sin‘𝐵))))
Theorem	sinadd 16091	Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵))))
Theorem	cosadd 16092	Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵))))
Theorem	tanaddlem 16093	A useful intermediate step in tanadd 16094 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) ≠ 0 ∧ (cos‘𝐵) ≠ 0)) → ((cos‘(𝐴 + 𝐵)) ≠ 0 ↔ ((tan‘𝐴) · (tan‘𝐵)) ≠ 1))
Theorem	tanadd 16094	Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((cos‘𝐴) ≠ 0 ∧ (cos‘𝐵) ≠ 0 ∧ (cos‘(𝐴 + 𝐵)) ≠ 0)) → (tan‘(𝐴 + 𝐵)) = (((tan‘𝐴) + (tan‘𝐵)) / (1 − ((tan‘𝐴) · (tan‘𝐵)))))
Theorem	sinsub 16095	Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 − 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) − ((cos‘𝐴) · (sin‘𝐵))))
Theorem	cossub 16096	Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (cos‘(𝐴 − 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) + ((sin‘𝐴) · (sin‘𝐵))))
Theorem	addsin 16097	Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) + (sin‘𝐵)) = (2 · ((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2)))))
Theorem	subsin 16098	Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) − (sin‘𝐵)) = (2 · ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2)))))
Theorem	sinmul 16099	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 16092 and cossub 16096. (Contributed by David A. Wheeler, 26-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((sin‘𝐴) · (sin‘𝐵)) = (((cos‘(𝐴 − 𝐵)) − (cos‘(𝐴 + 𝐵))) / 2))
Theorem	cosmul 16100	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 16092 and cossub 16096. (Contributed by David A. Wheeler, 26-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((cos‘𝐴) · (cos‘𝐵)) = (((cos‘(𝐴 − 𝐵)) + (cos‘(𝐴 + 𝐵))) / 2))