Theorem cospim

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

	Ref	Expression
Assertion	cospim	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( π − 𝐴 ) ) = - ( cos ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
2		picn	⊢ π ∈ ℂ
3	2	a1i	⊢ ( 𝐴 ∈ ℂ → π ∈ ℂ )
4	1 3	subcld	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − π ) ∈ ℂ )
5		cosneg	⊢ ( ( 𝐴 − π ) ∈ ℂ → ( cos ‘ - ( 𝐴 − π ) ) = ( cos ‘ ( 𝐴 − π ) ) )
6	4 5	syl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - ( 𝐴 − π ) ) = ( cos ‘ ( 𝐴 − π ) ) )
7	1 3	negsubdi2d	⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 − π ) = ( π − 𝐴 ) )
8	7	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - ( 𝐴 − π ) ) = ( cos ‘ ( π − 𝐴 ) ) )
9		cosmpi	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 𝐴 − π ) ) = - ( cos ‘ 𝐴 ) )
10	6 8 9	3eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( π − 𝐴 ) ) = - ( cos ‘ 𝐴 ) )