Theorem tanhbnd

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

	Ref	Expression
Assertion	tanhbnd	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}\in \left(-1,1\right)$$

Proof

Step	Hyp	Ref	Expression
1		retanhcl	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}\in ℝ$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		recn	$$⊢A\in ℝ\to A\in ℂ$$
4		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
5	2 3 4	sylancr	$$⊢A\in ℝ\to \mathrm{i}A\in ℂ$$
6		rpcoshcl	$$⊢A\in ℝ\to \cos \mathrm{i}A\in {ℝ}^{+}$$
7	6	rpne0d	$$⊢A\in ℝ\to \cos \mathrm{i}A\ne 0$$
8	5 7	tancld	$$⊢A\in ℝ\to \tan \mathrm{i}A\in ℂ$$
9	2	a1i	$$⊢A\in ℝ\to \mathrm{i}\in ℂ$$
10		ine0	$$⊢\mathrm{i}\ne 0$$
11	10	a1i	$$⊢A\in ℝ\to \mathrm{i}\ne 0$$
12	8 9 11	divnegd	$$⊢A\in ℝ\to -\frac{\tan \mathrm{i}A}{\mathrm{i}}=\frac{-\tan \mathrm{i}A}{\mathrm{i}}$$
13		mulneg2	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
14	2 3 13	sylancr	$$⊢A\in ℝ\to \mathrm{i}\left(-A\right)=-\mathrm{i}A$$
15	14	fveq2d	$$⊢A\in ℝ\to \tan \mathrm{i}\left(-A\right)=\tan \left(-\mathrm{i}A\right)$$
16		tanneg	$$⊢\left(\mathrm{i}A\in ℂ\wedge \cos \mathrm{i}A\ne 0\right)\to \tan \left(-\mathrm{i}A\right)=-\tan \mathrm{i}A$$
17	5 7 16	syl2anc	$$⊢A\in ℝ\to \tan \left(-\mathrm{i}A\right)=-\tan \mathrm{i}A$$
18	15 17	eqtrd	$$⊢A\in ℝ\to \tan \mathrm{i}\left(-A\right)=-\tan \mathrm{i}A$$
19	18	oveq1d	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}\left(-A\right)}{\mathrm{i}}=\frac{-\tan \mathrm{i}A}{\mathrm{i}}$$
20	12 19	eqtr4d	$$⊢A\in ℝ\to -\frac{\tan \mathrm{i}A}{\mathrm{i}}=\frac{\tan \mathrm{i}\left(-A\right)}{\mathrm{i}}$$
21		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
22		tanhlt1	$$⊢-A\in ℝ\to \frac{\tan \mathrm{i}\left(-A\right)}{\mathrm{i}}<1$$
23	21 22	syl	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}\left(-A\right)}{\mathrm{i}}<1$$
24	20 23	eqbrtrd	$$⊢A\in ℝ\to -\frac{\tan \mathrm{i}A}{\mathrm{i}}<1$$
25		1re	$$⊢1\in ℝ$$
26		ltnegcon1	$$⊢\left(\frac{\tan \mathrm{i}A}{\mathrm{i}}\in ℝ\wedge 1\in ℝ\right)\to \left(-\frac{\tan \mathrm{i}A}{\mathrm{i}}<1\leftrightarrow -1<\frac{\tan \mathrm{i}A}{\mathrm{i}}\right)$$
27	1 25 26	sylancl	$$⊢A\in ℝ\to \left(-\frac{\tan \mathrm{i}A}{\mathrm{i}}<1\leftrightarrow -1<\frac{\tan \mathrm{i}A}{\mathrm{i}}\right)$$
28	24 27	mpbid	$$⊢A\in ℝ\to -1<\frac{\tan \mathrm{i}A}{\mathrm{i}}$$
29		tanhlt1	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}<1$$
30		neg1rr	$$⊢-1\in ℝ$$
31	30	rexri	$$⊢-1\in {ℝ}^{*}$$
32	25	rexri	$$⊢1\in {ℝ}^{*}$$
33		elioo2	$$⊢\left(-1\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to \left(\frac{\tan \mathrm{i}A}{\mathrm{i}}\in \left(-1,1\right)\leftrightarrow \left(\frac{\tan \mathrm{i}A}{\mathrm{i}}\in ℝ\wedge -1<\frac{\tan \mathrm{i}A}{\mathrm{i}}\wedge \frac{\tan \mathrm{i}A}{\mathrm{i}}<1\right)\right)$$
34	31 32 33	mp2an	$$⊢\frac{\tan \mathrm{i}A}{\mathrm{i}}\in \left(-1,1\right)\leftrightarrow \left(\frac{\tan \mathrm{i}A}{\mathrm{i}}\in ℝ\wedge -1<\frac{\tan \mathrm{i}A}{\mathrm{i}}\wedge \frac{\tan \mathrm{i}A}{\mathrm{i}}<1\right)$$
35	1 28 29 34	syl3anbrc	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}\in \left(-1,1\right)$$