Metamath Proof Explorer
Table of Contents - 5.11.1. The exponential, sine, and cosine functions
- ce
- ceu
- csin
- ccos
- ctan
- cpi
- df-ef
- df-e
- df-sin
- df-cos
- df-tan
- df-pi
- eftcl
- reeftcl
- eftabs
- eftval
- efcllem
- ef0lem
- efval
- esum
- eff
- efcl
- efval2
- efcvg
- efcvgfsum
- reefcl
- reefcld
- ere
- ege2le3
- ef0
- efcj
- efaddlem
- efadd
- fprodefsum
- efcan
- efne0
- efneg
- eff2
- efsub
- efexp
- efzval
- efgt0
- rpefcl
- rpefcld
- eftlcvg
- eftlcl
- reeftlcl
- eftlub
- efsep
- effsumlt
- eft0val
- ef4p
- efgt1p2
- efgt1p
- efgt1
- eflt
- efle
- reef11
- reeff1
- eflegeo
- sinval
- cosval
- sinf
- cosf
- sincl
- coscl
- tanval
- tancl
- sincld
- coscld
- tancld
- tanval2
- tanval3
- resinval
- recosval
- efi4p
- resin4p
- recos4p
- resincl
- recoscl
- retancl
- resincld
- recoscld
- retancld
- sinneg
- cosneg
- tanneg
- sin0
- cos0
- tan0
- efival
- efmival
- sinhval
- coshval
- resinhcl
- rpcoshcl
- recoshcl
- retanhcl
- tanhlt1
- tanhbnd
- efeul
- efieq
- sinadd
- cosadd
- tanaddlem
- tanadd
- sinsub
- cossub
- addsin
- subsin
- sinmul
- cosmul
- addcos
- subcos
- sincossq
- sin2t
- cos2t
- cos2tsin
- sinbnd
- cosbnd
- sinbnd2
- cosbnd2
- ef01bndlem
- sin01bnd
- cos01bnd
- cos1bnd
- cos2bnd
- sinltx
- sin01gt0
- cos01gt0
- sin02gt0
- sincos1sgn
- sincos2sgn
- sin4lt0
- absefi
- absef
- absefib
- efieq1re
- demoivre
- demoivreALT
- The circle constant (tau = 2 pi)
- ctau
- df-tau