Metamath Proof Explorer

Theorem recosval

Description: The cosine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion recosval ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 cjmul ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( i · 𝐴 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) )
4 1 2 3 sylancr ⊢ ( 𝐴 ∈ ℝ → ( ∗ ‘ ( i · 𝐴 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) )
5 cji ⊢ ( ∗ ‘ i ) = - i
6 5 oveq1i ⊢ ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) = ( - i · ( ∗ ‘ 𝐴 ) )
7 cjre ⊢ ( 𝐴 ∈ ℝ → ( ∗ ‘ 𝐴 ) = 𝐴 )
8 7 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( - i · ( ∗ ‘ 𝐴 ) ) = ( - i · 𝐴 ) )
9 6 8 eqtrid ⊢ ( 𝐴 ∈ ℝ → ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) = ( - i · 𝐴 ) )
10 4 9 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( ∗ ‘ ( i · 𝐴 ) ) = ( - i · 𝐴 ) )
11 10 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ∗ ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
12 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
13 1 2 12 sylancr ⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∈ ℂ )
14 efcj ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( ∗ ‘ ( i · 𝐴 ) ) ) = ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )
15 13 14 syl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( ∗ ‘ ( i · 𝐴 ) ) ) = ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )
16 11 15 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( - i · 𝐴 ) ) = ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )
17 16 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) + ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ) )
18 17 oveq1d ⊢ ( 𝐴 ∈ ℝ → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ) / 2 ) )
19 cosval ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
20 2 19 syl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
21 efcl ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
22 reval ⊢ ( ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ) / 2 ) )
23 13 21 22 3syl ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( ∗ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ) / 2 ) )
24 18 20 23 3eqtr4d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )