Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sinh Unicode version

Definition df-sinh 28203
Description: Define the hyperbolic sine function (sinh). We define it this way for cmpt 4077, which requires the form  (
x  e.  A  |->  B ). See sinhval-named 28206 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 28209 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
StepHypRef Expression
1 csinh 28200 . 2  class sinh
2 vx . . 3  set  x
3 cc 8735 . . 3  class  CC
4 ci 8739 . . . . . 6  class  _i
52cv 1622 . . . . . 6  class  x
6 cmul 8742 . . . . . 6  class  x.
74, 5, 6co 5858 . . . . 5  class  ( _i  x.  x )
8 csin 12345 . . . . 5  class  sin
97, 8cfv 5255 . . . 4  class  ( sin `  ( _i  x.  x
) )
10 cdiv 9423 . . . 4  class  /
119, 4, 10co 5858 . . 3  class  ( ( sin `  ( _i  x.  x ) )  /  _i )
122, 3, 11cmpt 4077 . 2  class  ( x  e.  CC  |->  ( ( sin `  ( _i  x.  x ) )  /  _i ) )
131, 12wceq 1623 1  wff sinh  =  ( x  e.  CC  |->  ( ( sin `  (
_i  x.  x )
)  /  _i ) )
Colors of variables: wff set class
This definition is referenced by:  sinhval-named  28206
  Copyright terms: Public domain W3C validator