P. 147 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	risefacp1d 14601	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 RiseFac (𝑁 + 1)) = ((𝐴 RiseFac 𝑁) · (𝐴 + 𝑁)))
Theorem	fallfacp1d 14602	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 FallFac (𝑁 + 1)) = ((𝐴 FallFac 𝑁) · (𝐴 − 𝑁)))
Theorem	risefac1 14603	The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝐴 ∈ ℂ → (𝐴 RiseFac 1) = 𝐴)
Theorem	fallfac1 14604	The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 1) = 𝐴)
Theorem	risefacfac 14605	Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝑁 ∈ ℕ0 → (1 RiseFac 𝑁) = (!‘𝑁))
Theorem	fallfacfwd 14606	The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (((𝐴 + 1) FallFac 𝑁) − (𝐴 FallFac 𝑁)) = (𝑁 · (𝐴 FallFac (𝑁 − 1))))
Theorem	0fallfac 14607	The value of the zero falling factorial at natural 𝑁. (Contributed by Scott Fenton, 17-Feb-2018.)
⊢ (𝑁 ∈ ℕ → (0 FallFac 𝑁) = 0)
Theorem	0risefac 14608	The value of the zero rising factorial at natural 𝑁. (Contributed by Scott Fenton, 17-Feb-2018.)
⊢ (𝑁 ∈ ℕ → (0 RiseFac 𝑁) = 0)
Theorem	binomfallfaclem1 14609	Lemma for binomfallfac 14611. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁C𝐾) · ((𝐴 FallFac (𝑁 − 𝐾)) · (𝐵 FallFac (𝐾 + 1)))) ∈ ℂ)
Theorem	binomfallfaclem2 14610*	Lemma for binomfallfac 14611. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜓 → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵) FallFac (𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴 FallFac ((𝑁 + 1) − 𝑘)) · (𝐵 FallFac 𝑘))))
Theorem	binomfallfac 14611*	A version of the binomial theorem using falling factorials instead of exponentials. (Contributed by Scott Fenton, 13-Mar-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵) FallFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 FallFac (𝑁 − 𝑘)) · (𝐵 FallFac 𝑘))))
Theorem	binomrisefac 14612*	A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 + 𝐵) RiseFac 𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴 RiseFac (𝑁 − 𝑘)) · (𝐵 RiseFac 𝑘))))
Theorem	fallfacval4 14613	Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.)
⊢ (𝑁 ∈ (0...𝐴) → (𝐴 FallFac 𝑁) = ((!‘𝐴) / (!‘(𝐴 − 𝑁))))
Theorem	bcfallfac 14614	Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.)
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((𝑁 FallFac 𝐾) / (!‘𝐾)))
Theorem	fallfacfac 14615	Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 FallFac 𝑁) = (!‘𝑁))
5.10.14  Bernoulli polynomials and sums of k-th powers
Syntax	cbp 14616	Declare the constant for the Bernoulli polynomial operator.
class BernPoly
Definition	df-bpoly 14617*	Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulae do exist. (Contributed by Scott Fenton, 22-May-2014.)
⊢ BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
Theorem	bpolylem 14618*	Lemma for bpolyval 14619. (Contributed by Scott Fenton, 22-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐺 = (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))    &   ⊢ 𝐹 = wrecs( < , ℕ0, 𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
Theorem	bpolyval 14619*	The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
Theorem	bpoly0 14620	The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
Theorem	bpoly1 14621	The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
Theorem	bpolycl 14622	Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) ∈ ℂ)
Theorem	bpolysum 14623*	A sum for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = (𝑋↑𝑁))
Theorem	bpolydiflem 14624*	Lemma for bpolydif 14625. (Contributed by Scott Fenton, 12-Jun-2014.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1))))    ⇒   ⊢ (𝜑 → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))
Theorem	bpolydif 14625	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 14626*	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 14627	The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
Theorem	bpoly3 14628	The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
Theorem	bpoly4 14629	The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30)))
Theorem	fsumcube 14630*	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 14631	Extend class notation to include the exponential function.
class exp
Syntax	ceu 14632	Extend class notation to include Euler's constant = 2.7182818....
class e
Syntax	csin 14633	Extend class notation to include the sine function.
class sin
Syntax	ccos 14634	Extend class notation to include the cosine function.
class cos
Syntax	ctan 14635	Extend class notation to include the tangent function.
class tan
Syntax	cpi 14636	Extend class notation to include pi = 3.14159....
class π
Definition	df-ef 14637*	Define the exponential function. (Contributed by NM, 14-Mar-2005.)
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘)))
Definition	df-e 14638	Define Euler's constant 2.71828.... (Contributed by NM, 14-Mar-2005.)
⊢ e = (exp‘1)
Definition	df-sin 14639	Define the sine function. (Contributed by NM, 14-Mar-2005.)
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
Definition	df-cos 14640	Define the cosine function. (Contributed by NM, 14-Mar-2005.)
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
Definition	df-tan 14641	Define the tangent function. We define it this way for cmpt 4643, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
Definition	df-pi 14642	Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.)
⊢ π = inf((ℝ+ ∩ (◡sin “ {0})), ℝ, < )
Theorem	eftcl 14643	Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ)
Theorem	reeftcl 14644	The terms of the series expansion of the exponential function of a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℝ)
Theorem	eftabs 14645	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 14646*	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 14647*	Lemma for efcl 14652. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 14454 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → seq0( + , 𝐹) ∈ dom ⇝ )
Theorem	ef0lem 14648*	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 14649*	Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘)))
Theorem	esum 14650	Value of Euler's constant e = 2.71828... (Contributed by Steve Rodriguez, 5-Mar-2006.)
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘))
Theorem	eff 14651	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 14652	Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ)
Theorem	efval2 14653*	Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘))
Theorem	efcvg 14654*	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 14655*	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 14656	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 14657	The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ)
Theorem	ere 14658	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 14659	Lemma for egt2lt3 14773. (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 14660	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 14661	Exponential function 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 14662*	Lemma for efadd 14663 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Theorem	efadd 14663	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 14664*	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 14665	Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1)
Theorem	efne0 14666	The exponential function never vanishes. 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 14667	Exponent of a negative number. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴)))
Theorem	eff2 14668	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
⊢ exp:ℂ⟶(ℂ ∖ {0})
Theorem	efsub 14669	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	efexp 14670	Exponential function to 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 14671	Value of the exponential function for integers. Special case of efval 14649. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁))
Theorem	efgt0 14672	The exponential function 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 14673	The exponential function of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ+)
Theorem	rpefcld 14674	The exponential function of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ+)
Theorem	eftlcvg 14675*	The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Theorem	eftlcl 14676*	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 14677*	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 14678*	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 14679*	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 14680*	The partial sums of the series expansion of the exponential function of 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 14681	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 14682*	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 14683	The exponential function of a positive real number is greater than the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → ((1 + 𝐴) + ((𝐴↑2) / 2)) < (exp‘𝐴))
Theorem	efgt1p 14684	The exponential function 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 14685	The exponential function 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 14686	The exponential function on the reals is strictly monotonic. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (exp‘𝐴) < (exp‘𝐵)))
Theorem	efle 14687	The exponential function on the reals is strictly monotonic. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵)))
Theorem	reef11 14688	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 14689	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 14690	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 14691	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 14692	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 14693	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ sin:ℂ⟶ℂ
Theorem	cosf 14694	Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ cos:ℂ⟶ℂ
Theorem	sincl 14695	Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
Theorem	coscl 14696	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 14697	Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
Theorem	tancl 14698	The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ)
Theorem	sincld 14699	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ)
Theorem	coscld 14700	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ)