This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efimpi

Description: The exponential function at _i times a real number less _pi . (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion efimpi ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 𝐴 − π ) ) ) = - ( exp ‘ ( i · 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ π ∈ ℂ ) → ( 𝐴 − π ) ∈ ℂ )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − π ) ∈ ℂ )
4 efival ⊢ ( ( 𝐴 − π ) ∈ ℂ → ( exp ‘ ( i · ( 𝐴 − π ) ) ) = ( ( cos ‘ ( 𝐴 − π ) ) + ( i · ( sin ‘ ( 𝐴 − π ) ) ) ) )
5 3 4 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 𝐴 − π ) ) ) = ( ( cos ‘ ( 𝐴 − π ) ) + ( i · ( sin ‘ ( 𝐴 − π ) ) ) ) )
6 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
7 ax-icn ⊢ i ∈ ℂ
8 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
9 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
10 7 8 9 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
11 6 10 negdid ⊢ ( 𝐴 ∈ ℂ → - ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( - ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) )
12 cosmpi ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 𝐴 − π ) ) = - ( cos ‘ 𝐴 ) )
13 sinmpi ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 − π ) ) = - ( sin ‘ 𝐴 ) )
14 13 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( i · ( sin ‘ ( 𝐴 − π ) ) ) = ( i · - ( sin ‘ 𝐴 ) ) )
15 mulneg2 ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · - ( sin ‘ 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
16 7 8 15 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · - ( sin ‘ 𝐴 ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
17 14 16 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( i · ( sin ‘ ( 𝐴 − π ) ) ) = - ( i · ( sin ‘ 𝐴 ) ) )
18 12 17 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( 𝐴 − π ) ) + ( i · ( sin ‘ ( 𝐴 − π ) ) ) ) = ( - ( cos ‘ 𝐴 ) + - ( i · ( sin ‘ 𝐴 ) ) ) )
19 11 18 eqtr4d ⊢ ( 𝐴 ∈ ℂ → - ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ ( 𝐴 − π ) ) + ( i · ( sin ‘ ( 𝐴 − π ) ) ) ) )
20 5 19 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 𝐴 − π ) ) ) = - ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
21 efival ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
22 21 negeqd ⊢ ( 𝐴 ∈ ℂ → - ( exp ‘ ( i · 𝐴 ) ) = - ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
23 20 22 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 𝐴 − π ) ) ) = - ( exp ‘ ( i · 𝐴 ) ) )