Metamath Proof Explorer

Table of Contents - 14.3. Basic trigonometry

1. The exponential, sine, and cosine functions (cont.)
   1. efcn
   2. sincn
   3. coscn
   4. reeff1olem
   5. reeff1o
   6. reefiso
   7. efcvx
   8. reefgim
2. Properties of pi = 3.14159...
   1. pilem1
   2. pilem2
   3. pilem3
   4. pigt2lt4
   5. sinpi
   6. pire
   7. picn
   8. pipos
   9. pirp
   10. negpicn
   11. sinhalfpilem
   12. halfpire
   13. neghalfpire
   14. neghalfpirx
   15. pidiv2halves
   16. sinhalfpi
   17. coshalfpi
   18. cosneghalfpi
   19. efhalfpi
   20. cospi
   21. efipi
   22. eulerid
   23. sin2pi
   24. cos2pi
   25. ef2pi
   26. ef2kpi
   27. efper
   28. sinperlem
   29. sinper
   30. cosper
   31. sin2kpi
   32. cos2kpi
   33. sin2pim
   34. cos2pim
   35. sinmpi
   36. cosmpi
   37. sinppi
   38. cosppi
   39. efimpi
   40. sinhalfpip
   41. sinhalfpim
   42. coshalfpip
   43. coshalfpim
   44. ptolemy
   45. sincosq1lem
   46. sincosq1sgn
   47. sincosq2sgn
   48. sincosq3sgn
   49. sincosq4sgn
   50. coseq00topi
   51. coseq0negpitopi
   52. tanrpcl
   53. tangtx
   54. tanabsge
   55. sinq12gt0
   56. sinq12ge0
   57. sinq34lt0t
   58. cosq14gt0
   59. cosq14ge0
   60. sincosq1eq
   61. sincos4thpi
   62. tan4thpi
   63. sincos6thpi
   64. sincos3rdpi
   65. pigt3
   66. pige3
   67. pige3ALT
   68. abssinper
   69. sinkpi
   70. coskpi
   71. sineq0
   72. coseq1
   73. cos02pilt1
   74. cosq34lt1
   75. efeq1
   76. cosne0
   77. cosordlem
   78. cosord
   79. cos0pilt1
   80. cos11
   81. sinord
   82. recosf1o
   83. resinf1o
   84. tanord1
   85. tanord
   86. tanregt0
   87. negpitopissre
3. Mapping of the exponential function
   1. efgh
   2. efif1olem1
   3. efif1olem2
   4. efif1olem3
   5. efif1olem4
   6. efif1o
   7. efifo
   8. eff1olem
   9. eff1o
   10. efabl
   11. efsubm
   12. circgrp
   13. circsubm
