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