Metamath Proof Explorer

Theorem cotsqcscsq

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

Ref Expression
Assertion cotsqcscsq 
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( cot ` A ) ^ 2 ) ) = ( ( csc ` A ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 cotval 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) = ( ( cos ` A ) / ( sin ` A ) ) )
2 1 oveq1d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( cot ` A ) ^ 2 ) = ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) )
3 2 oveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( cot ` A ) ^ 2 ) ) = ( 1 + ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) ) )
4 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
5 4 oveq1d 
 |-  ( A e. CC -> ( ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) / ( ( sin ` A ) ^ 2 ) ) = ( 1 / ( ( sin ` A ) ^ 2 ) ) )
6 5 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) / ( ( sin ` A ) ^ 2 ) ) = ( 1 / ( ( sin ` A ) ^ 2 ) ) )
7 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
8 7 sqcld 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC )
9 8 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( sin ` A ) ^ 2 ) e. CC )
10 sqne0 
 |-  ( ( sin ` A ) e. CC -> ( ( ( sin ` A ) ^ 2 ) =/= 0 <-> ( sin ` A ) =/= 0 ) )
11 7 10 syl 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) =/= 0 <-> ( sin ` A ) =/= 0 ) )
12 11 biimpar 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( sin ` A ) ^ 2 ) =/= 0 )
13 9 12 dividd 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( ( sin ` A ) ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) = 1 )
14 13 oveq1d 
 |-  ( ( A e. CC /\ ( 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 e. CC -> ( cos ` A ) e. CC )
16 15 sqcld 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC )
17 16 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( cos ` A ) ^ 2 ) e. CC )
18 9 17 9 12 divdird 
 |-  ( ( A e. CC /\ ( 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 e. CC -> ( ( cos ` A ) e. CC /\ ( sin ` A ) e. CC ) )
20 2nn0 
 |-  2 e. NN0
21 expdiv 
 |-  ( ( ( cos ` A ) e. CC /\ ( ( sin ` A ) e. CC /\ ( sin ` A ) =/= 0 ) /\ 2 e. NN0 ) -> ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) = ( ( ( cos ` A ) ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) )
22 20 21 mp3an3 
 |-  ( ( ( cos ` A ) e. CC /\ ( ( sin ` A ) e. CC /\ ( sin ` A ) =/= 0 ) ) -> ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) = ( ( ( cos ` A ) ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) )
23 22 anassrs 
 |-  ( ( ( ( cos ` A ) e. CC /\ ( sin ` A ) e. CC ) /\ ( sin ` A ) =/= 0 ) -> ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) = ( ( ( cos ` A ) ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) )
24 19 23 sylan 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) = ( ( ( cos ` A ) ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) )
25 24 oveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) ) = ( 1 + ( ( ( cos ` A ) ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) ) )
26 14 18 25 3eqtr4rd 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) ) = ( ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) / ( ( sin ` A ) ^ 2 ) ) )
27 cscval 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) = ( 1 / ( sin ` A ) ) )
28 27 oveq1d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( csc ` A ) ^ 2 ) = ( ( 1 / ( sin ` A ) ) ^ 2 ) )
29 ax-1cn 
 |-  1 e. CC
30 expdiv 
 |-  ( ( 1 e. CC /\ ( ( sin ` A ) e. CC /\ ( sin ` A ) =/= 0 ) /\ 2 e. NN0 ) -> ( ( 1 / ( sin ` A ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) )
31 29 20 30 mp3an13 
 |-  ( ( ( sin ` A ) e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( 1 / ( sin ` A ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( sin ` A ) ^ 2 ) ) )
32 7 31 sylan 
 |-  ( ( A e. CC /\ ( 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 e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( 1 / ( sin ` A ) ) ^ 2 ) = ( 1 / ( ( sin ` A ) ^ 2 ) ) )
36 28 35 eqtrd 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( csc ` A ) ^ 2 ) = ( 1 / ( ( sin ` A ) ^ 2 ) ) )
37 6 26 36 3eqtr4rd 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( csc ` A ) ^ 2 ) = ( 1 + ( ( ( cos ` A ) / ( sin ` A ) ) ^ 2 ) ) )
38 3 37 eqtr4d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 + ( ( cot ` A ) ^ 2 ) ) = ( ( csc ` A ) ^ 2 ) )