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