Theorem cosmpi

Description: Cosine of a number less _pi . (Contributed by Paul Chapman, 15-Mar-2008)

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

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		cossub	⊢ ( ( 𝐴 ∈ ℂ ∧ π ∈ ℂ ) → ( cos ‘ ( 𝐴 − π ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ π ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ π ) ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 𝐴 − π ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ π ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ π ) ) ) )
4		cospi	⊢ ( cos ‘ π ) = - 1
5	4	oveq2i	⊢ ( ( cos ‘ 𝐴 ) · ( cos ‘ π ) ) = ( ( cos ‘ 𝐴 ) · - 1 )
6		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
7		neg1cn	⊢ - 1 ∈ ℂ
8		mulcom	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · - 1 ) = ( - 1 · ( cos ‘ 𝐴 ) ) )
9	7 8	mpan2	⊢ ( ( cos ‘ 𝐴 ) ∈ ℂ → ( ( cos ‘ 𝐴 ) · - 1 ) = ( - 1 · ( cos ‘ 𝐴 ) ) )
10		mulm1	⊢ ( ( cos ‘ 𝐴 ) ∈ ℂ → ( - 1 · ( cos ‘ 𝐴 ) ) = - ( cos ‘ 𝐴 ) )
11	9 10	eqtrd	⊢ ( ( cos ‘ 𝐴 ) ∈ ℂ → ( ( cos ‘ 𝐴 ) · - 1 ) = - ( cos ‘ 𝐴 ) )
12	6 11	syl	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) · - 1 ) = - ( cos ‘ 𝐴 ) )
13	5 12	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) · ( cos ‘ π ) ) = - ( cos ‘ 𝐴 ) )
14		sinpi	⊢ ( sin ‘ π ) = 0
15	14	oveq2i	⊢ ( ( sin ‘ 𝐴 ) · ( sin ‘ π ) ) = ( ( sin ‘ 𝐴 ) · 0 )
16		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
17	16	mul01d	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) · 0 ) = 0 )
18	15 17	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) · ( sin ‘ π ) ) = 0 )
19	13 18	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ π ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ π ) ) ) = ( - ( cos ‘ 𝐴 ) + 0 ) )
20	6	negcld	⊢ ( 𝐴 ∈ ℂ → - ( cos ‘ 𝐴 ) ∈ ℂ )
21	20	addid1d	⊢ ( 𝐴 ∈ ℂ → ( - ( cos ‘ 𝐴 ) + 0 ) = - ( cos ‘ 𝐴 ) )
22	19 21	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ π ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ π ) ) ) = - ( cos ‘ 𝐴 ) )
23	3 22	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 𝐴 − π ) ) = - ( cos ‘ 𝐴 ) )