Theorem recoshcl

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

	Ref	Expression
Assertion	recoshcl	$$⊢A\in ℝ\to \cos \mathrm{i}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rpcoshcl	$$⊢A\in ℝ\to \cos \mathrm{i}A\in {ℝ}^{+}$$
2	1	rpred	$$⊢A\in ℝ\to \cos \mathrm{i}A\in ℝ$$