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 =\left(x\in ℂ⟼\frac{\sin \mathrm{i}x}{\mathrm{i}}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csinh	$$class\sinh$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		csin	$$class\sin$$
4		ci	$$class\mathrm{i}$$
5		cmul	$$class\times$$
6	1	cv	$$setvarx$$
7	4 6 5	co	$$class\mathrm{i}x$$
8	7 3	cfv	$$class\sin \mathrm{i}x$$
9		cdiv	$$class÷$$
10	8 4 9	co	$$class\left(\frac{\sin \mathrm{i}x}{\mathrm{i}}\right)$$
11	1 2 10	cmpt	$$class\left(x\in ℂ⟼\frac{\sin \mathrm{i}x}{\mathrm{i}}\right)$$
12	0 11	wceq	$$wff\sinh =\left(x\in ℂ⟼\frac{\sin \mathrm{i}x}{\mathrm{i}}\right)$$