Metamath Proof Explorer

Theorem sinhpcosh

Description: Prove that ( sinhA ) + ( coshA ) = ( expA ) using the conventional hyperbolic trigonometric functions. (Contributed by David A. Wheeler, 27-May-2015)

Ref Expression
Assertion sinhpcosh ( 𝐴 ∈ ℂ → ( ( sinh ‘ 𝐴 ) + ( cosh ‘ 𝐴 ) ) = ( exp ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sinhval-named ⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( ( sin ‘ ( i · 𝐴 ) ) / i ) )
2 sinhval ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) )
3 1 2 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) )
4 coshval-named ⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) = ( cos ‘ ( i · 𝐴 ) ) )
5 coshval ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( i · 𝐴 ) ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )
6 4 5 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) = ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) )
7 3 6 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( sinh ‘ 𝐴 ) + ( cosh ‘ 𝐴 ) ) = ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) + ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ) )
8 2cn ⊢ 2 ∈ ℂ
9 2ne0 ⊢ 2 ≠ 0
10 efcl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
11 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
12 efcl ⊢ ( - 𝐴 ∈ ℂ → ( exp ‘ - 𝐴 ) ∈ ℂ )
13 11 12 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - 𝐴 ) ∈ ℂ )
14 10 13 addcld ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ∈ ℂ )
15 10 13 subcld ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) ∈ ℂ )
16 divdir ⊢ ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) ∈ ℂ ∧ ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) / 2 ) = ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) + ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ) )
17 15 16 syl3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) / 2 ) = ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) + ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ) )
18 14 17 syl3an2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) / 2 ) = ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) + ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ) )
19 18 3anidm12 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) / 2 ) = ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) + ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ) )
20 8 9 19 mpanr12 ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) / 2 ) = ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) / 2 ) + ( ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) / 2 ) ) )
21 10 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( exp ‘ 𝐴 ) ) = ( ( exp ‘ 𝐴 ) + ( exp ‘ 𝐴 ) ) )
22 10 13 10 nppcand ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( exp ‘ 𝐴 ) ) + ( exp ‘ - 𝐴 ) ) = ( ( exp ‘ 𝐴 ) + ( exp ‘ 𝐴 ) ) )
23 15 10 13 addassd ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( exp ‘ 𝐴 ) ) + ( exp ‘ - 𝐴 ) ) = ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) )
24 21 22 23 3eqtr2rd ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) = ( 2 · ( exp ‘ 𝐴 ) ) )
25 24 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ 𝐴 ) − ( exp ‘ - 𝐴 ) ) + ( ( exp ‘ 𝐴 ) + ( exp ‘ - 𝐴 ) ) ) / 2 ) = ( ( 2 · ( exp ‘ 𝐴 ) ) / 2 ) )
26 7 20 25 3eqtr2d ⊢ ( 𝐴 ∈ ℂ → ( ( sinh ‘ 𝐴 ) + ( cosh ‘ 𝐴 ) ) = ( ( 2 · ( exp ‘ 𝐴 ) ) / 2 ) )
27 8 a1i ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
28 9 a1i ⊢ ( 𝐴 ∈ ℂ → 2 ≠ 0 )
29 10 27 28 divcan3d ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · ( exp ‘ 𝐴 ) ) / 2 ) = ( exp ‘ 𝐴 ) )
30 26 29 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( sinh ‘ 𝐴 ) + ( cosh ‘ 𝐴 ) ) = ( exp ‘ 𝐴 ) )