4. The natural logarithm on complex numbers
   1. clog
   2. ccxp
   3. df-log
   4. df-cxp
   5. logrn
   6. ellogrn
   7. dflog2
   8. relogrn
   9. logrncn
   10. eff1o2
   11. logf1o
   12. dfrelog
   13. relogf1o
   14. logrncl
   15. logcl
   16. logimcl
   17. logcld
   18. logimcld
   19. logimclad
   20. abslogimle
   21. logrnaddcl
   22. relogcl
   23. eflog
   24. logeq0im1
   25. logccne0
   26. logne0
   27. reeflog
   28. logef
   29. relogef
   30. logeftb
   31. relogeftb
   32. log1
   33. loge
   34. logneg
   35. logm1
   36. lognegb
   37. relogoprlem
   38. relogmul
   39. relogdiv
   40. explog
   41. reexplog
   42. relogexp
   43. relog
   44. relogiso
   45. reloggim
   46. logltb
   47. logfac
   48. eflogeq
   49. logleb
   50. rplogcl
   51. logge0
   52. logcj
   53. efiarg
   54. cosargd
   55. cosarg0d
   56. argregt0
   57. argrege0
   58. argimgt0
   59. argimlt0
   60. logimul
   61. logneg2
   62. logmul2
   63. logdiv2
   64. abslogle
   65. tanarg
   66. logdivlti
   67. logdivlt
   68. logdivle
   69. relogcld
   70. reeflogd
   71. relogmuld
   72. relogdivd
   73. logled
   74. relogefd
   75. rplogcld
   76. logge0d
   77. logge0b
   78. loggt0b
   79. logle1b
   80. loglt1b
   81. divlogrlim
   82. logno1
   83. dvrelog
   84. relogcn
   85. ellogdm
   86. logdmn0
   87. logdmnrp
   88. logdmss
   89. logcnlem2
   90. logcnlem3
   91. logcnlem4
   92. logcnlem5
   93. logcn
   94. dvloglem
   95. logdmopn
   96. logf1o2
   97. dvlog
   98. dvlog2lem
   99. dvlog2
   100. advlog
   101. advlogexp
   102. efopnlem1
   103. efopnlem2
   104. efopn
   105. logtayllem
   106. logtayl
   107. logtaylsum
   108. logtayl2
   109. logccv
   110. cxpval
   111. cxpef
   112. 0cxp
   113. cxpexpz
   114. cxpexp
   115. logcxp
   116. cxp0
   117. cxp1
   118. 1cxp
   119. ecxp
   120. cxpcl
   121. recxpcl
   122. rpcxpcl
   123. cxpne0
   124. cxpeq0
   125. cxpadd
   126. cxpp1
   127. cxpneg
   128. cxpsub
   129. cxpge0
   130. mulcxplem
   131. mulcxp
   132. cxprec
   133. divcxp
   134. cxpmul
   135. cxpmul2
   136. cxproot
   137. cxpmul2z
   138. abscxp
   139. abscxp2
   140. cxplt
   141. cxple
   142. cxplea
   143. cxple2
   144. cxplt2
   145. cxple2a
   146. cxplt3
   147. cxple3
   148. cxpsqrtlem
   149. cxpsqrt
   150. logsqrt
   151. cxp0d
   152. cxp1d
   153. 1cxpd
   154. cxpcld
   155. cxpmul2d
   156. 0cxpd
   157. cxpexpzd
   158. cxpefd
   159. cxpne0d
   160. cxpp1d
   161. cxpnegd
   162. cxpmul2zd
   163. cxpaddd
   164. cxpsubd
   165. cxpltd
   166. cxpled
   167. cxplead
   168. divcxpd
   169. recxpcld
   170. cxpge0d
   171. cxple2ad
   172. cxplt2d
   173. cxple2d
   174. mulcxpd
   175. cxpsqrtth
   176. 2irrexpq
   177. cxprecd
   178. rpcxpcld
   179. logcxpd
   180. cxplt3d
   181. cxple3d
   182. cxpmuld
   183. cxpcom
   184. dvcxp1
   185. dvcxp2
   186. dvsqrt
   187. dvcncxp1
   188. dvcnsqrt
   189. cxpcn
   190. cxpcn2
   191. cxpcn3lem
   192. cxpcn3
   193. resqrtcn
   194. sqrtcn
   195. cxpaddlelem
   196. cxpaddle
   197. abscxpbnd
   198. root1id
   199. root1eq1
   200. root1cj
   201. cxpeq
   202. loglesqrt
   203. logreclem
   204. logrec
5. Logarithms to an arbitrary base
   1. clogb
   2. df-logb
   3. logbval
   4. logbcl
   5. logbid1
   6. logb1
   7. elogb
   8. logbchbase
   9. relogbval
   10. relogbcl
   11. relogbzcl
   12. relogbreexp
   13. relogbzexp
   14. relogbmul
   15. relogbmulexp
   16. relogbdiv
   17. relogbexp
   18. nnlogbexp
   19. logbrec
   20. logbleb
   21. logblt
   22. relogbcxp
   23. cxplogb
   24. relogbcxpb
   25. logbmpt
   26. logbf
   27. logbfval
   28. relogbf
   29. logblog
   30. logbgt0b
   31. logbgcd1irr
   32. 2logb9irr
   33. logbprmirr
   34. 2logb3irr
   35. 2logb9irrALT
   36. sqrt2cxp2logb9e3
   37. 2irrexpqALT
6. Theorems of Pythagoras, isosceles triangles, and intersecting chords
   1. angval
   2. angcan
   3. angneg
   4. angvald
   5. angcld
   6. angrteqvd
   7. cosangneg2d
   8. angrtmuld
   9. ang180lem1
   10. ang180lem2
   11. ang180lem3
   12. ang180lem4
   13. ang180lem5
   14. ang180
   15. lawcoslem1
   16. lawcos
   17. pythag
   18. isosctrlem1
   19. isosctrlem2
   20. isosctrlem3
   21. isosctr
   22. ssscongptld
   23. affineequiv
   24. affineequiv2
   25. affineequiv3
   26. affineequiv4
   27. affineequivne
   28. angpieqvdlem
   29. angpieqvdlem2
   30. angpined
   31. angpieqvd
   32. chordthmlem
   33. chordthmlem2
   34. chordthmlem3
   35. chordthmlem4
   36. chordthmlem5
   37. chordthm
   38. heron
7. Solutions of quadratic, cubic, and quartic equations
   1. quad2
   2. quad
   3. 1cubrlem
   4. 1cubr
   5. dcubic1lem
   6. dcubic2
   7. dcubic1
   8. dcubic
   9. mcubic
   10. cubic2
   11. cubic
   12. binom4
   13. dquartlem1
   14. dquartlem2
   15. dquart
   16. quart1cl
   17. quart1lem
   18. quart1
   19. quartlem1
   20. quartlem2
   21. quartlem3
   22. quartlem4
   23. quart
