Definition df-sinh 42273

Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 4643, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). See sinhval-named 42276 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 metamath). See sinh-conventional 42279 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

Step	Hyp	Ref	Expression
1		csinh 42270	. 2 class sinh
2		vx	. . 3 setvar 𝑥
3		cc 9813	. . 3 class ℂ
4		ci 9817	. . . . . 6 class i
5	2	cv 1474	. . . . . 6 class 𝑥
6		cmul 9820	. . . . . 6 class ·
7	4, 5, 6	co 6549	. . . . 5 class (i · 𝑥)
8		csin 14633	. . . . 5 class sin
9	7, 8	cfv 5804	. . . 4 class (sin‘(i · 𝑥))
10		cdiv 10563	. . . 4 class /
11	9, 4, 10	co 6549	. . 3 class ((sin‘(i · 𝑥)) / i)
12	2, 3, 11	cmpt 4643	. 2 class (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
13	1, 12	wceq 1475	1 wff sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))

This definition is referenced by:  sinhval-named  42276