Metamath Proof Explorer


Theorem cosppi

Description: Cosine of a number plus _pi . (Contributed by NM, 18-Aug-2008)

Ref Expression
Assertion cosppi A cos A + π = cos A

Proof

Step Hyp Ref Expression
1 picn π
2 cosadd A π cos A + π = cos A cos π sin A sin π
3 1 2 mpan2 A cos A + π = cos A cos π sin A sin π
4 cospi cos π = 1
5 4 oveq2i cos A cos π = cos A -1
6 coscl A cos A
7 neg1cn 1
8 mulcom cos A 1 cos A -1 = -1 cos A
9 7 8 mpan2 cos A cos A -1 = -1 cos A
10 mulm1 cos A -1 cos A = cos A
11 9 10 eqtrd cos A cos A -1 = cos A
12 6 11 syl A cos A -1 = cos A
13 5 12 syl5eq A cos A cos π = cos A
14 sinpi sin π = 0
15 14 oveq2i sin A sin π = sin A 0
16 sincl A sin A
17 16 mul01d A sin A 0 = 0
18 15 17 syl5eq A sin A sin π = 0
19 13 18 oveq12d A cos A cos π sin A sin π = - cos A - 0
20 6 negcld A cos A
21 20 subid1d A - cos A - 0 = cos A
22 19 21 eqtrd A cos A cos π sin A sin π = cos A
23 3 22 eqtrd A cos A + π = cos A