|   | Mathbox for David A. Wheeler | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-sinh | Structured version Visualization version GIF version | ||
| Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 5225, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). See sinhval-named 49255 for a simple way to evaluate it. We define this function by dividing by i, which uses fewer operations than many conventional definitions (and thus is more convenient to use in set.mm). See sinh-conventional 49258 for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015.) | 
| Ref | Expression | 
|---|---|
| df-sinh | ⊢ sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | csinh 49249 | . 2 class sinh | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | cc 11153 | . . 3 class ℂ | |
| 4 | ci 11157 | . . . . . 6 class i | |
| 5 | 2 | cv 1539 | . . . . . 6 class 𝑥 | 
| 6 | cmul 11160 | . . . . . 6 class · | |
| 7 | 4, 5, 6 | co 7431 | . . . . 5 class (i · 𝑥) | 
| 8 | csin 16099 | . . . . 5 class sin | |
| 9 | 7, 8 | cfv 6561 | . . . 4 class (sin‘(i · 𝑥)) | 
| 10 | cdiv 11920 | . . . 4 class / | |
| 11 | 9, 4, 10 | co 7431 | . . 3 class ((sin‘(i · 𝑥)) / i) | 
| 12 | 2, 3, 11 | cmpt 5225 | . 2 class (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i)) | 
| 13 | 1, 12 | wceq 1540 | 1 wff sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i)) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: sinhval-named 49255 | 
| Copyright terms: Public domain | W3C validator |