Step | Hyp | Ref
| Expression |
1 | | ctanh 47263 |
. 2
class
tanh |
2 | | vx |
. . 3
setvar π₯ |
3 | | ccosh 47262 |
. . . . 5
class
cosh |
4 | 3 | ccnv 5633 |
. . . 4
class β‘cosh |
5 | | cc 11054 |
. . . . 5
class
β |
6 | | cc0 11056 |
. . . . . 6
class
0 |
7 | 6 | csn 4587 |
. . . . 5
class
{0} |
8 | 5, 7 | cdif 3908 |
. . . 4
class (β
β {0}) |
9 | 4, 8 | cima 5637 |
. . 3
class (β‘cosh β (β β
{0})) |
10 | | ci 11058 |
. . . . . 6
class
i |
11 | 2 | cv 1541 |
. . . . . 6
class π₯ |
12 | | cmul 11061 |
. . . . . 6
class
Β· |
13 | 10, 11, 12 | co 7358 |
. . . . 5
class (i
Β· π₯) |
14 | | ctan 15953 |
. . . . 5
class
tan |
15 | 13, 14 | cfv 6497 |
. . . 4
class
(tanβ(i Β· π₯)) |
16 | | cdiv 11817 |
. . . 4
class
/ |
17 | 15, 10, 16 | co 7358 |
. . 3
class
((tanβ(i Β· π₯)) / i) |
18 | 2, 9, 17 | cmpt 5189 |
. 2
class (π₯ β (β‘cosh β (β β {0})) β¦
((tanβ(i Β· π₯))
/ i)) |
19 | 1, 18 | wceq 1542 |
1
wff tanh =
(π₯ β (β‘cosh β (β β {0})) β¦
((tanβ(i Β· π₯))
/ i)) |