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 e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) e. ( -u 1 (,) 1 ) )

Proof

Step	Hyp	Ref	Expression
1		retanhcl	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) e. RR )
2		ax-icn	|- _i e. CC
3		recn	|- ( A e. RR -> A e. CC )
4		mulcl	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
5	2 3 4	sylancr	|- ( A e. RR -> ( _i x. A ) e. CC )
6		rpcoshcl	|- ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR+ )
7	6	rpne0d	|- ( A e. RR -> ( cos ` ( _i x. A ) ) =/= 0 )
8	5 7	tancld	|- ( A e. RR -> ( tan ` ( _i x. A ) ) e. CC )
9	2	a1i	|- ( A e. RR -> _i e. CC )
10		ine0	|- _i =/= 0
11	10	a1i	|- ( A e. RR -> _i =/= 0 )
12	8 9 11	divnegd	|- ( A e. RR -> -u ( ( tan ` ( _i x. A ) ) / _i ) = ( -u ( tan ` ( _i x. A ) ) / _i ) )
13		mulneg2	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
14	2 3 13	sylancr	|- ( A e. RR -> ( _i x. -u A ) = -u ( _i x. A ) )
15	14	fveq2d	|- ( A e. RR -> ( tan ` ( _i x. -u A ) ) = ( tan ` -u ( _i x. A ) ) )
16		tanneg	|- ( ( ( _i x. A ) e. CC /\ ( cos ` ( _i x. A ) ) =/= 0 ) -> ( tan ` -u ( _i x. A ) ) = -u ( tan ` ( _i x. A ) ) )
17	5 7 16	syl2anc	|- ( A e. RR -> ( tan ` -u ( _i x. A ) ) = -u ( tan ` ( _i x. A ) ) )
18	15 17	eqtrd	|- ( A e. RR -> ( tan ` ( _i x. -u A ) ) = -u ( tan ` ( _i x. A ) ) )
19	18	oveq1d	|- ( A e. RR -> ( ( tan ` ( _i x. -u A ) ) / _i ) = ( -u ( tan ` ( _i x. A ) ) / _i ) )
20	12 19	eqtr4d	|- ( A e. RR -> -u ( ( tan ` ( _i x. A ) ) / _i ) = ( ( tan ` ( _i x. -u A ) ) / _i ) )
21		renegcl	|- ( A e. RR -> -u A e. RR )
22		tanhlt1	|- ( -u A e. RR -> ( ( tan ` ( _i x. -u A ) ) / _i ) < 1 )
23	21 22	syl	|- ( A e. RR -> ( ( tan ` ( _i x. -u A ) ) / _i ) < 1 )
24	20 23	eqbrtrd	|- ( A e. RR -> -u ( ( tan ` ( _i x. A ) ) / _i ) < 1 )
25		1re	|- 1 e. RR
26		ltnegcon1	|- ( ( ( ( tan ` ( _i x. A ) ) / _i ) e. RR /\ 1 e. RR ) -> ( -u ( ( tan ` ( _i x. A ) ) / _i ) < 1 <-> -u 1 < ( ( tan ` ( _i x. A ) ) / _i ) ) )
27	1 25 26	sylancl	|- ( A e. RR -> ( -u ( ( tan ` ( _i x. A ) ) / _i ) < 1 <-> -u 1 < ( ( tan ` ( _i x. A ) ) / _i ) ) )
28	24 27	mpbid	|- ( A e. RR -> -u 1 < ( ( tan ` ( _i x. A ) ) / _i ) )
29		tanhlt1	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) < 1 )
30		neg1rr	|- -u 1 e. RR
31	30	rexri	|- -u 1 e. RR*
32	25	rexri	|- 1 e. RR*
33		elioo2	|- ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( ( ( tan ` ( _i x. A ) ) / _i ) e. ( -u 1 (,) 1 ) <-> ( ( ( tan ` ( _i x. A ) ) / _i ) e. RR /\ -u 1 < ( ( tan ` ( _i x. A ) ) / _i ) /\ ( ( tan ` ( _i x. A ) ) / _i ) < 1 ) ) )
34	31 32 33	mp2an	|- ( ( ( tan ` ( _i x. A ) ) / _i ) e. ( -u 1 (,) 1 ) <-> ( ( ( tan ` ( _i x. A ) ) / _i ) e. RR /\ -u 1 < ( ( tan ` ( _i x. A ) ) / _i ) /\ ( ( tan ` ( _i x. A ) ) / _i ) < 1 ) )
35	1 28 29 34	syl3anbrc	|- ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) e. ( -u 1 (,) 1 ) )