This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )