Theorem sin0 9613

Description: Value of the sine function at 0. (Contributed by Steve Rodriguez, 5-Jul-2006.)

Assertion

Ref	Expression
sin0	|- (sin` 0) = 0

Proof of Theorem sin0

Step	Hyp	Ref	Expression
1		neg0 7410	. . . 4 |- -u0 = 0
2	1	fveq2i 4693	. . 3 |- (sin` -u0) = (sin` 0)
3		0cn 7205	. . . 4 |- 0 e. CC
4		sinneg 9610	. . . 4 |- (0 e. CC -> (sin` -u0) = -u(sin` 0))
5	3, 4	ax-mp 8	. . 3 |- (sin` -u0) = -u(sin` 0)
6	2, 5	eqtr3i 1939	. 2 |- (sin` 0) = -u(sin` 0)
7		sincl 9598	. . . 4 |- (0 e. CC -> (sin` 0) e. CC)
8	3, 7	ax-mp 8	. . 3 |- (sin` 0) e. CC
9	8	eqnegi 7668	. 2 |- ((sin` 0) = -u(sin` 0) <-> (sin` 0) = 0)
10	6, 9	mpbi 196	1 |- (sin` 0) = 0

Syntax hints:   = wceq 1413   e. wcel 1415  ` cfv 4007  CCcc 7105  0cc0 7107  -ucneg 7331  sincsin 9538

This theorem is referenced by:  tan0 9615  demoivreALT 9653  sin2kpi 13297  sinq12ge0 13318  sinkpi 13325

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-15 1791  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-inf2 6154  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-mulcom 7168  ax-addass 7169  ax-mulass 7170  ax-distr 7171  ax-i2m1 7172  ax-1ne0 7173  ax-1rid 7174  ax-rnegex 7175  ax-rrecex 7176  ax-cnre 7177  ax-pre-lttri 7178  ax-pre-lttrn 7179  ax-pre-ltadd 7180  ax-pre-mulgt0 7181  ax-pre-sup 7182

This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-nel 2037  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  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 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-iso 4024  df-ov 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-1st 5231  df-2nd 5232  df-iota 5336  df-rdg 5424  df-1o 5461  df-er 5598  df-map 5690  df-pm 5691  df-en 5750  df-dom 5751  df-sdom 5752  df-fin 5753  df-riota 5896  df-sup 6075  df-card 6318  df-pnf 7220  df-mnf 7221  df-xr 7222  df-ltxr 7223  df-le 7224  df-sub 7349  df-neg 7351  df-div 7575  df-n 7814  df-2 7860  df-3 7861  df-n0 7984  df-z 8029  df-uz 8149  df-q 8231  df-rp 8356  df-fz 8501  df-fl 8595  df-seq 8688  df-exp 8741  df-fac 8873  df-hash 8920  df-shft 8962  df-cj 8984  df-re 8985  df-im 8986  df-sqr 9078  df-abs 9079  df-limsup 9233  df-clim 9249  df-rlim 9250  df-sum 9375  df-ef 9542  df-sin 9544

Copyright terms: Public domain