Theorem retanhcl

Description: The hyperbolic tangent of a real number is real. (Contributed by Mario Carneiro, 4-Apr-2015)

	Ref	Expression
Assertion	retanhcl	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		recn	$$⊢A\in ℝ\to A\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
4	1 2 3	sylancr	$$⊢A\in ℝ\to \mathrm{i}A\in ℂ$$
5		rpcoshcl	$$⊢A\in ℝ\to \cos \mathrm{i}A\in {ℝ}^{+}$$
6	5	rpne0d	$$⊢A\in ℝ\to \cos \mathrm{i}A\ne 0$$
7		tanval	$$⊢\left(\mathrm{i}A\in ℂ\wedge \cos \mathrm{i}A\ne 0\right)\to \tan \mathrm{i}A=\frac{\sin \mathrm{i}A}{\cos \mathrm{i}A}$$
8	4 6 7	syl2anc	$$⊢A\in ℝ\to \tan \mathrm{i}A=\frac{\sin \mathrm{i}A}{\cos \mathrm{i}A}$$
9	8	oveq1d	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}=\frac{\frac{\sin \mathrm{i}A}{\cos \mathrm{i}A}}{\mathrm{i}}$$
10	4	sincld	$$⊢A\in ℝ\to \sin \mathrm{i}A\in ℂ$$
11		recoshcl	$$⊢A\in ℝ\to \cos \mathrm{i}A\in ℝ$$
12	11	recnd	$$⊢A\in ℝ\to \cos \mathrm{i}A\in ℂ$$
13	1	a1i	$$⊢A\in ℝ\to \mathrm{i}\in ℂ$$
14		ine0	$$⊢\mathrm{i}\ne 0$$
15	14	a1i	$$⊢A\in ℝ\to \mathrm{i}\ne 0$$
16	10 12 13 6 15	divdiv32d	$$⊢A\in ℝ\to \frac{\frac{\sin \mathrm{i}A}{\cos \mathrm{i}A}}{\mathrm{i}}=\frac{\frac{\sin \mathrm{i}A}{\mathrm{i}}}{\cos \mathrm{i}A}$$
17	9 16	eqtrd	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}=\frac{\frac{\sin \mathrm{i}A}{\mathrm{i}}}{\cos \mathrm{i}A}$$
18		resinhcl	$$⊢A\in ℝ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}\in ℝ$$
19	18 5	rerpdivcld	$$⊢A\in ℝ\to \frac{\frac{\sin \mathrm{i}A}{\mathrm{i}}}{\cos \mathrm{i}A}\in ℝ$$
20	17 19	eqeltrd	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}\in ℝ$$