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 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( 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 )