Metamath Proof Explorer


Theorem cotval

Description: Value of the cotangent function. (Contributed by David A. Wheeler, 14-Mar-2014)

Ref Expression
Assertion cotval ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑦 = 𝐴 → ( sin ‘ 𝑦 ) = ( sin ‘ 𝐴 ) )
2 1 neeq1d ( 𝑦 = 𝐴 → ( ( sin ‘ 𝑦 ) ≠ 0 ↔ ( sin ‘ 𝐴 ) ≠ 0 ) )
3 2 elrab ( 𝐴 ∈ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 } ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) )
4 fveq2 ( 𝑥 = 𝐴 → ( cos ‘ 𝑥 ) = ( cos ‘ 𝐴 ) )
5 fveq2 ( 𝑥 = 𝐴 → ( sin ‘ 𝑥 ) = ( sin ‘ 𝐴 ) )
6 4 5 oveq12d ( 𝑥 = 𝐴 → ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
7 df-cot cot = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 } ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) )
8 ovex ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ∈ V
9 6 7 8 fvmpt ( 𝐴 ∈ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 } → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
10 3 9 sylbir ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )