Step | Hyp | Ref
| Expression |
1 | | ctan 15940 |
. 2
class
tan |
2 | | vx |
. . 3
setvar π₯ |
3 | | ccos 15939 |
. . . . 5
class
cos |
4 | 3 | ccnv 5630 |
. . . 4
class β‘cos |
5 | | cc 11045 |
. . . . 5
class
β |
6 | | cc0 11047 |
. . . . . 6
class
0 |
7 | 6 | csn 4584 |
. . . . 5
class
{0} |
8 | 5, 7 | cdif 3905 |
. . . 4
class (β
β {0}) |
9 | 4, 8 | cima 5634 |
. . 3
class (β‘cos β (β β
{0})) |
10 | 2 | cv 1540 |
. . . . 5
class π₯ |
11 | | csin 15938 |
. . . . 5
class
sin |
12 | 10, 11 | cfv 6493 |
. . . 4
class
(sinβπ₯) |
13 | 10, 3 | cfv 6493 |
. . . 4
class
(cosβπ₯) |
14 | | cdiv 11808 |
. . . 4
class
/ |
15 | 12, 13, 14 | co 7353 |
. . 3
class
((sinβπ₯) /
(cosβπ₯)) |
16 | 2, 9, 15 | cmpt 5186 |
. 2
class (π₯ β (β‘cos β (β β {0})) β¦
((sinβπ₯) /
(cosβπ₯))) |
17 | 1, 16 | wceq 1541 |
1
wff tan =
(π₯ β (β‘cos β (β β {0})) β¦
((sinβπ₯) /
(cosβπ₯))) |