rpcoshcl

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

		Ref	Expression
	Assertion	rpcoshcl	$⊢ A \in ℝ \to \cos i A \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		coshval	$⊢ A \in ℂ \to \cos i A = \frac{e^{A} + e^{- A}}{2}$
3	1 2	syl	$⊢ A \in ℝ \to \cos i A = \frac{e^{A} + e^{- A}}{2}$
4		rpefcl	$⊢ A \in ℝ \to e^{A} \in ℝ^{+}$
5		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
6	5	rpefcld	$⊢ A \in ℝ \to e^{- A} \in ℝ^{+}$
7	4 6	rpaddcld	$⊢ A \in ℝ \to e^{A} + e^{- A} \in ℝ^{+}$
8	7	rphalfcld	$⊢ A \in ℝ \to \frac{e^{A} + e^{- A}}{2} \in ℝ^{+}$
9	3 8	eqeltrd	$⊢ A \in ℝ \to \cos i A \in ℝ^{+}$

Metamath Proof Explorer