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 45300
 Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 5111, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). See sinhval-named 45303 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 45306 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 45297 . 2 class sinh
2 vx . . 3 setvar 𝑥
3 cc 10527 . . 3 class
4 ci 10531 . . . . . 6 class i
52cv 1537 . . . . . 6 class 𝑥
6 cmul 10534 . . . . . 6 class ·
74, 5, 6co 7136 . . . . 5 class (i · 𝑥)
8 csin 15412 . . . . 5 class sin
97, 8cfv 6325 . . . 4 class (sin‘(i · 𝑥))
10 cdiv 11289 . . . 4 class /
119, 4, 10co 7136 . . 3 class ((sin‘(i · 𝑥)) / i)
122, 3, 11cmpt 5111 . 2 class (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
131, 12wceq 1538 1 wff sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
 Colors of variables: wff setvar class This definition is referenced by:  sinhval-named  45303
 Copyright terms: Public domain W3C validator