P. 156 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15501-15600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bpolydif 15501	Calculate the difference between successive values of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 26-May-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℂ) → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))
Theorem	fsumkthpow 15502*	A closed-form expression for the sum of 𝐾-th powers. (Contributed by Scott Fenton, 16-May-2014.) This is Metamath 100 proof #77. (Revised by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾) = ((((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0)) / (𝐾 + 1)))
Theorem	bpoly2 15503	The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
Theorem	bpoly3 15504	The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
Theorem	bpoly4 15505	The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30)))
Theorem	fsumcube 15506*	Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.)
⊢ (𝑇 ∈ ℕ0 → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
5.11  Elementary trigonometry
5.11.1  The exponential, sine, and cosine functions
Syntax	ce 15507	Extend class notation to include the exponential function.
class exp
Syntax	ceu 15508	Extend class notation to include Euler's constant e = 2.71828....
class e
Syntax	csin 15509	Extend class notation to include the sine function.
class sin
Syntax	ccos 15510	Extend class notation to include the cosine function.
class cos
Syntax	ctan 15511	Extend class notation to include the tangent function.
class tan
Syntax	cpi 15512	Extend class notation to include the constant pi, π = 3.14159....
class π
Definition	df-ef 15513*	Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 15525. (Contributed by NM, 14-Mar-2005.)
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘)))
Definition	df-e 15514	Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.)
⊢ e = (exp‘1)
Definition	df-sin 15515	Define the sine function. (Contributed by NM, 14-Mar-2005.)
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
Definition	df-cos 15516	Define the cosine function. (Contributed by NM, 14-Mar-2005.)
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
Definition	df-tan 15517	Define the tangent function. We define it this way for cmpt 5110, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
Definition	df-pi 15518	Define the constant pi, π = 3.14159..., which is the smallest positive number whose sine is zero. Definition of π in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.)
⊢ π = inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < )
Theorem	eftcl 15519	Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ)
Theorem	reeftcl 15520	The terms of the series expansion of the exponential function at a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℝ)
Theorem	eftabs 15521	The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → (abs‘((𝐴↑𝐾) / (!‘𝐾))) = (((abs‘𝐴)↑𝐾) / (!‘𝐾)))
Theorem	eftval 15522*	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 15523*	Lemma for efcl 15528. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15331 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 15524*	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 15525*	Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘)))
Theorem	esum 15526	Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘))
Theorem	eff 15527	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 15528	Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ)
Theorem	efval2 15529*	Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘))
Theorem	efcvg 15530*	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 15531*	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 15532	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 15533	The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ)
Theorem	ere 15534	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 15535	Lemma for egt2lt3 15651. (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 15536	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 15537	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 15538*	Lemma for efadd 15539 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Theorem	efadd 15539	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 15540*	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 15541	Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1)
Theorem	efne0 15542	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.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ≠ 0)
Theorem	efneg 15543	The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴)))
Theorem	eff2 15544	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
⊢ exp:ℂ⟶(ℂ ∖ {0})
Theorem	efsub 15545	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	efexp 15546	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 15547	Value of the exponential function for integers. Special case of efval 15525. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁))
Theorem	efgt0 15548	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 15549	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ+)
Theorem	rpefcld 15550	The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ+)
Theorem	eftlcvg 15551*	The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	eftlcl 15552*	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 15553*	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 15554*	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 15555*	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 15556*	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 15557	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 15558*	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 15559	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 15560	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 15561	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 15562	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 15563	The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵)))
Theorem	reef11 15564	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 15565	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 15566	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 15567	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 15568	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 15569	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ sin:ℂ⟶ℂ
Theorem	cosf 15570	Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ cos:ℂ⟶ℂ
Theorem	sincl 15571	Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
Theorem	coscl 15572	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 15573	Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
Theorem	tancl 15574	The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
Theorem	sincld 15575	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ)
Theorem	coscld 15576	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)
Theorem	tancld 15577	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (cos‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ)
Theorem	tanval2 15578	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 15579	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 15580	The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴))))
Theorem	recosval 15581	The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴))))
Theorem	efi4p 15582*	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 15583*	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 15584*	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 15585	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ)
Theorem	recoscl 15586	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ)
Theorem	retancl 15587	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℝ)
Theorem	resincld 15588	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ)
Theorem	recoscld 15589	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ)
Theorem	retancld 15590	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (cos‘𝐴) ≠ 0)    ⇒   ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ)
Theorem	sinneg 15591	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴))
Theorem	cosneg 15592	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴))
Theorem	tanneg 15593	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 15594	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
⊢ (sin‘0) = 0
Theorem	cos0 15595	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
⊢ (cos‘0) = 1
Theorem	tan0 15596	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
⊢ (tan‘0) = 0
Theorem	efival 15597	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴))))
Theorem	efmival 15598	The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴))))
Theorem	sinhval 15599	Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℂ → ((sin‘(i · 𝐴)) / i) = (((exp‘𝐴) − (exp‘-𝐴)) / 2))
Theorem	coshval 15600	Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (cos‘(i · 𝐴)) = (((exp‘𝐴) + (exp‘-𝐴)) / 2))