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