Metamath Proof Explorer


Theorem sinval

Description: Value of the sine function. (Contributed by NM, 14-Mar-2005) (Revised by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion sinval A sin A = e i A e i A 2 i

Proof

Step Hyp Ref Expression
1 oveq2 x = A i x = i A
2 1 fveq2d x = A e i x = e i A
3 oveq2 x = A i x = i A
4 3 fveq2d x = A e i x = e i A
5 2 4 oveq12d x = A e i x e i x = e i A e i A
6 5 oveq1d x = A e i x e i x 2 i = e i A e i A 2 i
7 df-sin sin = x e i x e i x 2 i
8 ovex e i A e i A 2 i V
9 6 7 8 fvmpt A sin A = e i A e i A 2 i