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

Metamath Proof Explorer

Theorem coshalfpip

Description: The cosine of _pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion coshalfpip ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) + 𝐴 ) ) = - ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 coshalfpi ⊢ ( cos ‘ ( π / 2 ) ) = 0
2 1 oveq1i ⊢ ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) = ( 0 · ( cos ‘ 𝐴 ) )
3 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
4 3 mul02d ⊢ ( 𝐴 ∈ ℂ → ( 0 · ( cos ‘ 𝐴 ) ) = 0 )
5 2 4 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) = 0 )
6 sinhalfpi ⊢ ( sin ‘ ( π / 2 ) ) = 1
7 6 oveq1i ⊢ ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) = ( 1 · ( sin ‘ 𝐴 ) )
8 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
9 8 mullidd ⊢ ( 𝐴 ∈ ℂ → ( 1 · ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
10 7 9 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
11 5 10 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) − ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) = ( 0 − ( sin ‘ 𝐴 ) ) )
12 halfpire ⊢ ( π / 2 ) ∈ ℝ
13 12 recni ⊢ ( π / 2 ) ∈ ℂ
14 cosadd ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( cos ‘ ( ( π / 2 ) + 𝐴 ) ) = ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) − ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) )
15 13 14 mpan ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) + 𝐴 ) ) = ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) − ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) )
16 df-neg ⊢ - ( sin ‘ 𝐴 ) = ( 0 − ( sin ‘ 𝐴 ) )
17 16 a1i ⊢ ( 𝐴 ∈ ℂ → - ( sin ‘ 𝐴 ) = ( 0 − ( sin ‘ 𝐴 ) ) )
18 11 15 17 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) + 𝐴 ) ) = - ( sin ‘ 𝐴 ) )