Metamath Proof Explorer


Theorem cosval

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

Ref Expression
Assertion cosval ( ๐ด โˆˆ โ„‚ โ†’ ( cos โ€˜ ๐ด ) = ( ( ( exp โ€˜ ( i ยท ๐ด ) ) + ( exp โ€˜ ( - i ยท ๐ด ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 oveq2 โŠข ( ๐‘ฅ = ๐ด โ†’ ( i ยท ๐‘ฅ ) = ( i ยท ๐ด ) )
2 1 fveq2d โŠข ( ๐‘ฅ = ๐ด โ†’ ( exp โ€˜ ( i ยท ๐‘ฅ ) ) = ( exp โ€˜ ( i ยท ๐ด ) ) )
3 oveq2 โŠข ( ๐‘ฅ = ๐ด โ†’ ( - i ยท ๐‘ฅ ) = ( - i ยท ๐ด ) )
4 3 fveq2d โŠข ( ๐‘ฅ = ๐ด โ†’ ( exp โ€˜ ( - i ยท ๐‘ฅ ) ) = ( exp โ€˜ ( - i ยท ๐ด ) ) )
5 2 4 oveq12d โŠข ( ๐‘ฅ = ๐ด โ†’ ( ( exp โ€˜ ( i ยท ๐‘ฅ ) ) + ( exp โ€˜ ( - i ยท ๐‘ฅ ) ) ) = ( ( exp โ€˜ ( i ยท ๐ด ) ) + ( exp โ€˜ ( - i ยท ๐ด ) ) ) )
6 5 oveq1d โŠข ( ๐‘ฅ = ๐ด โ†’ ( ( ( exp โ€˜ ( i ยท ๐‘ฅ ) ) + ( exp โ€˜ ( - i ยท ๐‘ฅ ) ) ) / 2 ) = ( ( ( exp โ€˜ ( i ยท ๐ด ) ) + ( exp โ€˜ ( - i ยท ๐ด ) ) ) / 2 ) )
7 df-cos โŠข cos = ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ( ( ( exp โ€˜ ( i ยท ๐‘ฅ ) ) + ( exp โ€˜ ( - i ยท ๐‘ฅ ) ) ) / 2 ) )
8 ovex โŠข ( ( ( exp โ€˜ ( i ยท ๐ด ) ) + ( exp โ€˜ ( - i ยท ๐ด ) ) ) / 2 ) โˆˆ V
9 6 7 8 fvmpt โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( cos โ€˜ ๐ด ) = ( ( ( exp โ€˜ ( i ยท ๐ด ) ) + ( exp โ€˜ ( - i ยท ๐ด ) ) ) / 2 ) )