8. Inverse trigonometric functions
   1. casin
   2. cacos
   3. catan
   4. df-asin
   5. df-acos
   6. df-atan
   7. asinlem
   8. asinlem2
   9. asinlem3a
   10. asinlem3
   11. asinf
   12. asincl
   13. acosf
   14. acoscl
   15. atandm
   16. atandm2
   17. atandm3
   18. atandm4
   19. atanf
   20. atancl
   21. asinval
   22. acosval
   23. atanval
   24. atanre
   25. asinneg
   26. acosneg
   27. efiasin
   28. sinasin
   29. cosacos
   30. asinsinlem
   31. asinsin
   32. acoscos
   33. asin1
   34. acos1
   35. reasinsin
   36. asinsinb
   37. acoscosb
   38. asinbnd
   39. acosbnd
   40. asinrebnd
   41. asinrecl
   42. acosrecl
   43. cosasin
   44. sinacos
   45. atandmneg
   46. atanneg
   47. atan0
   48. atandmcj
   49. atancj
   50. atanrecl
   51. efiatan
   52. atanlogaddlem
   53. atanlogadd
   54. atanlogsublem
   55. atanlogsub
   56. efiatan2
   57. 2efiatan
   58. tanatan
   59. atandmtan
   60. cosatan
   61. cosatanne0
   62. atantan
   63. atantanb
   64. atanbndlem
   65. atanbnd
   66. atanord
   67. atan1
   68. bndatandm
   69. atans
   70. atans2
   71. atansopn
   72. atansssdm
   73. ressatans
   74. dvatan
   75. atancn
   76. atantayl
   77. atantayl2
   78. atantayl3
   79. leibpilem1
   80. leibpilem2
   81. leibpi
   82. leibpisum
   83. log2cnv
   84. log2tlbnd
9. The Birthday Problem
   1. log2ublem1
   2. log2ublem2
   3. log2ublem3
   4. log2ub
   5. log2le1
   6. birthdaylem1
   7. birthdaylem2
   8. birthdaylem3
   9. birthday
10. Areas in R^2
    1. carea
    2. df-area
    3. dmarea
    4. areambl
    5. areass
    6. dfarea
    7. areaf
    8. areacl
    9. areage0
    10. areaval
11. More miscellaneous converging sequences
    1. rlimcnp
    2. rlimcnp2
    3. rlimcnp3
    4. xrlimcnp
    5. efrlim
    6. dfef2
    7. cxplim
    8. sqrtlim
    9. rlimcxp
    10. o1cxp
    11. cxp2limlem
    12. cxp2lim
    13. cxploglim
    14. cxploglim2
    15. divsqrtsumlem
    16. divsqrsumf
    17. divsqrsum
    18. divsqrtsum2
    19. divsqrtsumo1
12. Inequality of arithmetic and geometric means
    1. cvxcl
    2. scvxcvx
    3. jensenlem1
    4. jensenlem2
    5. jensen
    6. amgmlem
    7. amgm
13. Euler-Mascheroni constant
    1. cem
    2. df-em
    3. logdifbnd
    4. logdiflbnd
    5. emcllem1
    6. emcllem2
    7. emcllem3
    8. emcllem4
    9. emcllem5
    10. emcllem6
    11. emcllem7
    12. emcl
    13. harmonicbnd
    14. harmonicbnd2
    15. emre
    16. emgt0
    17. harmonicbnd3
    18. harmoniclbnd
    19. harmonicubnd
    20. harmonicbnd4
    21. fsumharmonic
14. Zeta function
    1. czeta
    2. df-zeta
    3. zetacvg
15. Gamma function
    1. clgam
    2. cgam
    3. cigam
    4. df-lgam
    5. df-gam
    6. df-igam
    7. eldmgm
    8. dmgmaddn0
    9. dmlogdmgm
    10. rpdmgm
    11. dmgmn0
    12. dmgmaddnn0
    13. dmgmdivn0
    14. lgamgulmlem1
    15. lgamgulmlem2
    16. lgamgulmlem3
    17. lgamgulmlem4
    18. lgamgulmlem5
    19. lgamgulmlem6
    20. lgamgulm
    21. lgamgulm2
    22. lgambdd
    23. lgamucov
    24. lgamucov2
    25. lgamcvglem
    26. lgamcl
    27. lgamf
    28. gamf
    29. gamcl
    30. eflgam
    31. gamne0
    32. igamval
    33. igamz
    34. igamgam
    35. igamlgam
    36. igamf
    37. igamcl
    38. gamigam
    39. lgamcvg
    40. lgamcvg2
    41. gamcvg
    42. lgamp1
    43. gamp1
    44. gamcvg2lem
    45. gamcvg2
    46. regamcl
    47. relgamcl
    48. rpgamcl
    49. lgam1
    50. gam1
    51. facgam
    52. gamfac