Metamath Proof Explorer


Theorem rpcoshcl

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

Ref Expression
Assertion rpcoshcl AcosiA+

Proof

Step Hyp Ref Expression
1 recn AA
2 coshval AcosiA=eA+eA2
3 1 2 syl AcosiA=eA+eA2
4 rpefcl AeA+
5 renegcl AA
6 5 rpefcld AeA+
7 4 6 rpaddcld AeA+eA+
8 7 rphalfcld AeA+eA2+
9 3 8 eqeltrd AcosiA+