Metamath Proof Explorer


Theorem sincossq

Description: Sine squared plus cosine squared is 1. Equation 17 of Gleason p. 311. Note that this holds for non-real arguments, even though individually each term is unbounded. (Contributed by NM, 15-Jan-2006)

Ref Expression
Assertion sincossq A sin A 2 + cos A 2 = 1

Proof

Step Hyp Ref Expression
1 negcl A A
2 cosadd A A cos A + A = cos A cos A sin A sin A
3 1 2 mpdan A cos A + A = cos A cos A sin A sin A
4 negid A A + A = 0
5 4 fveq2d A cos A + A = cos 0
6 cos0 cos 0 = 1
7 5 6 eqtrdi A cos A + A = 1
8 sincl A sin A
9 8 sqcld A sin A 2
10 coscl A cos A
11 10 sqcld A cos A 2
12 9 11 addcomd A sin A 2 + cos A 2 = cos A 2 + sin A 2
13 10 sqvald A cos A 2 = cos A cos A
14 cosneg A cos A = cos A
15 14 oveq2d A cos A cos A = cos A cos A
16 13 15 eqtr4d A cos A 2 = cos A cos A
17 8 sqvald A sin A 2 = sin A sin A
18 sinneg A sin A = sin A
19 18 negeqd A sin A = sin A
20 8 negnegd A sin A = sin A
21 19 20 eqtrd A sin A = sin A
22 21 oveq2d A sin A sin A = sin A sin A
23 17 22 eqtr4d A sin A 2 = sin A sin A
24 1 sincld A sin A
25 8 24 mulneg2d A sin A sin A = sin A sin A
26 23 25 eqtrd A sin A 2 = sin A sin A
27 16 26 oveq12d A cos A 2 + sin A 2 = cos A cos A + sin A sin A
28 1 coscld A cos A
29 10 28 mulcld A cos A cos A
30 8 24 mulcld A sin A sin A
31 29 30 negsubd A cos A cos A + sin A sin A = cos A cos A sin A sin A
32 12 27 31 3eqtrrd A cos A cos A sin A sin A = sin A 2 + cos A 2
33 3 7 32 3eqtr3rd A sin A 2 + cos A 2 = 1