Definition df-sinh 42474

Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 4729, which requires the form ( x e. A |-> B ). 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 = ( x e. CC |-> ( ( sin ` ( _i x. x ) ) / _i ) )

Detailed syntax breakdown of Definition df-sinh

Step	Hyp	Ref	Expression
1		csinh 42471	. 2 class sinh
2		vx	. . 3 setvar x
3		cc 9934	. . 3 class CC
4		ci 9938	. . . . . 6 class _i
5	2	cv 1482	. . . . . 6 class x
6		cmul 9941	. . . . . 6 class x.
7	4, 5, 6	co 6650	. . . . 5 class ( _i x. x )
8		csin 14794	. . . . 5 class sin
9	7, 8	cfv 5888	. . . 4 class ( sin ` ( _i x. x ) )
10		cdiv 10684	. . . 4 class /
11	9, 4, 10	co 6650	. . 3 class ( ( sin ` ( _i x. x ) ) / _i )
12	2, 3, 11	cmpt 4729	. 2 class ( x e. CC |-> ( ( sin ` ( _i x. x ) ) / _i ) )
13	1, 12	wceq 1483	1 wff sinh = ( x e. CC |-> ( ( sin ` ( _i x. x ) ) / _i ) )

This definition is referenced by:  sinhval-named  42477