Description: The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | rpcoshcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn | |
|
2 | coshval | |
|
3 | 1 2 | syl | |
4 | rpefcl | |
|
5 | renegcl | |
|
6 | 5 | rpefcld | |
7 | 4 6 | rpaddcld | |
8 | 7 | rphalfcld | |
9 | 3 8 | eqeltrd | |