This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpcoshcl

Description: The hyperbolic cosine of a real number is a positive real. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion rpcoshcl ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 coshval ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )
4 rpefcl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ+ )
5 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
6 5 rpefcld ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ - 𝐴 ) ∈ ℝ+ )
7 4 6 rpaddcld ⊢ ( 𝐴 ∈ ℝ → ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ∈ ℝ+ )
8 7 rphalfcld ⊢ ( 𝐴 ∈ ℝ → ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ∈ ℝ+ )
9 3 8 eqeltrd ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ ( i · 𝐴 ) ) ∈ ℝ+ )