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\in ℂ\to {\sin A}^2+{\cos A}^2=1$$

Proof

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