Metamath Proof Explorer


Theorem cos0

Description: Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion cos0 cos0=1

Proof

Step Hyp Ref Expression
1 0re 0
2 recosval 0cos0=ei0
3 1 2 ax-mp cos0=ei0
4 it0e0 i0=0
5 4 fveq2i ei0=e0
6 ef0 e0=1
7 5 6 eqtri ei0=1
8 7 fveq2i ei0=1
9 re1 1=1
10 8 9 eqtri ei0=1
11 3 10 eqtri cos0=1