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 e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )

Proof

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