Metamath Proof Explorer


Theorem cotsqcscsq

Description: Prove the tangent squared cosecant squared identity ( 1 + ( ( cot A ) ^ 2 ) ) = ( ( csc A ) ^ 2 ) ) . (Contributed by David A. Wheeler, 27-May-2015)

Ref Expression
Assertion cotsqcscsq AsinA01+cotA2=cscA2

Proof

Step Hyp Ref Expression
1 cotval AsinA0cotA=cosAsinA
2 1 oveq1d AsinA0cotA2=cosAsinA2
3 2 oveq2d AsinA01+cotA2=1+cosAsinA2
4 sincossq AsinA2+cosA2=1
5 4 oveq1d AsinA2+cosA2sinA2=1sinA2
6 5 adantr AsinA0sinA2+cosA2sinA2=1sinA2
7 sincl AsinA
8 7 sqcld AsinA2
9 8 adantr AsinA0sinA2
10 sqne0 sinAsinA20sinA0
11 7 10 syl AsinA20sinA0
12 11 biimpar AsinA0sinA20
13 9 12 dividd AsinA0sinA2sinA2=1
14 13 oveq1d AsinA0sinA2sinA2+cosA2sinA2=1+cosA2sinA2
15 coscl AcosA
16 15 sqcld AcosA2
17 16 adantr AsinA0cosA2
18 9 17 9 12 divdird AsinA0sinA2+cosA2sinA2=sinA2sinA2+cosA2sinA2
19 15 7 jca AcosAsinA
20 2nn0 20
21 expdiv cosAsinAsinA020cosAsinA2=cosA2sinA2
22 20 21 mp3an3 cosAsinAsinA0cosAsinA2=cosA2sinA2
23 22 anassrs cosAsinAsinA0cosAsinA2=cosA2sinA2
24 19 23 sylan AsinA0cosAsinA2=cosA2sinA2
25 24 oveq2d AsinA01+cosAsinA2=1+cosA2sinA2
26 14 18 25 3eqtr4rd AsinA01+cosAsinA2=sinA2+cosA2sinA2
27 cscval AsinA0cscA=1sinA
28 27 oveq1d AsinA0cscA2=1sinA2
29 ax-1cn 1
30 expdiv 1sinAsinA0201sinA2=12sinA2
31 29 20 30 mp3an13 sinAsinA01sinA2=12sinA2
32 7 31 sylan AsinA01sinA2=12sinA2
33 sq1 12=1
34 33 oveq1i 12sinA2=1sinA2
35 32 34 eqtrdi AsinA01sinA2=1sinA2
36 28 35 eqtrd AsinA0cscA2=1sinA2
37 6 26 36 3eqtr4rd AsinA0cscA2=1+cosAsinA2
38 3 37 eqtr4d AsinA01+cotA2=cscA2