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. tan4thpiOLD
   64. sincos6thpi
   65. sincos3rdpi
   66. pigt3
   67. pige3
   68. pige3ALT
   69. abssinper
   70. sinkpi
   71. coskpi
   72. sineq0
   73. coseq1
   74. cos02pilt1
   75. cosq34lt1
   76. efeq1
   77. cosne0
   78. cosordlem
   79. cosord
   80. cos0pilt1
   81. cos11
   82. sinord
   83. recosf1o
   84. resinf1o
   85. tanord1
   86. tanord
   87. tanregt0
   88. 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. logi
   35. logneg
   36. logm1
   37. lognegb
   38. relogoprlem
   39. relogmul
   40. relogdiv
   41. explog
   42. reexplog
   43. relogexp
   44. relog
   45. relogiso
   46. reloggim
   47. logltb
   48. logfac
   49. eflogeq
   50. logleb
   51. rplogcl
   52. logge0
   53. logcj
   54. efiarg
   55. cosargd
   56. cosarg0d
   57. argregt0
   58. argrege0
   59. argimgt0
   60. argimlt0
   61. logimul
   62. logneg2
   63. logmul2
   64. logdiv2
   65. abslogle
   66. tanarg
   67. logdivlti
   68. logdivlt
   69. logdivle
   70. relogcld
   71. reeflogd
   72. relogmuld
   73. relogdivd
   74. logled
   75. relogefd
   76. rplogcld
   77. logge0d
   78. logge0b
   79. loggt0b
   80. logle1b
   81. loglt1b
   82. divlogrlim
   83. logno1
   84. dvrelog
   85. relogcn
   86. ellogdm
   87. logdmn0
   88. logdmnrp
   89. logdmss
   90. logcnlem2
   91. logcnlem3
   92. logcnlem4
   93. logcnlem5
   94. logcn
   95. dvloglem
   96. logdmopn
   97. logf1o2
   98. dvlog
   99. dvlog2lem
   100. dvlog2
   101. advlog
   102. advlogexp
   103. efopnlem1
   104. efopnlem2
   105. efopn
   106. logtayllem
   107. logtayl
   108. logtaylsum
   109. logtayl2
   110. logccv
   111. cxpval
   112. cxpef
   113. 0cxp
   114. cxpexpz
   115. cxpexp
   116. logcxp
   117. cxp0
   118. cxp1
   119. 1cxp
   120. ecxp
   121. cxpcl
   122. recxpcl
   123. rpcxpcl
   124. cxpne0
   125. cxpeq0
   126. cxpadd
   127. cxpp1
   128. cxpneg
   129. cxpsub
   130. cxpge0
   131. mulcxplem
   132. mulcxp
   133. cxprec
   134. divcxp
   135. cxpmul
   136. cxpmul2
   137. cxproot
   138. cxpmul2z
   139. abscxp
   140. abscxp2
   141. cxplt
   142. cxple
   143. cxplea
   144. cxple2
   145. cxplt2
   146. cxple2a
   147. cxplt3
   148. cxple3
   149. cxpsqrtlem
   150. cxpsqrt
   151. logsqrt
   152. cxp0d
   153. cxp1d
   154. 1cxpd
   155. cxpcld
   156. cxpmul2d
   157. 0cxpd
   158. cxpexpzd
   159. cxpefd
   160. cxpne0d
   161. cxpp1d
   162. cxpnegd
   163. cxpmul2zd
   164. cxpaddd
   165. cxpsubd
   166. cxpltd
   167. cxpled
   168. cxplead
   169. divcxpd
   170. recxpcld
   171. cxpge0d
   172. cxple2ad
   173. cxplt2d
   174. cxple2d
   175. mulcxpd
   176. recxpf1lem
   177. cxpsqrtth
   178. 2irrexpq
   179. cxprecd
   180. rpcxpcld
   181. logcxpd
   182. cxplt3d
   183. cxple3d
   184. cxpmuld
   185. cxpgt0d
   186. cxpcom
   187. dvcxp1
   188. dvcxp2
   189. dvsqrt
   190. dvcncxp1
   191. dvcnsqrt
   192. cxpcn
   193. cxpcnOLD
   194. cxpcn2
   195. cxpcn3lem
   196. cxpcn3
   197. resqrtcn
   198. sqrtcn
   199. cxpaddlelem
   200. cxpaddle
   201. abscxpbnd
   202. root1id
   203. root1eq1
   204. root1cj
   205. cxpeq
   206. zrtelqelz
   207. zrtdvds
   208. rtprmirr
   209. loglesqrt
   210. logreclem
   211. 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. efrlimOLD
    7. dfef2
    8. cxplim
    9. sqrtlim
    10. rlimcxp
    11. o1cxp
    12. cxp2limlem
    13. cxp2lim
    14. cxploglim
    15. cxploglim2
    16. divsqrtsumlem
    17. divsqrsumf
    18. divsqrsum
    19. divsqrtsum2
    20. 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