Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sinh Structured version   Visualization version   GIF version

Definition df-sinh 48964
Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 5231, which requires the form (𝑥𝐴𝐵). See sinhval-named 48967 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 48970 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.)
Assertion
Ref Expression
df-sinh sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))

Detailed syntax breakdown of Definition df-sinh
StepHypRef Expression
1 csinh 48961 . 2 class sinh
2 vx . . 3 setvar 𝑥
3 cc 11151 . . 3 class
4 ci 11155 . . . . . 6 class i
52cv 1536 . . . . . 6 class 𝑥
6 cmul 11158 . . . . . 6 class ·
74, 5, 6co 7431 . . . . 5 class (i · 𝑥)
8 csin 16096 . . . . 5 class sin
97, 8cfv 6563 . . . 4 class (sin‘(i · 𝑥))
10 cdiv 11918 . . . 4 class /
119, 4, 10co 7431 . . 3 class ((sin‘(i · 𝑥)) / i)
122, 3, 11cmpt 5231 . 2 class (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
131, 12wceq 1537 1 wff sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
Colors of variables: wff setvar class
This definition is referenced by:  sinhval-named  48967
  Copyright terms: Public domain W3C validator