Home | Metamath
Proof Explorer Theorem List (p. 147 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
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 𝑁) = (!‘𝑁)) | ||
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)) | ||
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‘𝐴) ∈ ℂ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |