This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tanval

Description: Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
2 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
3 2 anim1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) )
4 eldifsn ⊢ ( ( cos ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) )
5 3 4 sylibr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) )
6 cosf ⊢ cos : ℂ ⟶ ℂ
7 ffn ⊢ ( cos : ℂ ⟶ ℂ → cos Fn ℂ )
8 elpreima ⊢ ( cos Fn ℂ → ( 𝐴 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
9 6 7 8 mp2b ⊢ ( 𝐴 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) )
10 1 5 9 sylanbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) )
11 fveq2 ⊢ ( 𝑥 = 𝐴 → ( sin ‘ 𝑥 ) = ( sin ‘ 𝐴 ) )
12 fveq2 ⊢ ( 𝑥 = 𝐴 → ( cos ‘ 𝑥 ) = ( cos ‘ 𝐴 ) )
13 11 12 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
14 df-tan ⊢ tan = ( 𝑥 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
15 ovex ⊢ ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ∈ V
16 13 14 15 fvmpt ⊢ ( 𝐴 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
17 10 16 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )