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 27567
Description: Define the hyperbolic tangent function (tanh). We define it this way for cmpt 4077, 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 27564 . 2  class tanh
2 vx . . 3  set  x
3 ccosh 27563 . . . . 5  class cosh
43ccnv 4688 . . . 4  class  `'cosh
5 cc 8735 . . . . 5  class  CC
6 cc0 8737 . . . . . 6  class  0
76csn 3640 . . . . 5  class  { 0 }
85, 7cdif 3149 . . . 4  class  ( CC 
\  { 0 } )
94, 8cima 4692 . . 3  class  ( `'cosh " ( CC  \  { 0 } ) )
10 ci 8739 . . . . . 6  class  _i
112cv 1622 . . . . . 6  class  x
12 cmul 8742 . . . . . 6  class  x.
1310, 11, 12co 5858 . . . . 5  class  ( _i  x.  x )
14 ctan 12347 . . . . 5  class  tan
1513, 14cfv 5255 . . . 4  class  ( tan `  ( _i  x.  x
) )
16 cdiv 9423 . . . 4  class  /
1715, 10, 16co 5858 . . 3  class  ( ( tan `  ( _i  x.  x ) )  /  _i )
182, 9, 17cmpt 4077 . 2  class  ( x  e.  ( `'cosh " ( CC  \  { 0 } ) )  |->  ( ( tan `  ( _i  x.  x ) )  /  _i ) )
191, 18wceq 1623 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  27570
  Copyright terms: Public domain W3C validator