resinhcl

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

		Ref	Expression
	Assertion	resinhcl	$⊢ A \in ℝ \to \frac{\sin i A}{i} \in ℝ$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		sinhval	$⊢ A \in ℂ \to \frac{\sin i A}{i} = \frac{e^{A} - e^{- A}}{2}$
3	1 2	syl	$⊢ A \in ℝ \to \frac{\sin i A}{i} = \frac{e^{A} - e^{- A}}{2}$
4		reefcl	$⊢ A \in ℝ \to e^{A} \in ℝ$
5		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
6	5	reefcld	$⊢ A \in ℝ \to e^{- A} \in ℝ$
7	4 6	resubcld	$⊢ A \in ℝ \to e^{A} - e^{- A} \in ℝ$
8	7	rehalfcld	$⊢ A \in ℝ \to \frac{e^{A} - e^{- A}}{2} \in ℝ$
9	3 8	eqeltrd	$⊢ A \in ℝ \to \frac{\sin i A}{i} \in ℝ$

Metamath Proof Explorer