Theorem coshalfpim

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

	Ref	Expression
Assertion	coshalfpim	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		halfpire	⊢ ( π / 2 ) ∈ ℝ
2	1	recni	⊢ ( π / 2 ) ∈ ℂ
3		cossub	⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) )
4	2 3	mpan	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) )
5		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
6	5	oveq1i	⊢ ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) = ( 0 · ( cos ‘ 𝐴 ) )
7		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
8	7	mul02d	⊢ ( 𝐴 ∈ ℂ → ( 0 · ( cos ‘ 𝐴 ) ) = 0 )
9	6 8	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) = 0 )
10		sinhalfpi	⊢ ( sin ‘ ( π / 2 ) ) = 1
11	10	oveq1i	⊢ ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) = ( 1 · ( sin ‘ 𝐴 ) )
12		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
13	12	mulid2d	⊢ ( 𝐴 ∈ ℂ → ( 1 · ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
14	11 13	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
15	9 14	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ ( π / 2 ) ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ ( π / 2 ) ) · ( sin ‘ 𝐴 ) ) ) = ( 0 + ( sin ‘ 𝐴 ) ) )
16	12	addid2d	⊢ ( 𝐴 ∈ ℂ → ( 0 + ( sin ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
17	4 15 16	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )