Description: The hyperbolic cosine of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | recoshcl | |- ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpcoshcl | |- ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR+ ) |
|
2 | 1 | rpred | |- ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR ) |