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

Theorem sin0 10740
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 8375 . . . 4
21fveq2i 4995 . . 3
3 0cn 8164 . . . 4
4 sinneg 10737 . . . 4
53, 4ax-mp 8 . . 3
62, 5eqtr3i 2112 . 2
7 sincl 10723 . . . 4
83, 7ax-mp 8 . . 3
98eqnegi 8636 . 2
106, 9mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wceq 1531   wcel 1533  cfv 4261  cc 8059  cc0 8061  cneg 8296  csin 10664
This theorem is referenced by:  tan0  10742  demoivreALT  10792  sin2kpi  15564  sinq12ge0  15587  sinkpi  15596
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-15 1958  ax-ext 2072  ax-rep 3677  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-inf2 6755  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-addrcl 8121  ax-mulcl 8122  ax-mulrcl 8123  ax-mulcom 8124  ax-addass 8125  ax-mulass 8126  ax-distr 8127  ax-i2m1 8128  ax-1ne0 8129  ax-1rid 8130  ax-rnegex 8131  ax-rrecex 8132  ax-cnre 8133  ax-pre-lttri 8134  ax-pre-lttrn 8135  ax-pre-ltadd 8136  ax-pre-mulgt0 8137  ax-pre-sup 8138
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-nel 2210  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-int 3469  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-se 3892  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-iso 4278  df-ov 5298  df-oprab 5299  df-mpt 5461  df-mpt2 5462  df-1st 5613  df-2nd 5614  df-iota 5740  df-recs 5814  df-rdg 5849  df-1o 5903  df-oadd 5907  df-er 6076  df-map 6171  df-pm 6172  df-en 6249  df-dom 6250  df-sdom 6251  df-fin 6252  df-riota 6415  df-sup 6607  df-oi 6639  df-card 6983  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8314  df-neg 8316  df-div 8542  df-n 8782  df-2 8829  df-3 8830  df-n0 8975  df-z 9026  df-uz 9222  df-rp 9440  df-fz 9589  df-fl 9675  df-seq 9775  df-exp 9830  df-fac 9967  df-hash 10015  df-shft 10064  df-cj 10086  df-re 10087  df-im 10088  df-sqr 10184  df-abs 10185  df-limsup 10343  df-clim 10359  df-rlim 10360  df-sum 10495  df-ef 10668  df-sin 10670
Copyright terms: Public domain