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

Metamath Proof Explorer

Theorem resinhcl

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

Ref Expression
Assertion resinhcl ( 𝐴 ∈ ℝ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 sinhval ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) )
4 reefcl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ )
5 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
6 5 reefcld ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ - 𝐴 ) ∈ ℝ )
7 4 6 resubcld ⊢ ( 𝐴 ∈ ℝ → ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) ∈ ℝ )
8 7 rehalfcld ⊢ ( 𝐴 ∈ ℝ → ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) ∈ ℝ )
9 3 8 eqeltrd ⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ )