Theorem tanhval-named

Description: Value of the named tanh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-tanh . (Contributed by David A. Wheeler, 10-May-2015)

	Ref	Expression
Assertion	tanhval-named	$$⊢A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \tanh \left(A\right)=\frac{\tan \mathrm{i}A}{\mathrm{i}}$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
2	1	fveq2d	$$⊢x=A\to \tan \mathrm{i}x=\tan \mathrm{i}A$$
3	2	oveq1d	$$⊢x=A\to \frac{\tan \mathrm{i}x}{\mathrm{i}}=\frac{\tan \mathrm{i}A}{\mathrm{i}}$$
4		df-tanh	$$⊢\tanh =\left(x\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\tan \mathrm{i}x}{\mathrm{i}}\right)$$
5		ovex	$$⊢\frac{\tan \mathrm{i}A}{\mathrm{i}}\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in {\cosh }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \tanh \left(A\right)=\frac{\tan \mathrm{i}A}{\mathrm{i}}$$