Theorem sinhalfpim

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

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

Proof

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