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 ∈ ℝ → tan ⁡ i ⁢ A i ∈ − 1 1

Proof

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