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. efne0d
38. efne0
39. efne0OLD
40. efneg
41. eff2
42. efsub
43. efexp
44. efzval
45. efgt0
46. rpefcl
47. rpefcld
48. eftlcvg
49. eftlcl
50. reeftlcl
51. eftlub
52. efsep
53. effsumlt
54. eft0val
55. ef4p
56. efgt1p2
57. efgt1p
58. efgt1
59. eflt
60. efle
61. reef11
62. reeff1
63. eflegeo
64. sinval
65. cosval
66. sinf
67. cosf
68. sincl
69. coscl
70. tanval
71. tancl
72. sincld
73. coscld
74. tancld
75. tanval2
76. tanval3
77. resinval
78. recosval
79. efi4p
80. resin4p
81. recos4p
82. resincl
83. recoscl
84. retancl
85. resincld
86. recoscld
87. retancld
88. sinneg
89. cosneg
90. tanneg
91. sin0
92. cos0
93. tan0
94. efival
95. efmival
96. sinhval
97. coshval
98. resinhcl
99. rpcoshcl
100. recoshcl
101. retanhcl
102. tanhlt1
103. tanhbnd
104. efeul
105. efieq
106. sinadd
107. cosadd
108. tanaddlem
109. tanadd
110. sinsub
111. cossub
112. addsin
113. subsin
114. sinmul
115. cosmul
116. addcos
117. subcos
118. sincossq
119. sin2t
120. cos2t
121. cos2tsin
122. sinbnd
123. cosbnd
124. sinbnd2
125. cosbnd2
126. ef01bndlem
127. sin01bnd
128. cos01bnd
129. cos1bnd
130. cos2bnd
131. sinltx
132. sin01gt0
133. cos01gt0
134. sin02gt0
135. sincos1sgn
136. sincos2sgn
137. sin4lt0
138. absefi
139. absef
140. absefib
141. efieq1re
142. demoivre
143. demoivreALT
144. The circle constant (tau = 2 pi)
     1. ctau
     2. df-tau