Theorem tanhlt1

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

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

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		sinhval	$$⊢A\in ℂ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}$$
18	2 17	syl	$$⊢A\in ℝ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}$$
19		coshval	$$⊢A\in ℂ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$
20	2 19	syl	$$⊢A\in ℝ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$
21	18 20	oveq12d	$$⊢A\in ℝ\to \frac{\frac{\sin \mathrm{i}A}{\mathrm{i}}}{\cos \mathrm{i}A}=\frac{\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}}{\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}}$$
22	9 16 21	3eqtrd	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}=\frac{\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}}{\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}}$$
23		reefcl	$$⊢A\in ℝ\to {\mathrm{e}}^A\in ℝ$$
24		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
25	24	reefcld	$$⊢A\in ℝ\to {\mathrm{e}}^{-A}\in ℝ$$
26	23 25	resubcld	$$⊢A\in ℝ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}\in ℝ$$
27	26	recnd	$$⊢A\in ℝ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}\in ℂ$$
28	23 25	readdcld	$$⊢A\in ℝ\to {\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℝ$$
29	28	recnd	$$⊢A\in ℝ\to {\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℂ$$
30		2cnd	$$⊢A\in ℝ\to 2\in ℂ$$
31	20 6	eqnetrrd	$$⊢A\in ℝ\to \frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\ne 0$$
32		2ne0	$$⊢2\ne 0$$
33	32	a1i	$$⊢A\in ℝ\to 2\ne 0$$
34	29 30 33	divne0bd	$$⊢A\in ℝ\to \left({\mathrm{e}}^A+{\mathrm{e}}^{-A}\ne 0\leftrightarrow \frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\ne 0\right)$$
35	31 34	mpbird	$$⊢A\in ℝ\to {\mathrm{e}}^A+{\mathrm{e}}^{-A}\ne 0$$
36	27 29 30 35 33	divcan7d	$$⊢A\in ℝ\to \frac{\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}}{\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}}=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}$$
37	22 36	eqtrd	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}$$
38	24	rpefcld	$$⊢A\in ℝ\to {\mathrm{e}}^{-A}\in {ℝ}^{+}$$
39	23 38	ltsubrpd	$$⊢A\in ℝ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}<{\mathrm{e}}^A$$
40	23 38	ltaddrpd	$$⊢A\in ℝ\to {\mathrm{e}}^A<{\mathrm{e}}^A+{\mathrm{e}}^{-A}$$
41	26 23 28 39 40	lttrd	$$⊢A\in ℝ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}<{\mathrm{e}}^A+{\mathrm{e}}^{-A}$$
42	29	mulid1d	$$⊢A\in ℝ\to \left({\mathrm{e}}^A+{\mathrm{e}}^{-A}\right)\cdot 1={\mathrm{e}}^A+{\mathrm{e}}^{-A}$$
43	41 42	breqtrrd	$$⊢A\in ℝ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}<\left({\mathrm{e}}^A+{\mathrm{e}}^{-A}\right)\cdot 1$$
44		1red	$$⊢A\in ℝ\to 1\in ℝ$$
45		efgt0	$$⊢A\in ℝ\to 0<{\mathrm{e}}^A$$
46		efgt0	$$⊢-A\in ℝ\to 0<{\mathrm{e}}^{-A}$$
47	24 46	syl	$$⊢A\in ℝ\to 0<{\mathrm{e}}^{-A}$$
48	23 25 45 47	addgt0d	$$⊢A\in ℝ\to 0<{\mathrm{e}}^A+{\mathrm{e}}^{-A}$$
49		ltdivmul	$$⊢\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\in ℝ\wedge 1\in ℝ\wedge \left({\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℝ\wedge 0<{\mathrm{e}}^A+{\mathrm{e}}^{-A}\right)\right)\to \left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}<1\leftrightarrow {\mathrm{e}}^A-{\mathrm{e}}^{-A}<\left({\mathrm{e}}^A+{\mathrm{e}}^{-A}\right)\cdot 1\right)$$
50	26 44 28 48 49	syl112anc	$$⊢A\in ℝ\to \left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}<1\leftrightarrow {\mathrm{e}}^A-{\mathrm{e}}^{-A}<\left({\mathrm{e}}^A+{\mathrm{e}}^{-A}\right)\cdot 1\right)$$
51	43 50	mpbird	$$⊢A\in ℝ\to \frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}<1$$
52	37 51	eqbrtrd	$$⊢A\in ℝ\to \frac{\tan \mathrm{i}A}{\mathrm{i}}<1$$