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	$$⊢A\in ℂ\to \sinh \left(A\right)+\cosh \left(A\right)={\mathrm{e}}^A$$

Proof

Step	Hyp	Ref	Expression
1		sinhval-named	$$⊢A\in ℂ\to \sinh \left(A\right)=\frac{\sin \mathrm{i}A}{\mathrm{i}}$$
2		sinhval	$$⊢A\in ℂ\to \frac{\sin \mathrm{i}A}{\mathrm{i}}=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}$$
3	1 2	eqtrd	$$⊢A\in ℂ\to \sinh \left(A\right)=\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}$$
4		coshval-named	$$⊢A\in ℂ\to \cosh \left(A\right)=\cos \mathrm{i}A$$
5		coshval	$$⊢A\in ℂ\to \cos \mathrm{i}A=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$
6	4 5	eqtrd	$$⊢A\in ℂ\to \cosh \left(A\right)=\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}$$
7	3 6	oveq12d	$$⊢A\in ℂ\to \sinh \left(A\right)+\cosh \left(A\right)=\left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}\right)+\left(\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\right)$$
8		2cn	$$⊢2\in ℂ$$
9		2ne0	$$⊢2\ne 0$$
10		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
11		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
12		efcl	$$⊢-A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
13	11 12	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
14	10 13	addcld	$$⊢A\in ℂ\to {\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℂ$$
15	10 13	subcld	$$⊢A\in ℂ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}\in ℂ$$
16		divdir	$$⊢\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\in ℂ\wedge {\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}=\left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}\right)+\left(\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\right)$$
17	15 16	syl3an1	$$⊢\left(A\in ℂ\wedge {\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}=\left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}\right)+\left(\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\right)$$
18	14 17	syl3an2	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}=\left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}\right)+\left(\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\right)$$
19	18	3anidm12	$$⊢\left(A\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}=\left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}\right)+\left(\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\right)$$
20	8 9 19	mpanr12	$$⊢A\in ℂ\to \frac{\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}=\left(\frac{{\mathrm{e}}^A-{\mathrm{e}}^{-A}}{2}\right)+\left(\frac{{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}\right)$$
21	10	2timesd	$$⊢A\in ℂ\to 2{\mathrm{e}}^A={\mathrm{e}}^A+{\mathrm{e}}^A$$
22	10 13 10	nppcand	$$⊢A\in ℂ\to \left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}={\mathrm{e}}^A+{\mathrm{e}}^A$$
23	15 10 13	addassd	$$⊢A\in ℂ\to \left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}=\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}$$
24	21 22 23	3eqtr2rd	$$⊢A\in ℂ\to \left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}=2{\mathrm{e}}^A$$
25	24	oveq1d	$$⊢A\in ℂ\to \frac{\left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}}{2}=\frac{2{\mathrm{e}}^A}{2}$$
26	7 20 25	3eqtr2d	$$⊢A\in ℂ\to \sinh \left(A\right)+\cosh \left(A\right)=\frac{2{\mathrm{e}}^A}{2}$$
27	8	a1i	$$⊢A\in ℂ\to 2\in ℂ$$
28	9	a1i	$$⊢A\in ℂ\to 2\ne 0$$
29	10 27 28	divcan3d	$$⊢A\in ℂ\to \frac{2{\mathrm{e}}^A}{2}={\mathrm{e}}^A$$
30	26 29	eqtrd	$$⊢A\in ℂ\to \sinh \left(A\right)+\cosh \left(A\right)={\mathrm{e}}^A$$