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

Theorem sin0 9679
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 7473 . . . 4
21fveq2i 4720 . . 3
3 0cn 7268 . . . 4
4 sinneg 9676 . . . 4
53, 4ax-mp 8 . . 3
62, 5eqtr3i 1940 . 2
7 sincl 9664 . . . 4
83, 7ax-mp 8 . . 3
98eqnegi 7731 . 2
106, 9mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wceq 1414   wcel 1416  cfv 4019  cc 7168  cc0 7170  cneg 7394  csin 9604
This theorem is referenced by:  tan0 9681  demoivreALT 9719  sin2kpi 13487  sinq12ge0 13508  sinkpi 13515
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 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809  ax-inf2 6217  ax-resscn 7224  ax-1cn 7225  ax-icn 7226  ax-addcl 7227  ax-addrcl 7228  ax-mulcl 7229  ax-mulrcl 7230  ax-mulcom 7231  ax-addass 7232  ax-mulass 7233  ax-distr 7234  ax-i2m1 7235  ax-1ne0 7236  ax-1rid 7237  ax-rnegex 7238  ax-rrecex 7239  ax-cnre 7240  ax-pre-lttri 7241  ax-pre-lttrn 7242  ax-pre-ltadd 7243  ax-pre-mulgt0 7244  ax-pre-sup 7245
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 2326  df-sbc 2493  df-csb 2575  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-if 3009  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-int 3258  df-iun 3297  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3974  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-f1 4032  df-fo 4033  df-f1o 4034  df-fv 4035  df-iso 4036  df-ov 4981  df-oprab 4982  df-mpt 5142  df-mpt2 5143  df-1st 5269  df-2nd 5270  df-iota 5377  df-rdg 5468  df-1o 5505  df-er 5643  df-map 5735  df-pm 5736  df-en 5800  df-dom 5801  df-sdom 5802  df-fin 5803  df-riota 5951  df-sup 6131  df-card 6381  df-pnf 7283  df-mnf 7284  df-xr 7285  df-ltxr 7286  df-le 7287  df-sub 7412  df-neg 7414  df-div 7638  df-n 7877  df-2 7923  df-3 7924  df-n0 8049  df-z 8094  df-uz 8214  df-q 8296  df-rp 8421  df-fz 8566  df-fl 8660  df-seq 8754  df-exp 8807  df-fac 8939  df-hash 8986  df-shft 9028  df-cj 9050  df-re 9051  df-im 9052  df-sqr 9144  df-abs 9145  df-limsup 9299  df-clim 9315  df-rlim 9316  df-sum 9441  df-ef 9608  df-sin 9610
Copyright terms: Public domain