Theorem coshalfpip

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

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

Proof

Step	Hyp	Ref	Expression
1		coshalfpi	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
2	1	oveq1i	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A=0\cdot \cos A$$
3		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
4	3	mul02d	$$⊢A\in ℂ\to 0\cdot \cos A=0$$
5	2 4	eqtrid	$$⊢A\in ℂ\to \cos \left(\frac{\mathrm{\pi }}{2}\right)\cos A=0$$
6		sinhalfpi	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=1$$
7	6	oveq1i	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A=1\sin A$$
8		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
9	8	mullidd	$$⊢A\in ℂ\to 1\sin A=\sin A$$
10	7 9	eqtrid	$$⊢A\in ℂ\to \sin \left(\frac{\mathrm{\pi }}{2}\right)\sin A=\sin A$$
11	5 10	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$$
12		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
13	12	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
14		cosadd	$$⊢\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$$
15	13 14	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$$
16		df-neg	$$⊢-\sin A=0-\sin A$$
17	16	a1i	$$⊢A\in ℂ\to -\sin A=0-\sin A$$
18	11 15 17	3eqtr4d	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)+A\right)=-\sin A$$