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 )