Definition df-sinh 42474

Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 4729, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). See sinhval-named 42477 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 42480 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 42471	. 2 class sinh
2		vx	. . 3 setvar 𝑥
3		cc 9934	. . 3 class ℂ
4		ci 9938	. . . . . 6 class i
5	2	cv 1482	. . . . . 6 class 𝑥
6		cmul 9941	. . . . . 6 class ·
7	4, 5, 6	co 6650	. . . . 5 class (i · 𝑥)
8		csin 14794	. . . . 5 class sin
9	7, 8	cfv 5888	. . . 4 class (sin‘(i · 𝑥))
10		cdiv 10684	. . . 4 class /
11	9, 4, 10	co 6650	. . 3 class ((sin‘(i · 𝑥)) / i)
12	2, 3, 11	cmpt 4729	. 2 class (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
13	1, 12	wceq 1483	1 wff sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))

This definition is referenced by:  sinhval-named  42477