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 ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ( - 1 (,) 1 ) )

Proof

Step Hyp Ref Expression
1 retanhcl ⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ )
2 ax-icn ⊢ i ∈ ℂ
3 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
5 2 3 4 sylancr ⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∈ ℂ )
6 rpcoshcl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ∈ ℝ+ )
7 6 rpne0d ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ≠ 0 )
8 5 7 tancld ⊢ ( 𝐴 ∈ ℝ → ( tan ‘ ( i · 𝐴 ) ) ∈ ℂ )
9 2 a1i ⊢ ( 𝐴 ∈ ℝ → i ∈ ℂ )
10 ine0 ⊢ i ≠ 0
11 10 a1i ⊢ ( 𝐴 ∈ ℝ → i ≠ 0 )
12 8 9 11 divnegd ⊢ ( 𝐴 ∈ ℝ → - ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( - ( tan ‘ ( i · 𝐴 ) ) / i ) )
13 mulneg2 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
14 2 3 13 sylancr ⊢ ( 𝐴 ∈ ℝ → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
15 14 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( tan ‘ ( i · - 𝐴 ) ) = ( tan ‘ - ( i · 𝐴 ) ) )
16 tanneg ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( cos ‘ ( i · 𝐴 ) ) ≠ 0 ) → ( tan ‘ - ( i · 𝐴 ) ) = - ( tan ‘ ( i · 𝐴 ) ) )
17 5 7 16 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( tan ‘ - ( i · 𝐴 ) ) = - ( tan ‘ ( i · 𝐴 ) ) )
18 15 17 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( tan ‘ ( i · - 𝐴 ) ) = - ( tan ‘ ( i · 𝐴 ) ) )
19 18 oveq1d ⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · - 𝐴 ) ) / i ) = ( - ( tan ‘ ( i · 𝐴 ) ) / i ) )
20 12 19 eqtr4d ⊢ ( 𝐴 ∈ ℝ → - ( ( tan ‘ ( i · 𝐴 ) ) / i ) = ( ( tan ‘ ( i · - 𝐴 ) ) / i ) )
21 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
22 tanhlt1 ⊢ ( - 𝐴 ∈ ℝ → ( ( tan ‘ ( i · - 𝐴 ) ) / i ) < 1 )
23 21 22 syl ⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · - 𝐴 ) ) / i ) < 1 )
24 20 23 eqbrtrd ⊢ ( 𝐴 ∈ ℝ → - ( ( tan ‘ ( i · 𝐴 ) ) / i ) < 1 )
25 1re ⊢ 1 ∈ ℝ
26 ltnegcon1 ⊢ ( ( ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( - ( ( tan ‘ ( i · 𝐴 ) ) / i ) < 1 ↔ - 1 < ( ( tan ‘ ( i · 𝐴 ) ) / i ) ) )
27 1 25 26 sylancl ⊢ ( 𝐴 ∈ ℝ → ( - ( ( tan ‘ ( i · 𝐴 ) ) / i ) < 1 ↔ - 1 < ( ( tan ‘ ( i · 𝐴 ) ) / i ) ) )
28 24 27 mpbid ⊢ ( 𝐴 ∈ ℝ → - 1 < ( ( tan ‘ ( i · 𝐴 ) ) / i ) )
29 tanhlt1 ⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) < 1 )
30 neg1rr ⊢ - 1 ∈ ℝ
31 30 rexri ⊢ - 1 ∈ ℝ*
32 25 rexri ⊢ 1 ∈ ℝ*
33 elioo2 ⊢ ( ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ( - 1 (,) 1 ) ↔ ( ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ ∧ - 1 < ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∧ ( ( tan ‘ ( i · 𝐴 ) ) / i ) < 1 ) ) )
34 31 32 33 mp2an ⊢ ( ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ( - 1 (,) 1 ) ↔ ( ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ℝ ∧ - 1 < ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∧ ( ( tan ‘ ( i · 𝐴 ) ) / i ) < 1 ) )
35 1 28 29 34 syl3anbrc ⊢ ( 𝐴 ∈ ℝ → ( ( tan ‘ ( i · 𝐴 ) ) / i ) ∈ ( - 1 (,) 1 ) )