Definition df-sinh

Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt , which requires the form ( x e. A |-> B ) . See sinhval-named 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 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)

	Ref	Expression
Assertion	df-sinh	⊢ sinh = ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ ( i · 𝑥 ) ) / i ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csinh	⊢ sinh
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		csin	⊢ sin
4		ci	⊢ i
5		cmul	⊢ ·
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( i · 𝑥 )
8	7 3	cfv	⊢ ( sin ‘ ( i · 𝑥 ) )
9		cdiv	⊢ /
10	8 4 9	co	⊢ ( ( sin ‘ ( i · 𝑥 ) ) / i )
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ ( i · 𝑥 ) ) / i ) )
12	0 11	wceq	⊢ sinh = ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ ( i · 𝑥 ) ) / i ) )