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