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

Theorem sin0 9496
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 7309 . . . 4
21fveq2i 4675 . . 3
3 0cn 7104 . . . 4
4 sinneg 9493 . . . 4
53, 4ax-mp 8 . . 3
62, 5eqtr3i 1951 . 2
7 sincl 9481 . . . 4
83, 7ax-mp 8 . . 3
98eqnegi 7567 . 2
106, 9mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wceq 1425   wcel 1427  cfv 4003  cc 7004  cc0 7006  cneg 7230  csin 9421
This theorem is referenced by:  tan0 9498  demoivreALT 9536  sin2kpi 12690  sinq12ge0 12711  sinkpi 12718
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-15 1803  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-inf2 6078  ax-resscn 7060  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-addrcl 7064  ax-mulcl 7065  ax-mulrcl 7066  ax-mulcom 7067  ax-addass 7068  ax-mulass 7069  ax-distr 7070  ax-i2m1 7071  ax-1ne0 7072  ax-1rid 7073  ax-rnegex 7074  ax-rrecex 7075  ax-cnre 7076  ax-pre-lttri 7077  ax-pre-lttrn 7078  ax-pre-ltadd 7079  ax-pre-mulgt0 7080  ax-pre-sup 7081
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-nel 2050  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-if 3005  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-lim 3683  df-suc 3684  df-om 3958  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-f1 4016  df-fo 4017  df-f1o 4018  df-fv 4019  df-iso 4020  df-ov 4926  df-oprab 4927  df-mpt 5063  df-mpt2 5064  df-1st 5173  df-2nd 5174  df-iota 5277  df-rdg 5363  df-1o 5400  df-er 5537  df-map 5625  df-pm 5626  df-en 5682  df-dom 5683  df-sdom 5684  df-fin 5685  df-riota 5825  df-sup 5999  df-card 6242  df-pnf 7119  df-mnf 7120  df-xr 7121  df-ltxr 7122  df-le 7123  df-sub 7248  df-neg 7250  df-div 7474  df-n 7713  df-2 7759  df-3 7760  df-n0 7883  df-z 7927  df-uz 8047  df-q 8129  df-rp 8254  df-fz 8399  df-fl 8492  df-seq 8585  df-exp 8637  df-fac 8770  df-hash 8816  df-shft 8849  df-cj 8871  df-re 8872  df-im 8873  df-sqr 8965  df-abs 8966  df-limsup 9120  df-clim 9136  df-rlim 9137  df-sum 9262  df-ef 9425  df-sin 9427
Copyright terms: Public domain