Theorem sinpim

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

	Ref	Expression
Assertion	sinpim	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( π − 𝐴 ) ) = ( sin ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
2		picn	⊢ π ∈ ℂ
3	2	a1i	⊢ ( 𝐴 ∈ ℂ → π ∈ ℂ )
4	1 3	subcld	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − π ) ∈ ℂ )
5		sinneg	⊢ ( ( 𝐴 − π ) ∈ ℂ → ( sin ‘ - ( 𝐴 − π ) ) = - ( sin ‘ ( 𝐴 − π ) ) )
6	4 5	syl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - ( 𝐴 − π ) ) = - ( sin ‘ ( 𝐴 − π ) ) )
7	1 3	negsubdi2d	⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 − π ) = ( π − 𝐴 ) )
8	7	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - ( 𝐴 − π ) ) = ( sin ‘ ( π − 𝐴 ) ) )
9		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
10		sinmpi	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 − π ) ) = - ( sin ‘ 𝐴 ) )
11	10	eqcomd	⊢ ( 𝐴 ∈ ℂ → - ( sin ‘ 𝐴 ) = ( sin ‘ ( 𝐴 − π ) ) )
12	9 11	negcon1ad	⊢ ( 𝐴 ∈ ℂ → - ( sin ‘ ( 𝐴 − π ) ) = ( sin ‘ 𝐴 ) )
13	6 8 12	3eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( π − 𝐴 ) ) = ( sin ‘ 𝐴 ) )