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 ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( ( cot ‘ 𝐴 ) ↑ 2 ) ) = ( ( csc ‘ 𝐴 ) ↑ 2 ) )

Proof

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