P. 163 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	crisefac 16201	Declare the syntax for the rising factorial.
class RiseFac
Definition	df-risefac 16202*	Define the rising factorial function. This is the function (𝐴 · (𝐴 + 1) · ...(𝐴 + 𝑁)) for complex 𝐴 and nonnegative integers 𝑁. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ RiseFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 + 𝑘))
Definition	df-fallfac 16203*	Define the falling factorial function. This is the function (𝐴 · (𝐴 − 1) · ...(𝐴 − 𝑁)) for complex 𝐴 and nonnegative integers 𝑁. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ FallFac = (𝑥 ∈ ℂ, 𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (0...(𝑛 − 1))(𝑥 − 𝑘))
Theorem	risefacval 16204*	The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) = ∏𝑘 ∈ (0...(𝑁 − 1))(𝐴 + 𝑘))
Theorem	fallfacval 16205*	The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) = ∏𝑘 ∈ (0...(𝑁 − 1))(𝐴 − 𝑘))
Theorem	risefacval2 16206*	One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) = ∏𝑘 ∈ (1...𝑁)(𝐴 + (𝑘 − 1)))
Theorem	fallfacval2 16207*	One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) = ∏𝑘 ∈ (1...𝑁)(𝐴 − (𝑘 − 1)))
Theorem	fallfacval3 16208*	A product representation of falling factorial when 𝐴 is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.)
⊢ (𝑁 ∈ (0...𝐴) → (𝐴 FallFac 𝑁) = ∏𝑘 ∈ ((𝐴 − (𝑁 − 1))...𝐴)𝑘)
Theorem	risefaccllem 16209*	Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑆 ⊆ ℂ    &   ⊢ 1 ∈ 𝑆    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐴 + 𝑘) ∈ 𝑆)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ 𝑆)
Theorem	fallfaccllem 16210*	Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑆 ⊆ ℂ    &   ⊢ 1 ∈ 𝑆    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 · 𝑦) ∈ 𝑆)    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐴 − 𝑘) ∈ 𝑆)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ 𝑆)
Theorem	risefaccl 16211	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℂ)
Theorem	fallfaccl 16212	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ ℂ)
Theorem	rerisefaccl 16213	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℝ)
Theorem	refallfaccl 16214	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ ℝ)
Theorem	nnrisefaccl 16215	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℕ)
Theorem	zrisefaccl 16216	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℤ)
Theorem	zfallfaccl 16217	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ ℤ)
Theorem	nn0risefaccl 16218	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℕ0)
Theorem	rprisefaccl 16219	Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℝ+)
Theorem	risefallfac 16220	A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝑋 RiseFac 𝑁) = (( -1↑𝑁) · ( -𝑋 FallFac 𝑁)))
Theorem	fallrisefac 16221	A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.)
⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝑋 FallFac 𝑁) = (( -1↑𝑁) · ( -𝑋 RiseFac 𝑁)))
Theorem	risefac0 16222	The value of the rising factorial when 𝑁 = 0. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝐴 ∈ ℂ → (𝐴 RiseFac 0) = 1)
Theorem	fallfac0 16223	The value of the falling factorial when 𝑁 = 0. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 0) = 1)
Theorem	risefacp1 16224	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac (𝑁 + 1)) = ((𝐴 RiseFac 𝑁) · (𝐴 + 𝑁)))
Theorem	fallfacp1 16225	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac (𝑁 + 1)) = ((𝐴 FallFac 𝑁) · (𝐴 − 𝑁)))
Theorem	risefacp1d 16226	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 RiseFac (𝑁 + 1)) = ((𝐴 RiseFac 𝑁) · (𝐴 + 𝑁)))
Theorem	fallfacp1d 16227	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 FallFac (𝑁 + 1)) = ((𝐴 FallFac 𝑁) · (𝐴 − 𝑁)))
Theorem	risefac1 16228	The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝐴 ∈ ℂ → (𝐴 RiseFac 1) = 𝐴)
Theorem	fallfac1 16229	The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 1) = 𝐴)
Theorem	risefacfac 16230	Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ (𝑁 ∈ ℕ0 → (1 RiseFac 𝑁) = (!‘𝑁))
Theorem	fallfacfwd 16231	The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (((𝐴 + 1) FallFac 𝑁) − (𝐴 FallFac 𝑁)) = (𝑁 · (𝐴 FallFac (𝑁 − 1))))
Theorem	0fallfac 16232	The value of the zero falling factorial at natural 𝑁. (Contributed by Scott Fenton, 17-Feb-2018.)
⊢ (𝑁 ∈ ℕ → (0 FallFac 𝑁) = 0)
Theorem	0risefac 16233	The value of the zero rising factorial at natural 𝑁. (Contributed by Scott Fenton, 17-Feb-2018.)
⊢ (𝑁 ∈ ℕ → (0 RiseFac 𝑁) = 0)
Theorem	binomfallfaclem1 16234	Lemma for binomfallfac 16236. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁C𝐾) · ((𝐴 FallFac (𝑁 − 𝐾)) · (𝐵 FallFac (𝐾 + 1)))) ∈ ℂ)
Theorem	binomfallfaclem2 16235*	Lemma for binomfallfac 16236. 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 16236*	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 16237*	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 16238	Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.)
⊢ (𝑁 ∈ (0...𝐴) → (𝐴 FallFac 𝑁) = ((!‘𝐴) / (!‘(𝐴 − 𝑁))))
Theorem	bcfallfac 16239	Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.)
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((𝑁 FallFac 𝐾) / (!‘𝐾)))
Theorem	fallfacfac 16240	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 16241	Declare the constant for the Bernoulli polynomial operator.
class BernPoly
Definition	df-bpoly 16242*	Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulas do exist. (Contributed by Scott Fenton, 22-May-2014.)
⊢ BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
Theorem	bpolylem 16243*	Lemma for bpolyval 16244. (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 16244*	The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
Theorem	bpoly0 16245	The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
Theorem	bpoly1 16246	The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
Theorem	bpolycl 16247	Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) ∈ ℂ)
Theorem	bpolysum 16248*	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 16249*	Lemma for bpolydif 16250. (Contributed by Scott Fenton, 12-Jun-2014.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1))))    ⇒   ⊢ (𝜑 → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))
Theorem	bpolydif 16250	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 16251*	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 16252	The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
Theorem	bpoly3 16253	The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
Theorem	bpoly4 16254	The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30)))
Theorem	fsumcube 16255*	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 16256	Extend class notation to include the exponential function.
class exp
Syntax	ceu 16257	Extend class notation to include Euler's constant e = 2.71828....
class e
Syntax	csin 16258	Extend class notation to include the sine function.
class sin
Syntax	ccos 16259	Extend class notation to include the cosine function.
class cos
Syntax	ctan 16260	Extend class notation to include the tangent function.
class tan
Syntax	cpi 16261	Extend class notation to include the constant pi, π = 3.14159....
class π
Definition	df-ef 16262*	Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 16274. (Contributed by NM, 14-Mar-2005.)
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘)))
Definition	df-e 16263	Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.)
⊢ e = (exp‘1)
Definition	df-sin 16264	Define the sine function. (Contributed by NM, 14-Mar-2005.)
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i)))
Definition	df-cos 16265	Define the cosine function. (Contributed by NM, 14-Mar-2005.)
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) / 2))
Definition	df-tan 16266	Define the tangent function. We define it this way for cmpt 5189, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
Definition	df-pi 16267	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 16268	Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ)
Theorem	reeftcl 16269	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 16270	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 16271*	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 16272*	Lemma for efcl 16277. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 16081 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 16273*	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 16274*	Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘)))
Theorem	esum 16275	Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.)
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘))
Theorem	eff 16276	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 16277	Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.)
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ)
Theorem	efcld 16278	Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℂ)
Theorem	efval2 16279*	Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    ⇒   ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘))
Theorem	efcvg 16280*	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 16281*	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 16282	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 16283	The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ)
Theorem	ere 16284	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 16285	Lemma for egt2lt3 16403. (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 16286	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 16287	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 16288*	Lemma for efadd 16289 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛)))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵)))
Theorem	efadd 16289	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 16290*	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 16291	Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘ -𝐴)) = 1)
Theorem	efne0d 16292	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 16293	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 16294	Obsolete version of efne0 16293 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 16295	The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.)
⊢ (𝐴 ∈ ℂ → (exp‘ -𝐴) = (1 / (exp‘𝐴)))
Theorem	eff2 16296	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
⊢ exp:ℂ⟶(ℂ ∖ {0})
Theorem	efsub 16297	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵)))
Theorem	efexp 16298	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 16299	Value of the exponential function for integers. Special case of efval 16274. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁))
Theorem	efgt0 16300	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‘𝐴))