Definition df-sinh 51116

Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 5190, which requires the form (𝑥 ∈ 𝐴 ↦ 𝐵). See sinhval-named 51119 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 51121 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 51113	. 2 class sinh
2		vx	. . 3 setvar 𝑥
3		cc 11228	. . 3 class ℂ
4		ci 11232	. . . . . 6 class i
5	2	cv 1569	. . . . . 6 class 𝑥
6		cmul 11235	. . . . . 6 class ·
7	4, 5, 6	co 7446	. . . . 5 class (i · 𝑥)
8		csin 16261	. . . . 5 class sin
9	7, 8	cfv 6561	. . . 4 class (sin‘(i · 𝑥))
10		cdiv 12003	. . . 4 class /
11	9, 4, 10	co 7446	. . 3 class ((sin‘(i · 𝑥)) / i)
12	2, 3, 11	cmpt 5190	. 2 class (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))
13	1, 12	wceq 1570	1 wff sinh = (𝑥 ∈ ℂ ↦ ((sin‘(i · 𝑥)) / i))

This definition is used by:  sinhval-named  51119  sinhf  51123