# 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 ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )

### Proof

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