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. 2pire
   8. picn
   9. 2picn
   10. pipos
   11. pige0
   12. pine0
   13. pirp
   14. negpicn
   15. sinhalfpilem
   16. halfpire
   17. neghalfpire
   18. neghalfpirx
   19. pidiv2halves
   20. sinhalfpi
   21. coshalfpi
   22. cosneghalfpi
   23. efhalfpi
   24. cospi
   25. efipi
   26. eulerid
   27. sin2pi
   28. cos2pi
   29. ef2pi
   30. ef2kpi
   31. efper
   32. sinperlem
   33. sinper
   34. cosper
   35. sin2kpi
   36. cos2kpi
   37. sin2pim
   38. cos2pim
   39. sinmpi
   40. cosmpi
   41. sinppi
   42. cosppi
   43. efimpi
   44. sinhalfpip
   45. sinhalfpim
   46. coshalfpip
   47. coshalfpim
   48. ptolemy
   49. sincosq1lem
   50. sincosq1sgn
   51. sincosq2sgn
   52. sincosq3sgn
   53. sincosq4sgn
   54. coseq00topi
   55. coseq0negpitopi
   56. tanrpcl
   57. tangtx
   58. tanabsge
   59. sinq12gt0
   60. sinq12ge0
   61. sinq34lt0t
   62. cosq14gt0
   63. cosq14ge0
   64. sincosq1eq
   65. sincos4thpi
   66. tan4thpi
   67. tan4thpiOLD
   68. sincos6thpi
   69. sincos3rdpi
   70. pigt3
   71. pige3
   72. pige3ALT
   73. abssinper
   74. sinkpi
   75. coskpi
   76. sineq0
   77. coseq1
   78. cos02pilt1
   79. cosq34lt1
   80. efeq1
   81. cosne0
   82. cosordlem
   83. cosord
   84. cos0pilt1
   85. cos11
   86. sinord
   87. recosf1o
   88. resinf1o
   89. tanord1
   90. tanord
   91. tanregt0
   92. 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. cxpcn2
   194. cxpcn3lem
   195. cxpcn3
   196. resqrtcn
   197. sqrtcn
   198. cxpaddlelem
   199. cxpaddle
   200. abscxpbnd
   201. root1id
   202. root1eq1
   203. root1cj
   204. cxpeq
   205. zrtelqelz
   206. zrtdvds
   207. rtprmirr
   208. loglesqrt
   209. logreclem
   210. 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