Metamath Proof Explorer

Table of Contents - 5.11. Elementary trigonometry

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)
2. _e is irrational
   1. eirrlem
   2. eirr
   3. egt2lt3
   4. epos
   5. epr
   6. ene0
   7. ene1