Definition df-cosh

Description: Define the hyperbolic cosine function (cosh). We define it this way for cmpt , which requires the form ( x e. A |-> B ) . (Contributed by David A. Wheeler, 10-May-2015)

	Ref	Expression
Assertion	df-cosh	|- cosh = ( x e. CC |-> ( cos ` ( _i x. x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccosh	|- cosh
1		vx	|- x
2		cc	|- CC
3		ccos	|- cos
4		ci	|- _i
5		cmul	|- x.
6	1	cv	|- x
7	4 6 5	co	|- ( _i x. x )
8	7 3	cfv	|- ( cos ` ( _i x. x ) )
9	1 2 8	cmpt	|- ( x e. CC |-> ( cos ` ( _i x. x ) ) )
10	0 9	wceq	|- cosh = ( x e. CC |-> ( cos ` ( _i x. x ) ) )