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