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	mulid2d	⊢ ( 𝐴 ∈ ℂ → ( 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 ‘ 𝐴 ) )