Description: The closure of the sinh function with complex argument. (Contributed by Jon Pennant, 9-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sinhcl | |- ( A e. CC -> ( sinh ` A ) e. CC ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sinhf | |- sinh : CC --> CC |
|
| 2 | 1 | ffvelcdmi | |- ( A e. CC -> ( sinh ` A ) e. CC ) |