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