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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cotval | |
|
2 | 1 | oveq1d | |
3 | 2 | oveq2d | |
4 | sincossq | |
|
5 | 4 | oveq1d | |
6 | 5 | adantr | |
7 | sincl | |
|
8 | 7 | sqcld | |
9 | 8 | adantr | |
10 | sqne0 | |
|
11 | 7 10 | syl | |
12 | 11 | biimpar | |
13 | 9 12 | dividd | |
14 | 13 | oveq1d | |
15 | coscl | |
|
16 | 15 | sqcld | |
17 | 16 | adantr | |
18 | 9 17 9 12 | divdird | |
19 | 15 7 | jca | |
20 | 2nn0 | |
|
21 | expdiv | |
|
22 | 20 21 | mp3an3 | |
23 | 22 | anassrs | |
24 | 19 23 | sylan | |
25 | 24 | oveq2d | |
26 | 14 18 25 | 3eqtr4rd | |
27 | cscval | |
|
28 | 27 | oveq1d | |
29 | ax-1cn | |
|
30 | expdiv | |
|
31 | 29 20 30 | mp3an13 | |
32 | 7 31 | sylan | |
33 | sq1 | |
|
34 | 33 | oveq1i | |
35 | 32 34 | eqtrdi | |
36 | 28 35 | eqtrd | |
37 | 6 26 36 | 3eqtr4rd | |
38 | 3 37 | eqtr4d | |