HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem sin0 9766
Description: Value of the sine function at 0. (Contributed by Steve Rodriguez, 5-Jul-2006.)
Assertion
Ref Expression
sin0

Proof of Theorem sin0
StepHypRef Expression
1 neg0 7516 . . . 4
21fveq2i 4738 . . 3
3 0cn 7310 . . . 4
4 sinneg 9763 . . . 4
53, 4ax-mp 8 . . 3
62, 5eqtr3i 1940 . 2
7 sincl 9749 . . . 4
83, 7ax-mp 8 . . 3
98eqnegi 7775 . 2
106, 9mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wceq 1414   wcel 1416  cfv 4033  cc 7210  cc0 7212  cneg 7437  csin 9689
This theorem is referenced by:  tan0 9768  demoivreALT 9816  sin2kpi 14055  sinq12ge0 14077  sinkpi 14086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-15 1792  ax-ext 1900  ax-rep 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823  ax-inf2 6256  ax-resscn 7266  ax-1cn 7267  ax-icn 7268  ax-addcl 7269  ax-addrcl 7270  ax-mulcl 7271  ax-mulrcl 7272  ax-mulcom 7273  ax-addass 7274  ax-mulass 7275  ax-distr 7276  ax-i2m1 7277  ax-1ne0 7278  ax-1rid 7279  ax-rnegex 7280  ax-rrecex 7281  ax-cnre 7282  ax-pre-lttri 7283  ax-pre-lttrn 7284  ax-pre-ltadd 7285  ax-pre-mulgt0 7286  ax-pre-sup 7287
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-nel 2038  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2328  df-sbc 2495  df-csb 2577  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-if 3012  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-int 3268  df-iun 3307  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-lim 3710  df-suc 3711  df-om 3988  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-f1 4046  df-fo 4047  df-f1o 4048  df-fv 4049  df-iso 4050  df-ov 5004  df-oprab 5005  df-mpt 5165  df-mpt2 5166  df-1st 5296  df-2nd 5297  df-iota 5407  df-rdg 5498  df-1o 5535  df-er 5673  df-map 5765  df-pm 5766  df-en 5830  df-dom 5831  df-sdom 5832  df-fin 5833  df-riota 5987  df-sup 6170  df-card 6420  df-pnf 7325  df-mnf 7326  df-xr 7327  df-ltxr 7328  df-le 7329  df-sub 7455  df-neg 7457  df-div 7682  df-n 7921  df-2 7967  df-3 7968  df-n0 8105  df-z 8150  df-uz 8272  df-q 8354  df-rp 8481  df-fz 8630  df-fl 8724  df-seq 8819  df-exp 8873  df-fac 9006  df-hash 9053  df-shft 9098  df-cj 9120  df-re 9121  df-im 9122  df-sqr 9216  df-abs 9217  df-limsup 9374  df-clim 9390  df-rlim 9391  df-sum 9525  df-ef 9693  df-sin 9695
Copyright terms: Public domain