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 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 ) )