This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sin0

Description: Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005)

Ref Expression
Assertion sin0 ⊢ sin ⁡ 0 = 0

Proof

Step Hyp Ref Expression
1 neg0 ⊢ − 0 = 0
2 1 fveq2i ⊢ sin ⁡ -0 = sin ⁡ 0
3 0cn ⊢ 0 ∈ ℂ
4 sinneg ⊢ 0 ∈ ℂ → sin ⁡ -0 = − sin ⁡ 0
5 3 4 ax-mp ⊢ sin ⁡ -0 = − sin ⁡ 0
6 2 5 eqtr3i ⊢ sin ⁡ 0 = − sin ⁡ 0
7 sincl ⊢ 0 ∈ ℂ → sin ⁡ 0 ∈ ℂ
8 3 7 ax-mp ⊢ sin ⁡ 0 ∈ ℂ
9 8 eqnegi ⊢ sin ⁡ 0 = − sin ⁡ 0 ↔ sin ⁡ 0 = 0
10 6 9 mpbi ⊢ sin ⁡ 0 = 0