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