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