Metamath Proof Explorer

Table of Contents - 5.11.1. The exponential, sine, and cosine functions

1. ce
2. ceu
3. csin
4. ccos
5. ctan
6. cpi
7. df-ef
8. df-e
9. df-sin
10. df-cos
11. df-tan
12. df-pi
13. eftcl
14. reeftcl
15. eftabs
16. eftval
17. efcllem
18. ef0lem
19. efval
20. esum
21. eff
22. efcl
23. efcld
24. efval2
25. efcvg
26. efcvgfsum
27. reefcl
28. reefcld
29. ere
30. ege2le3
31. ef0
32. efcj
33. efaddlem
34. efadd
35. fprodefsum
36. efcan
37. efne0
38. efneg
39. eff2
40. efsub
41. efexp
42. efzval
43. efgt0
44. rpefcl
45. rpefcld
46. eftlcvg
47. eftlcl
48. reeftlcl
49. eftlub
50. efsep
51. effsumlt
52. eft0val
53. ef4p
54. efgt1p2
55. efgt1p
56. efgt1
57. eflt
58. efle
59. reef11
60. reeff1
61. eflegeo
62. sinval
63. cosval
64. sinf
65. cosf
66. sincl
67. coscl
68. tanval
69. tancl
70. sincld
71. coscld
72. tancld
73. tanval2
74. tanval3
75. resinval
76. recosval
77. efi4p
78. resin4p
79. recos4p
80. resincl
81. recoscl
82. retancl
83. resincld
84. recoscld
85. retancld
86. sinneg
87. cosneg
88. tanneg
89. sin0
90. cos0
91. tan0
92. efival
93. efmival
94. sinhval
95. coshval
96. resinhcl
97. rpcoshcl
98. recoshcl
99. retanhcl
100. tanhlt1
101. tanhbnd
102. efeul
103. efieq
104. sinadd
105. cosadd
106. tanaddlem
107. tanadd
108. sinsub
109. cossub
110. addsin
111. subsin
112. sinmul
113. cosmul
114. addcos
115. subcos
116. sincossq
117. sin2t
118. cos2t
119. cos2tsin
120. sinbnd
121. cosbnd
122. sinbnd2
123. cosbnd2
124. ef01bndlem
125. sin01bnd
126. cos01bnd
127. cos1bnd
128. cos2bnd
129. sinltx
130. sin01gt0
131. cos01gt0
132. sin02gt0
133. sincos1sgn
134. sincos2sgn
135. sin4lt0
136. absefi
137. absef
138. absefib
139. efieq1re
140. demoivre
141. demoivreALT
142. The circle constant (tau = 2 pi)
     1. ctau
     2. df-tau