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 A sin A 0 1 + cot A 2 = csc A 2

Proof

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