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

Proof

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