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

Metamath Proof Explorer

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 ) ∈ ℝ )