Home | Metamath
Proof Explorer Theorem List (p. 155 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bpoly4 15401 | The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.) |
⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30))) | ||
Theorem | fsumcube 15402* | Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.) |
⊢ (𝑇 ∈ ℕ0 → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4)) | ||
Syntax | ce 15403 | Extend class notation to include the exponential function. |
class exp | ||
Syntax | ceu 15404 | Extend class notation to include Euler's constant e = 2.71828.... |
class e | ||
Syntax | csin 15405 | Extend class notation to include the sine function. |
class sin | ||
Syntax | ccos 15406 | Extend class notation to include the cosine function. |
class cos | ||
Syntax | ctan 15407 | Extend class notation to include the tangent function. |
class tan | ||
Syntax | cpi 15408 | Extend class notation to include the constant pi, π = 3.14159.... |
class π | ||
Definition | df-ef 15409* | Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 15421. (Contributed by NM, 14-Mar-2005.) |
⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) | ||
Definition | df-e 15410 | Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.) |
⊢ e = (exp‘1) | ||
Definition | df-sin 15411 | Define the sine function. (Contributed by NM, 14-Mar-2005.) |
⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))) | ||
Definition | df-cos 15412 | Define the cosine function. (Contributed by NM, 14-Mar-2005.) |
⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)) | ||
Definition | df-tan 15413 | Define the tangent function. We define it this way for cmpt 5137, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥))) | ||
Definition | df-pi 15414 | 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 15415 | Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ) | ||
Theorem | reeftcl 15416 | 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 15417 | 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 15418* | 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 15419* | Lemma for efcl 15424. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15227 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 15420* | 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 15421* | Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘))) | ||
Theorem | esum 15422 | Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.) |
⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘)) | ||
Theorem | eff 15423 | 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 15424 | Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ) | ||
Theorem | efval2 15425* | Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘)) | ||
Theorem | efcvg 15426* | 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 15427* | 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 15428 | 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 15429 | The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ) | ||
Theorem | ere 15430 | 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 15431 | Lemma for egt2lt3 15547. (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 15432 | 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 15433 | 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 15434* | Lemma for efadd 15435 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) | ||
Theorem | efadd 15435 | 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 15436* | 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 15437 | Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1) | ||
Theorem | efne0 15438 | 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 15439 | The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.) |
⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴))) | ||
Theorem | eff2 15440 | The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) |
⊢ exp:ℂ⟶(ℂ ∖ {0}) | ||
Theorem | efsub 15441 | Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) | ||
Theorem | efexp 15442 | 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 15443 | Value of the exponential function for integers. Special case of efval 15421. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁)) | ||
Theorem | efgt0 15444 | 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 15445 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.) |
⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ+) | ||
Theorem | rpefcld 15446 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ+) | ||
Theorem | eftlcvg 15447* | The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | ||
Theorem | eftlcl 15448* | 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 15449* | 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 15450* | 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 15451* | 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 15452* | 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 15453 | 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 15454* | 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 15455 | 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 15456 | 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 15457 | 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 15458 | 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 15459 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵))) | ||
Theorem | reef11 15460 | 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 15461 | 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 15462 | 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 15463 | 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 15464 | 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 15465 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ sin:ℂ⟶ℂ | ||
Theorem | cosf 15466 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ cos:ℂ⟶ℂ | ||
Theorem | sincl 15467 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ) | ||
Theorem | coscl 15468 | 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 15469 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴))) | ||
Theorem | tancl 15470 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ) | ||
Theorem | sincld 15471 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ) | ||
Theorem | coscld 15472 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) | ||
Theorem | tancld 15473 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (cos‘𝐴) ≠ 0) ⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ) | ||
Theorem | tanval2 15474 | 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 15475 | 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 15476 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴)))) | ||
Theorem | recosval 15477 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴)))) | ||
Theorem | efi4p 15478* | 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 15479* | 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 15480* | 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 15481 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ) | ||
Theorem | recoscl 15482 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ) | ||
Theorem | retancl 15483 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℝ) | ||
Theorem | resincld 15484 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) | ||
Theorem | recoscld 15485 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ) | ||
Theorem | retancld 15486 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (cos‘𝐴) ≠ 0) ⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ) | ||
Theorem | sinneg 15487 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴)) | ||
Theorem | cosneg 15488 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴)) | ||
Theorem | tanneg 15489 | 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 15490 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
⊢ (sin‘0) = 0 | ||
Theorem | cos0 15491 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
⊢ (cos‘0) = 1 | ||
Theorem | tan0 15492 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
⊢ (tan‘0) = 0 | ||
Theorem | efival 15493 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) | ||
Theorem | efmival 15494 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴)))) | ||
Theorem | sinhval 15495 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → ((sin‘(i · 𝐴)) / i) = (((exp‘𝐴) − (exp‘-𝐴)) / 2)) | ||
Theorem | coshval 15496 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(i · 𝐴)) = (((exp‘𝐴) + (exp‘-𝐴)) / 2)) | ||
Theorem | resinhcl 15497 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → ((sin‘(i · 𝐴)) / i) ∈ ℝ) | ||
Theorem | rpcoshcl 15498 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ+) | ||
Theorem | recoshcl 15499 | The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ) | ||
Theorem | retanhcl 15500 | The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |