| Metamath
Proof Explorer Theorem List (p. 162 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | ctan 16101 | Extend class notation to include the tangent function. |
| class tan | ||
| Syntax | cpi 16102 | Extend class notation to include the constant pi, π = 3.14159.... |
| class π | ||
| Definition | df-ef 16103* | Define the exponential function. Its value at the complex number 𝐴 is (exp‘𝐴) and is called the "exponential of 𝐴"; see efval 16115. (Contributed by NM, 14-Mar-2005.) |
| ⊢ exp = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ ℕ0 ((𝑥↑𝑘) / (!‘𝑘))) | ||
| Definition | df-e 16104 | Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.) |
| ⊢ e = (exp‘1) | ||
| Definition | df-sin 16105 | Define the sine function. (Contributed by NM, 14-Mar-2005.) |
| ⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))) | ||
| Definition | df-cos 16106 | Define the cosine function. (Contributed by NM, 14-Mar-2005.) |
| ⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)) | ||
| Definition | df-tan 16107 | Define the tangent function. We define it this way for cmpt 5225, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). (Contributed by Mario Carneiro, 14-Mar-2014.) |
| ⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥))) | ||
| Definition | df-pi 16108 | 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 16109 | Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℕ0) → ((𝐴↑𝐾) / (!‘𝐾)) ∈ ℂ) | ||
| Theorem | reeftcl 16110 | 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 16111 | 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 16112* | 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 16113* | Lemma for efcl 16118. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15919 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 16114* | 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 16115* | Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 ((𝐴↑𝑘) / (!‘𝑘))) | ||
| Theorem | esum 16116 | Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.) |
| ⊢ e = Σ𝑘 ∈ ℕ0 (1 / (!‘𝑘)) | ||
| Theorem | eff 16117 | 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 16118 | Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ) | ||
| Theorem | efcld 16119 | Closure law for the exponential function, deduction version. (Contributed by Thierry Arnoux, 1-Dec-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℂ) | ||
| Theorem | efval2 16120* | Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = Σ𝑘 ∈ ℕ0 (𝐹‘𝑘)) | ||
| Theorem | efcvg 16121* | 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 16122* | 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 16123 | 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 16124 | The exponential function is real if its argument is real. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ) | ||
| Theorem | ere 16125 | 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 16126 | Lemma for egt2lt3 16242. (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 16127 | 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 16128 | 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 16129* | Lemma for efadd 16130 (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ ((𝐵↑𝑛) / (!‘𝑛))) & ⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝐴 + 𝐵)↑𝑛) / (!‘𝑛))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘(𝐴 + 𝐵)) = ((exp‘𝐴) · (exp‘𝐵))) | ||
| Theorem | efadd 16130 | 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 16131* | 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 16132 | Cancellation law for exponential function. Equation 27 of [Rudin] p. 164. (Contributed by NM, 13-Jan-2006.) |
| ⊢ (𝐴 ∈ ℂ → ((exp‘𝐴) · (exp‘-𝐴)) = 1) | ||
| Theorem | efne0 16133 | 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 16134 | The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘-𝐴) = (1 / (exp‘𝐴))) | ||
| Theorem | eff2 16135 | The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) |
| ⊢ exp:ℂ⟶(ℂ ∖ {0}) | ||
| Theorem | efsub 16136 | Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) | ||
| Theorem | efexp 16137 | 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 16138 | Value of the exponential function for integers. Special case of efval 16115. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 15-Sep-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
| ⊢ (𝑁 ∈ ℤ → (exp‘𝑁) = (e↑𝑁)) | ||
| Theorem | efgt0 16139 | 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 16140 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 10-Nov-2013.) |
| ⊢ (𝐴 ∈ ℝ → (exp‘𝐴) ∈ ℝ+) | ||
| Theorem | rpefcld 16141 | The exponential of a real number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ∈ ℝ+) | ||
| Theorem | eftlcvg 16142* | The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014.) |
| ⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((𝐴↑𝑛) / (!‘𝑛))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0) → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | ||
| Theorem | eftlcl 16143* | 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 16144* | 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 16145* | 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 16146* | 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 16147* | 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 16148 | 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 16149* | 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 16150 | 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 16151 | 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 16152 | 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 16153 | 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 16154 | The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (exp‘𝐴) ≤ (exp‘𝐵))) | ||
| Theorem | reef11 16155 | 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 16156 | 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 16157 | 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 16158 | 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 16159 | 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 16160 | Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| ⊢ sin:ℂ⟶ℂ | ||
| Theorem | cosf 16161 | Domain and codomain of the cosine function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| ⊢ cos:ℂ⟶ℂ | ||
| Theorem | sincl 16162 | Closure of the sine function. (Contributed by NM, 28-Apr-2005.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ) | ||
| Theorem | coscl 16163 | 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 16164 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴))) | ||
| Theorem | tancl 16165 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℂ) | ||
| Theorem | sincld 16166 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℂ) | ||
| Theorem | coscld 16167 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℂ) | ||
| Theorem | tancld 16168 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (cos‘𝐴) ≠ 0) ⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℂ) | ||
| Theorem | tanval2 16169 | 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 16170 | 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 16171 | The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℝ → (sin‘𝐴) = (ℑ‘(exp‘(i · 𝐴)))) | ||
| Theorem | recosval 16172 | The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) = (ℜ‘(exp‘(i · 𝐴)))) | ||
| Theorem | efi4p 16173* | 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 16174* | 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 16175* | 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 16176 | The sine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℝ → (sin‘𝐴) ∈ ℝ) | ||
| Theorem | recoscl 16177 | The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℝ → (cos‘𝐴) ∈ ℝ) | ||
| Theorem | retancl 16178 | The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ ℝ) | ||
| Theorem | resincld 16179 | Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (sin‘𝐴) ∈ ℝ) | ||
| Theorem | recoscld 16180 | Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (cos‘𝐴) ∈ ℝ) | ||
| Theorem | retancld 16181 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → (cos‘𝐴) ≠ 0) ⇒ ⊢ (𝜑 → (tan‘𝐴) ∈ ℝ) | ||
| Theorem | sinneg 16182 | The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℂ → (sin‘-𝐴) = -(sin‘𝐴)) | ||
| Theorem | cosneg 16183 | The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘-𝐴) = (cos‘𝐴)) | ||
| Theorem | tanneg 16184 | 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 16185 | Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.) |
| ⊢ (sin‘0) = 0 | ||
| Theorem | cos0 16186 | Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (cos‘0) = 1 | ||
| Theorem | tan0 16187 | The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.) |
| ⊢ (tan‘0) = 0 | ||
| Theorem | efival 16188 | The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) | ||
| Theorem | efmival 16189 | The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) = ((cos‘𝐴) − (i · (sin‘𝐴)))) | ||
| Theorem | sinhval 16190 | Value of the hyperbolic sine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℂ → ((sin‘(i · 𝐴)) / i) = (((exp‘𝐴) − (exp‘-𝐴)) / 2)) | ||
| Theorem | coshval 16191 | Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℂ → (cos‘(i · 𝐴)) = (((exp‘𝐴) + (exp‘-𝐴)) / 2)) | ||
| Theorem | resinhcl 16192 | The hyperbolic sine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ → ((sin‘(i · 𝐴)) / i) ∈ ℝ) | ||
| Theorem | rpcoshcl 16193 | The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ+) | ||
| Theorem | recoshcl 16194 | The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ → (cos‘(i · 𝐴)) ∈ ℝ) | ||
| Theorem | retanhcl 16195 | The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ ℝ) | ||
| Theorem | tanhlt1 16196 | The hyperbolic tangent of a real number is upper bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) < 1) | ||
| Theorem | tanhbnd 16197 | The hyperbolic tangent of a real number is bounded by 1. (Contributed by Mario Carneiro, 4-Apr-2015.) |
| ⊢ (𝐴 ∈ ℝ → ((tan‘(i · 𝐴)) / i) ∈ (-1(,)1)) | ||
| Theorem | efeul 16198 | Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.) |
| ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) = ((exp‘(ℜ‘𝐴)) · ((cos‘(ℑ‘𝐴)) + (i · (sin‘(ℑ‘𝐴)))))) | ||
| Theorem | efieq 16199 | The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((exp‘(i · 𝐴)) = (exp‘(i · 𝐵)) ↔ ((cos‘𝐴) = (cos‘𝐵) ∧ (sin‘𝐴) = (sin‘𝐵)))) | ||
| Theorem | sinadd 16200 | Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |