Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 recn 
 |-  ( A e. RR -> A e. CC )
3 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4 1 2 3 sylancr 
 |-  ( A e. RR -> ( _i x. A ) e. CC )
5 rpcoshcl 
 |-  ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR+ )
6 5 rpne0d 
 |-  ( A e. RR -> ( cos ` ( _i x. A ) ) =/= 0 )
7 tanval 
 |-  ( ( ( _i x. A ) e. CC /\ ( cos ` ( _i x. A ) ) =/= 0 ) -> ( tan ` ( _i x. A ) ) = ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) )
8 4 6 7 syl2anc 
 |-  ( A e. RR -> ( tan ` ( _i x. A ) ) = ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) )
9 8 oveq1d 
 |-  ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) )
10 4 sincld 
 |-  ( A e. RR -> ( sin ` ( _i x. A ) ) e. CC )
11 recoshcl 
 |-  ( A e. RR -> ( cos ` ( _i x. A ) ) e. RR )
12 11 recnd 
 |-  ( A e. RR -> ( cos ` ( _i x. A ) ) e. CC )
13 1 a1i 
 |-  ( A e. RR -> _i e. CC )
14 ine0 
 |-  _i =/= 0
15 14 a1i 
 |-  ( A e. RR -> _i =/= 0 )
16 10 12 13 6 15 divdiv32d 
 |-  ( A e. RR -> ( ( ( sin ` ( _i x. A ) ) / ( cos ` ( _i x. A ) ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) )
17 sinhval 
 |-  ( A e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
18 2 17 syl 
 |-  ( A e. RR -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
19 coshval 
 |-  ( A e. CC -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )
20 2 19 syl 
 |-  ( A e. RR -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )
21 18 20 oveq12d 
 |-  ( A e. RR -> ( ( ( sin ` ( _i x. A ) ) / _i ) / ( cos ` ( _i x. A ) ) ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) / ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
22 9 16 21 3eqtrd 
 |-  ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) / ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
23 reefcl 
 |-  ( A e. RR -> ( exp ` A ) e. RR )
24 renegcl 
 |-  ( A e. RR -> -u A e. RR )
25 24 reefcld 
 |-  ( A e. RR -> ( exp ` -u A ) e. RR )
26 23 25 resubcld 
 |-  ( A e. RR -> ( ( exp ` A ) - ( exp ` -u A ) ) e. RR )
27 26 recnd 
 |-  ( A e. RR -> ( ( exp ` A ) - ( exp ` -u A ) ) e. CC )
28 23 25 readdcld 
 |-  ( A e. RR -> ( ( exp ` A ) + ( exp ` -u A ) ) e. RR )
29 28 recnd 
 |-  ( A e. RR -> ( ( exp ` A ) + ( exp ` -u A ) ) e. CC )
30 2cnd 
 |-  ( A e. RR -> 2 e. CC )
31 20 6 eqnetrrd 
 |-  ( A e. RR -> ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) =/= 0 )
32 2ne0 
 |-  2 =/= 0
33 32 a1i 
 |-  ( A e. RR -> 2 =/= 0 )
34 29 30 33 divne0bd 
 |-  ( A e. RR -> ( ( ( exp ` A ) + ( exp ` -u A ) ) =/= 0 <-> ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) =/= 0 ) )
35 31 34 mpbird 
 |-  ( A e. RR -> ( ( exp ` A ) + ( exp ` -u A ) ) =/= 0 )
36 27 29 30 35 33 divcan7d 
 |-  ( A e. RR -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) / ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / ( ( exp ` A ) + ( exp ` -u A ) ) ) )
37 22 36 eqtrd 
 |-  ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / ( ( exp ` A ) + ( exp ` -u A ) ) ) )
38 24 rpefcld 
 |-  ( A e. RR -> ( exp ` -u A ) e. RR+ )
39 23 38 ltsubrpd 
 |-  ( A e. RR -> ( ( exp ` A ) - ( exp ` -u A ) ) < ( exp ` A ) )
40 23 38 ltaddrpd 
 |-  ( A e. RR -> ( exp ` A ) < ( ( exp ` A ) + ( exp ` -u A ) ) )
41 26 23 28 39 40 lttrd 
 |-  ( A e. RR -> ( ( exp ` A ) - ( exp ` -u A ) ) < ( ( exp ` A ) + ( exp ` -u A ) ) )
42 29 mulridd 
 |-  ( A e. RR -> ( ( ( exp ` A ) + ( exp ` -u A ) ) x. 1 ) = ( ( exp ` A ) + ( exp ` -u A ) ) )
43 41 42 breqtrrd 
 |-  ( A e. RR -> ( ( exp ` A ) - ( exp ` -u A ) ) < ( ( ( exp ` A ) + ( exp ` -u A ) ) x. 1 ) )
44 1red 
 |-  ( A e. RR -> 1 e. RR )
45 efgt0 
 |-  ( A e. RR -> 0 < ( exp ` A ) )
46 efgt0 
 |-  ( -u A e. RR -> 0 < ( exp ` -u A ) )
47 24 46 syl 
 |-  ( A e. RR -> 0 < ( exp ` -u A ) )
48 23 25 45 47 addgt0d 
 |-  ( A e. RR -> 0 < ( ( exp ` A ) + ( exp ` -u A ) ) )
49 ltdivmul 
 |-  ( ( ( ( exp ` A ) - ( exp ` -u A ) ) e. RR /\ 1 e. RR /\ ( ( ( exp ` A ) + ( exp ` -u A ) ) e. RR /\ 0 < ( ( exp ` A ) + ( exp ` -u A ) ) ) ) -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / ( ( exp ` A ) + ( exp ` -u A ) ) ) < 1 <-> ( ( exp ` A ) - ( exp ` -u A ) ) < ( ( ( exp ` A ) + ( exp ` -u A ) ) x. 1 ) ) )
50 26 44 28 48 49 syl112anc 
 |-  ( A e. RR -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / ( ( exp ` A ) + ( exp ` -u A ) ) ) < 1 <-> ( ( exp ` A ) - ( exp ` -u A ) ) < ( ( ( exp ` A ) + ( exp ` -u A ) ) x. 1 ) ) )
51 43 50 mpbird 
 |-  ( A e. RR -> ( ( ( exp ` A ) - ( exp ` -u A ) ) / ( ( exp ` A ) + ( exp ` -u A ) ) ) < 1 )
52 37 51 eqbrtrd 
 |-  ( A e. RR -> ( ( tan ` ( _i x. A ) ) / _i ) < 1 )