Theorem coshalfpim

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

	Ref	Expression
Assertion	coshalfpim	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=\sin A$$

Proof

Step	Hyp	Ref	Expression
1		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
2	1	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
3		cossub	$$⊢\left(\frac{\mathrm{\pi }}{2}\in ℂ\wedge A\in ℂ\right)\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=\cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A+\sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A$$
4	2 3	mpan	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=\cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A+\sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A$$
5		coshalfpi	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
6	5	oveq1i	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A=0\cdot \cos A$$
7		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
8	7	mul02d	$$⊢A\in ℂ\to 0\cdot \cos A=0$$
9	6 8	syl5eq	$$⊢A\in ℂ\to \cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A=0$$
10		sinhalfpi	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=1$$
11	10	oveq1i	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A=1\sin A$$
12		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
13	12	mulid2d	$$⊢A\in ℂ\to 1\sin A=\sin A$$
14	11 13	syl5eq	$$⊢A\in ℂ\to \sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A=\sin A$$
15	9 14	oveq12d	$$⊢A\in ℂ\to \cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A+\sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A=0+\sin A$$
16	12	addid2d	$$⊢A\in ℂ\to 0+\sin A=\sin A$$
17	4 15 16	3eqtrd	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=\sin A$$