Metamath Proof Explorer

Theorem sinh-conventional

Description: Conventional definition of sinh. Here we show that the sinh definition we're using has the same meaning as the conventional definition used in some other sources. We choose a slightly different definition of sinh because it has fewer operations, and thus is more convenient to manipulate using set.mm. (Contributed by David A. Wheeler, 10-May-2015)

Ref Expression
Assertion sinh-conventional 
|- ( A e. CC -> ( sinh ` A ) = ( -u _i x. ( sin ` ( _i x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 sinhval-named 
 |-  ( A e. CC -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
2 ax-icn 
 |-  _i e. CC
3 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4 2 3 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
5 4 sincld 
 |-  ( A e. CC -> ( sin ` ( _i x. A ) ) e. CC )
6 ine0 
 |-  _i =/= 0
7 divrec2 
 |-  ( ( ( sin ` ( _i x. A ) ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( 1 / _i ) x. ( sin ` ( _i x. A ) ) ) )
8 2 6 7 mp3an23 
 |-  ( ( sin ` ( _i x. A ) ) e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( 1 / _i ) x. ( sin ` ( _i x. A ) ) ) )
9 5 8 syl 
 |-  ( A e. CC -> ( ( sin ` ( _i x. A ) ) / _i ) = ( ( 1 / _i ) x. ( sin ` ( _i x. A ) ) ) )
10 irec 
 |-  ( 1 / _i ) = -u _i
11 10 oveq1i 
 |-  ( ( 1 / _i ) x. ( sin ` ( _i x. A ) ) ) = ( -u _i x. ( sin ` ( _i x. A ) ) )
12 11 a1i 
 |-  ( A e. CC -> ( ( 1 / _i ) x. ( sin ` ( _i x. A ) ) ) = ( -u _i x. ( sin ` ( _i x. A ) ) ) )
13 1 9 12 3eqtrd 
 |-  ( A e. CC -> ( sinh ` A ) = ( -u _i x. ( sin ` ( _i x. A ) ) ) )