![]() |
Metamath
Proof Explorer Theorem List (p. 161 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30848) |
![]() (30849-32371) |
![]() (32372-48589) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cfallfac 16001 | Declare the syntax for the falling factorial. |
class FallFac | ||
Syntax | crisefac 16002 | Declare the syntax for the rising factorial. |
class RiseFac | ||
Definition | df-risefac 16003* | 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 16004* | 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 16005* | The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) = ∏𝑘 ∈ (0...(𝑁 − 1))(𝐴 + 𝑘)) | ||
Theorem | fallfacval 16006* | The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) = ∏𝑘 ∈ (0...(𝑁 − 1))(𝐴 − 𝑘)) | ||
Theorem | risefacval2 16007* | One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) = ∏𝑘 ∈ (1...𝑁)(𝐴 + (𝑘 − 1))) | ||
Theorem | fallfacval2 16008* | One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) = ∏𝑘 ∈ (1...𝑁)(𝐴 − (𝑘 − 1))) | ||
Theorem | fallfacval3 16009* | A product representation of falling factorial when 𝐴 is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.) |
⊢ (𝑁 ∈ (0...𝐴) → (𝐴 FallFac 𝑁) = ∏𝑘 ∈ ((𝐴 − (𝑁 − 1))...𝐴)𝑘) | ||
Theorem | risefaccllem 16010* | Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ 𝑆 ⊆ ℂ & ⊢ 1 ∈ 𝑆 & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 · 𝑦) ∈ 𝑆) & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐴 + 𝑘) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ 𝑆) | ||
Theorem | fallfaccllem 16011* | Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ 𝑆 ⊆ ℂ & ⊢ 1 ∈ 𝑆 & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 · 𝑦) ∈ 𝑆) & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0) → (𝐴 − 𝑘) ∈ 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ 𝑆) | ||
Theorem | risefaccl 16012 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℂ) | ||
Theorem | fallfaccl 16013 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ ℂ) | ||
Theorem | rerisefaccl 16014 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℝ) | ||
Theorem | refallfaccl 16015 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ ℝ) | ||
Theorem | nnrisefaccl 16016 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℕ) | ||
Theorem | zrisefaccl 16017 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℤ) | ||
Theorem | zfallfaccl 16018 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac 𝑁) ∈ ℤ) | ||
Theorem | nn0risefaccl 16019 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℕ0) | ||
Theorem | rprisefaccl 16020 | Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac 𝑁) ∈ ℝ+) | ||
Theorem | risefallfac 16021 | A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝑋 RiseFac 𝑁) = ((-1↑𝑁) · (-𝑋 FallFac 𝑁))) | ||
Theorem | fallrisefac 16022 | A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.) |
⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝑋 FallFac 𝑁) = ((-1↑𝑁) · (-𝑋 RiseFac 𝑁))) | ||
Theorem | risefall0lem 16023 | Lemma for risefac0 16024 and fallfac0 16025. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (0...(0 − 1)) = ∅ | ||
Theorem | risefac0 16024 | The value of the rising factorial when 𝑁 = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (𝐴 ∈ ℂ → (𝐴 RiseFac 0) = 1) | ||
Theorem | fallfac0 16025 | The value of the falling factorial when 𝑁 = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 0) = 1) | ||
Theorem | risefacp1 16026 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 RiseFac (𝑁 + 1)) = ((𝐴 RiseFac 𝑁) · (𝐴 + 𝑁))) | ||
Theorem | fallfacp1 16027 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴 FallFac (𝑁 + 1)) = ((𝐴 FallFac 𝑁) · (𝐴 − 𝑁))) | ||
Theorem | risefacp1d 16028 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴 RiseFac (𝑁 + 1)) = ((𝐴 RiseFac 𝑁) · (𝐴 + 𝑁))) | ||
Theorem | fallfacp1d 16029 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴 FallFac (𝑁 + 1)) = ((𝐴 FallFac 𝑁) · (𝐴 − 𝑁))) | ||
Theorem | risefac1 16030 | The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (𝐴 ∈ ℂ → (𝐴 RiseFac 1) = 𝐴) | ||
Theorem | fallfac1 16031 | The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (𝐴 ∈ ℂ → (𝐴 FallFac 1) = 𝐴) | ||
Theorem | risefacfac 16032 | Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (𝑁 ∈ ℕ0 → (1 RiseFac 𝑁) = (!‘𝑁)) | ||
Theorem | fallfacfwd 16033 | The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (((𝐴 + 1) FallFac 𝑁) − (𝐴 FallFac 𝑁)) = (𝑁 · (𝐴 FallFac (𝑁 − 1)))) | ||
Theorem | 0fallfac 16034 | The value of the zero falling factorial at natural 𝑁. (Contributed by Scott Fenton, 17-Feb-2018.) |
⊢ (𝑁 ∈ ℕ → (0 FallFac 𝑁) = 0) | ||
Theorem | 0risefac 16035 | The value of the zero rising factorial at natural 𝑁. (Contributed by Scott Fenton, 17-Feb-2018.) |
⊢ (𝑁 ∈ ℕ → (0 RiseFac 𝑁) = 0) | ||
Theorem | binomfallfaclem1 16036 | Lemma for binomfallfac 16038. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁C𝐾) · ((𝐴 FallFac (𝑁 − 𝐾)) · (𝐵 FallFac (𝐾 + 1)))) ∈ ℂ) | ||
Theorem | binomfallfaclem2 16037* | Lemma for binomfallfac 16038. 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 16038* | 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 16039* | 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 16040 | Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.) |
⊢ (𝑁 ∈ (0...𝐴) → (𝐴 FallFac 𝑁) = ((!‘𝐴) / (!‘(𝐴 − 𝑁)))) | ||
Theorem | bcfallfac 16041 | Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((𝑁 FallFac 𝐾) / (!‘𝐾))) | ||
Theorem | fallfacfac 16042 | Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 FallFac 𝑁) = (!‘𝑁)) | ||
Syntax | cbp 16043 | Declare the constant for the Bernoulli polynomial operator. |
class BernPoly | ||
Definition | df-bpoly 16044* | 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 16045* | Lemma for bpolyval 16046. (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 16046* | The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) | ||
Theorem | bpoly0 16047 | The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1) | ||
Theorem | bpoly1 16048 | The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2))) | ||
Theorem | bpolycl 16049 | Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) ∈ ℂ) | ||
Theorem | bpolysum 16050* | 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 16051* | Lemma for bpolydif 16052. (Contributed by Scott Fenton, 12-Jun-2014.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ⇒ ⊢ (𝜑 → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1)))) | ||
Theorem | bpolydif 16052 | 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 16053* | 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 16054 | The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6))) | ||
Theorem | bpoly3 16055 | The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) | ||
Theorem | bpoly4 16056 | The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30))) | ||
Theorem | fsumcube 16057* | Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.) |
⊢ (𝑇 ∈ ℕ0 → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4)) | ||
Syntax | ce 16058 | Extend class notation to include the exponential function. |
class exp | ||
Syntax | ceu 16059 | Extend class notation to include Euler's constant e = 2.71828.... |
class e | ||
Syntax | csin 16060 | Extend class notation to include the sine function. |
class sin | ||
Syntax | ccos 16061 | Extend class notation to include the cosine function. |
class cos | ||
Syntax | ctan 16062 | Extend class notation to include the tangent function. |
class tan | ||
Syntax | cpi 16063 | Extend class notation to include the constant pi, π = 3.14159.... |
class π | ||
Definition | df-ef 16064* | Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 16076. (Contributed by NM, 14-Mar-2005.) |
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) | ||
Definition | df-e 16065 | Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.) |
⊢ e = (exp‘1) | ||
Definition | df-sin 16066 | Define the sine function. (Contributed by NM, 14-Mar-2005.) |
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))) | ||
Definition | df-cos 16067 | Define the cosine function. (Contributed by NM, 14-Mar-2005.) |
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)) | ||
Definition | df-tan 16068 | Define the tangent function. We define it this way for cmpt 5228, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥))) | ||
Definition | df-pi 16069 | 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 16070 | Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ) | ||
Theorem | reeftcl 16071 | 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 16072 | 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 16073* | 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 16074* | Lemma for efcl 16079. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15882 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 16075* | 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 16076* | Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘))) | ||
Theorem | esum 16077 | Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.) |
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘)) | ||
Theorem | eff 16078 | 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 16079 | Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ) | ||
Theorem | efcld 16080 | Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℂ) | ||
Theorem | efval2 16081* | Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘)) | ||
Theorem | efcvg 16082* | 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 16083* | 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 16084 | 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 16085 | The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ) | ||
Theorem | ere 16086 | 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 16087 | Lemma for egt2lt3 16203. (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 16088 | 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 16089 | 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 16090* | Lemma for efadd 16091 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) | ||
Theorem | efadd 16091 | 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 16092* | 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 16093 | Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1) | ||
Theorem | efne0 16094 | 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 16095 | The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.) |
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴))) | ||
Theorem | eff2 16096 | The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) |
⊢ exp:ℂ⟶(ℂ ∖ {0}) | ||
Theorem | efsub 16097 | Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) | ||
Theorem | efexp 16098 | 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 16099 | Value of the exponential function for integers. Special case of efval 16076. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁)) | ||
Theorem | efgt0 16100 | 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‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |