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

Definition df-tanh 28459
Description: Define the hyperbolic tangent function (tanh). We define it this way for cmpt 4093, which requires the form  (
x  e.  A  |->  B ). (Contributed by David A. Wheeler, 10-May-2015.)
Assertion
Ref Expression
df-tanh  |- tanh  =  ( x  e.  ( `'cosh " ( CC  \  { 0 } ) )  |->  ( ( tan `  ( _i  x.  x
) )  /  _i ) )

Detailed syntax breakdown of Definition df-tanh
StepHypRef Expression
1 ctanh 28456 . 2  class tanh
2 vx . . 3  set  x
3 ccosh 28455 . . . . 5  class cosh
43ccnv 4704 . . . 4  class  `'cosh
5 cc 8751 . . . . 5  class  CC
6 cc0 8753 . . . . . 6  class  0
76csn 3653 . . . . 5  class  { 0 }
85, 7cdif 3162 . . . 4  class  ( CC 
\  { 0 } )
94, 8cima 4708 . . 3  class  ( `'cosh " ( CC  \  { 0 } ) )
10 ci 8755 . . . . . 6  class  _i
112cv 1631 . . . . . 6  class  x
12 cmul 8758 . . . . . 6  class  x.
1310, 11, 12co 5874 . . . . 5  class  ( _i  x.  x )
14 ctan 12363 . . . . 5  class  tan
1513, 14cfv 5271 . . . 4  class  ( tan `  ( _i  x.  x
) )
16 cdiv 9439 . . . 4  class  /
1715, 10, 16co 5874 . . 3  class  ( ( tan `  ( _i  x.  x ) )  /  _i )
182, 9, 17cmpt 4093 . 2  class  ( x  e.  ( `'cosh " ( CC  \  { 0 } ) )  |->  ( ( tan `  ( _i  x.  x ) )  /  _i ) )
191, 18wceq 1632 1  wff tanh  =  ( x  e.  ( `'cosh " ( CC  \  { 0 } ) )  |->  ( ( tan `  ( _i  x.  x
) )  /  _i ) )
Colors of variables: wff set class
This definition is referenced by:  tanhval-named  28462
  Copyright terms: Public domain W3C validator