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 
|- ( A e. CC -> ( ( sinh ` A ) + ( cosh ` A ) ) = ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 sinhval-named 
 |-  ( A e. CC -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
2 sinhval 
 |-  ( A e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
3 1 2 eqtrd 
 |-  ( A e. CC -> ( sinh ` A ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) )
4 coshval-named 
 |-  ( A e. CC -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
5 coshval 
 |-  ( A e. CC -> ( cos ` ( _i x. A ) ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )
6 4 5 eqtrd 
 |-  ( A e. CC -> ( cosh ` A ) = ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) )
7 3 6 oveq12d 
 |-  ( A e. CC -> ( ( sinh ` A ) + ( cosh ` A ) ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) + ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
8 2cn 
 |-  2 e. CC
9 2ne0 
 |-  2 =/= 0
10 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
11 negcl 
 |-  ( A e. CC -> -u A e. CC )
12 efcl 
 |-  ( -u A e. CC -> ( exp ` -u A ) e. CC )
13 11 12 syl 
 |-  ( A e. CC -> ( exp ` -u A ) e. CC )
14 10 13 addcld 
 |-  ( A e. CC -> ( ( exp ` A ) + ( exp ` -u A ) ) e. CC )
15 10 13 subcld 
 |-  ( A e. CC -> ( ( exp ` A ) - ( exp ` -u A ) ) e. CC )
16 divdir 
 |-  ( ( ( ( exp ` A ) - ( exp ` -u A ) ) e. CC /\ ( ( exp ` A ) + ( exp ` -u A ) ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) / 2 ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) + ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
17 15 16 syl3an1 
 |-  ( ( A e. CC /\ ( ( exp ` A ) + ( exp ` -u A ) ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) / 2 ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) + ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
18 14 17 syl3an2 
 |-  ( ( A e. CC /\ A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) / 2 ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) + ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
19 18 3anidm12 
 |-  ( ( A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) / 2 ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) + ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
20 8 9 19 mpanr12 
 |-  ( A e. CC -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) / 2 ) = ( ( ( ( exp ` A ) - ( exp ` -u A ) ) / 2 ) + ( ( ( exp ` A ) + ( exp ` -u A ) ) / 2 ) ) )
21 10 2timesd 
 |-  ( A e. CC -> ( 2 x. ( exp ` A ) ) = ( ( exp ` A ) + ( exp ` A ) ) )
22 10 13 10 nppcand 
 |-  ( A e. CC -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( exp ` A ) ) + ( exp ` -u A ) ) = ( ( exp ` A ) + ( exp ` A ) ) )
23 15 10 13 addassd 
 |-  ( A e. CC -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( exp ` A ) ) + ( exp ` -u A ) ) = ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) )
24 21 22 23 3eqtr2rd 
 |-  ( A e. CC -> ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) = ( 2 x. ( exp ` A ) ) )
25 24 oveq1d 
 |-  ( A e. CC -> ( ( ( ( exp ` A ) - ( exp ` -u A ) ) + ( ( exp ` A ) + ( exp ` -u A ) ) ) / 2 ) = ( ( 2 x. ( exp ` A ) ) / 2 ) )
26 7 20 25 3eqtr2d 
 |-  ( A e. CC -> ( ( sinh ` A ) + ( cosh ` A ) ) = ( ( 2 x. ( exp ` A ) ) / 2 ) )
27 8 a1i 
 |-  ( A e. CC -> 2 e. CC )
28 9 a1i 
 |-  ( A e. CC -> 2 =/= 0 )
29 10 27 28 divcan3d 
 |-  ( A e. CC -> ( ( 2 x. ( exp ` A ) ) / 2 ) = ( exp ` A ) )
30 26 29 eqtrd 
 |-  ( A e. CC -> ( ( sinh ` A ) + ( cosh ` A ) ) = ( exp ` A ) )