Metamath Proof Explorer


Theorem coshval

Description: Value of the hyperbolic cosine of a complex number. (Contributed by Mario Carneiro, 4-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 ax-icn โŠข i โˆˆ โ„‚
2 mulcl โŠข ( ( i โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( i ยท ๐ด ) โˆˆ โ„‚ )
3 1 2 mpan โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( i ยท ๐ด ) โˆˆ โ„‚ )
4 cosval โŠข ( ( i ยท ๐ด ) โˆˆ โ„‚ โ†’ ( cos โ€˜ ( i ยท ๐ด ) ) = ( ( ( exp โ€˜ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ€˜ ( - i ยท ( i ยท ๐ด ) ) ) ) / 2 ) )
5 3 4 syl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( cos โ€˜ ( i ยท ๐ด ) ) = ( ( ( exp โ€˜ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ€˜ ( - i ยท ( i ยท ๐ด ) ) ) ) / 2 ) )
6 negcl โŠข ( ๐ด โˆˆ โ„‚ โ†’ - ๐ด โˆˆ โ„‚ )
7 efcl โŠข ( - ๐ด โˆˆ โ„‚ โ†’ ( exp โ€˜ - ๐ด ) โˆˆ โ„‚ )
8 6 7 syl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( exp โ€˜ - ๐ด ) โˆˆ โ„‚ )
9 efcl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( exp โ€˜ ๐ด ) โˆˆ โ„‚ )
10 ixi โŠข ( i ยท i ) = - 1
11 10 oveq1i โŠข ( ( i ยท i ) ยท ๐ด ) = ( - 1 ยท ๐ด )
12 mulass โŠข ( ( i โˆˆ โ„‚ โˆง i โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( ( i ยท i ) ยท ๐ด ) = ( i ยท ( i ยท ๐ด ) ) )
13 1 1 12 mp3an12 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( i ยท i ) ยท ๐ด ) = ( i ยท ( i ยท ๐ด ) ) )
14 mulm1 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( - 1 ยท ๐ด ) = - ๐ด )
15 11 13 14 3eqtr3a โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( i ยท ( i ยท ๐ด ) ) = - ๐ด )
16 15 fveq2d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( exp โ€˜ ( i ยท ( i ยท ๐ด ) ) ) = ( exp โ€˜ - ๐ด ) )
17 1 1 mulneg1i โŠข ( - i ยท i ) = - ( i ยท i )
18 10 negeqi โŠข - ( i ยท i ) = - - 1
19 negneg1e1 โŠข - - 1 = 1
20 17 18 19 3eqtri โŠข ( - i ยท i ) = 1
21 20 oveq1i โŠข ( ( - i ยท i ) ยท ๐ด ) = ( 1 ยท ๐ด )
22 negicn โŠข - i โˆˆ โ„‚
23 mulass โŠข ( ( - i โˆˆ โ„‚ โˆง i โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( ( - i ยท i ) ยท ๐ด ) = ( - i ยท ( i ยท ๐ด ) ) )
24 22 1 23 mp3an12 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( - i ยท i ) ยท ๐ด ) = ( - i ยท ( i ยท ๐ด ) ) )
25 mulid2 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( 1 ยท ๐ด ) = ๐ด )
26 21 24 25 3eqtr3a โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( - i ยท ( i ยท ๐ด ) ) = ๐ด )
27 26 fveq2d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( exp โ€˜ ( - i ยท ( i ยท ๐ด ) ) ) = ( exp โ€˜ ๐ด ) )
28 16 27 oveq12d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( exp โ€˜ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ€˜ ( - i ยท ( i ยท ๐ด ) ) ) ) = ( ( exp โ€˜ - ๐ด ) + ( exp โ€˜ ๐ด ) ) )
29 8 9 28 comraddd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( exp โ€˜ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ€˜ ( - i ยท ( i ยท ๐ด ) ) ) ) = ( ( exp โ€˜ ๐ด ) + ( exp โ€˜ - ๐ด ) ) )
30 29 oveq1d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( ( exp โ€˜ ( i ยท ( i ยท ๐ด ) ) ) + ( exp โ€˜ ( - i ยท ( i ยท ๐ด ) ) ) ) / 2 ) = ( ( ( exp โ€˜ ๐ด ) + ( exp โ€˜ - ๐ด ) ) / 2 ) )
31 5 30 eqtrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( cos โ€˜ ( i ยท ๐ด ) ) = ( ( ( exp โ€˜ ๐ด ) + ( exp โ€˜ - ๐ด ) ) / 2 ) )