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	11	efcld	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
13	10 12	addcld	$$⊢A\in ℂ\to {\mathrm{e}}^A+{\mathrm{e}}^{-A}\in ℂ$$
14	10 12	subcld	$$⊢A\in ℂ\to {\mathrm{e}}^A-{\mathrm{e}}^{-A}\in ℂ$$
15		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)$$
16	14 15	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)$$
17	13 16	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)$$
18	17	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)$$
19	8 9 18	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)$$
20	10	2timesd	$$⊢A\in ℂ\to 2{\mathrm{e}}^A={\mathrm{e}}^A+{\mathrm{e}}^A$$
21	10 12 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$$
22	14 10 12	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}$$
23	20 21 22	3eqtr2rd	$$⊢A\in ℂ\to \left({\mathrm{e}}^A-{\mathrm{e}}^{-A}\right)+{\mathrm{e}}^A+{\mathrm{e}}^{-A}=2{\mathrm{e}}^A$$
24	23	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}$$
25	7 19 24	3eqtr2d	$$⊢A\in ℂ\to \sinh \left(A\right)+\cosh \left(A\right)=\frac{2{\mathrm{e}}^A}{2}$$
26	8	a1i	$$⊢A\in ℂ\to 2\in ℂ$$
27	9	a1i	$$⊢A\in ℂ\to 2\ne 0$$
28	10 26 27	divcan3d	$$⊢A\in ℂ\to \frac{2{\mathrm{e}}^A}{2}={\mathrm{e}}^A$$
29	25 28	eqtrd	$$⊢A\in ℂ\to \sinh \left(A\right)+\cosh \left(A\right)={\mathrm{e}}^A$$