Theorem retanhcl

Description: The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015)

	Ref	Expression
Assertion	retanhcl	⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4	1 2 3	sylancr	⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∈ ℂ )
5		rpcoshcl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ∈ ℝ+ )
6	5	rpne0d	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ≠ 0 )
7		tanval	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( cos ‘ ( i · 𝐴 ) ) ≠ 0 ) → ( tan ‘ ( i · 𝐴 ) ) = ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) )
8	4 6 7	syl2anc	⊢ ( 𝐴 ∈ ℝ → ( tan ‘ ( i · 𝐴 ) ) = ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) )
9	8	oveq1d	⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) / i ) )
10	4	sincld	⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ )
11		recoshcl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ∈ ℝ )
12	11	recnd	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ∈ ℂ )
13	1	a1i	⊢ ( 𝐴 ∈ ℝ → i ∈ ℂ )
14		ine0	⊢ i ≠ 0
15	14	a1i	⊢ ( 𝐴 ∈ ℝ → i ≠ 0 )
16	10 12 13 6 15	divdiv32d	⊢ ( 𝐴 ∈ ℝ → ( ( ( sin ‘ ( i · 𝐴 ) ) / ( cos ‘ ( i · 𝐴 ) ) ) / i ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / i ) / ( cos ‘ ( i · 𝐴 ) ) ) )
17	9 16	eqtrd	⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( ( ( sin ‘ ( i · 𝐴 ) ) / i ) / ( cos ‘ ( i · 𝐴 ) ) ) )
18		resinhcl	⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ )
19	18 5	rerpdivcld	⊢ ( 𝐴 ∈ ℝ → ( ( ( sin ‘ ( i · 𝐴 ) ) / i ) / ( cos ‘ ( i · 𝐴 ) ) ) ∈ ℝ )
20	17 19	eqeltrd	⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ )