Theorem sinhalfpim

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

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

Proof

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