Theorem cospim

Description: Cosine of a number subtracted from _pi . (Contributed by SN, 19-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in ℂ\to A\in ℂ$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3	2	a1i	$$⊢A\in ℂ\to \mathrm{\pi }\in ℂ$$
4	1 3	subcld	$$⊢A\in ℂ\to A-\mathrm{\pi }\in ℂ$$
5		cosneg	$$⊢A-\mathrm{\pi }\in ℂ\to \cos \left(-\left(A-\mathrm{\pi }\right)\right)=\cos \left(A-\mathrm{\pi }\right)$$
6	4 5	syl	$$⊢A\in ℂ\to \cos \left(-\left(A-\mathrm{\pi }\right)\right)=\cos \left(A-\mathrm{\pi }\right)$$
7	1 3	negsubdi2d	$$⊢A\in ℂ\to -\left(A-\mathrm{\pi }\right)=\mathrm{\pi }-A$$
8	7	fveq2d	$$⊢A\in ℂ\to \cos \left(-\left(A-\mathrm{\pi }\right)\right)=\cos \left(\mathrm{\pi }-A\right)$$
9		cosmpi	$$⊢A\in ℂ\to \cos \left(A-\mathrm{\pi }\right)=-\cos A$$
10	6 8 9	3eqtr3d	$$⊢A\in ℂ\to \cos \left(\mathrm{\pi }-A\right)=-\cos A$$