Theorem coshval-named

Description: Value of the named cosh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-cosh . See coshval for a theorem to convert this further. (Contributed by David A. Wheeler, 10-May-2015)

	Ref	Expression
Assertion	coshval-named	$$⊢A\in ℂ\to \cosh \left(A\right)=\cos \mathrm{i}A$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
2	1	fveq2d	$$⊢x=A\to \cos \mathrm{i}x=\cos \mathrm{i}A$$
3		df-cosh	$$⊢\cosh =\left(x\in ℂ⟼\cos \mathrm{i}x\right)$$
4		fvex	$$⊢\cos \mathrm{i}A\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢A\in ℂ\to \cosh \left(A\right)=\cos \mathrm{i}A$$