Theorem sinpim

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

	Ref	Expression
Assertion	sinpim	$$⊢A\in ℂ\to \sin \left(\mathrm{\pi }-A\right)=\sin 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		sinneg	$$⊢A-\mathrm{\pi }\in ℂ\to \sin \left(-\left(A-\mathrm{\pi }\right)\right)=-\sin \left(A-\mathrm{\pi }\right)$$
6	4 5	syl	$$⊢A\in ℂ\to \sin \left(-\left(A-\mathrm{\pi }\right)\right)=-\sin \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 \sin \left(-\left(A-\mathrm{\pi }\right)\right)=\sin \left(\mathrm{\pi }-A\right)$$
9		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
10		sinmpi	$$⊢A\in ℂ\to \sin \left(A-\mathrm{\pi }\right)=-\sin A$$
11	10	eqcomd	$$⊢A\in ℂ\to -\sin A=\sin \left(A-\mathrm{\pi }\right)$$
12	9 11	negcon1ad	$$⊢A\in ℂ\to -\sin \left(A-\mathrm{\pi }\right)=\sin A$$
13	6 8 12	3eqtr3d	$$⊢A\in ℂ\to \sin \left(\mathrm{\pi }-A\right)=\sin A$$