Metamath Proof Explorer

Theorem sinhadd

Description: Addition formula for sinh. (Contributed by Jon Pennant, 9-Sep-2026)

Ref Expression
Assertion sinhadd 
|- ( ( A e. CC /\ B e. CC ) -> ( sinh ` ( A + B ) ) = ( ( ( sinh ` A ) x. ( cosh ` B ) ) + ( ( cosh ` A ) x. ( sinh ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 sinhval-named 
 |-  ( ( A + B ) e. CC -> ( sinh ` ( A + B ) ) = ( ( sin ` ( _i x. ( A + B ) ) ) / _i ) )
3 1 2 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sinh ` ( A + B ) ) = ( ( sin ` ( _i x. ( A + B ) ) ) / _i ) )
4 ax-icn 
 |-  _i e. CC
5 adddi 
 |-  ( ( _i e. CC /\ A e. CC /\ B e. CC ) -> ( _i x. ( A + B ) ) = ( ( _i x. A ) + ( _i x. B ) ) )
6 4 5 mp3an1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( A + B ) ) = ( ( _i x. A ) + ( _i x. B ) ) )
7 6 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( _i x. ( A + B ) ) ) = ( sin ` ( ( _i x. A ) + ( _i x. B ) ) ) )
8 7 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( _i x. ( A + B ) ) ) / _i ) = ( ( sin ` ( ( _i x. A ) + ( _i x. B ) ) ) / _i ) )
9 4 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> _i e. CC )
10 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
11 9 10 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. A ) e. CC )
12 mulcl 
 |-  ( ( _i e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
13 9 12 sylancom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
14 sinadd 
 |-  ( ( ( _i x. A ) e. CC /\ ( _i x. B ) e. CC ) -> ( sin ` ( ( _i x. A ) + ( _i x. B ) ) ) = ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
15 11 13 14 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( ( _i x. A ) + ( _i x. B ) ) ) = ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
16 15 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( ( _i x. A ) + ( _i x. B ) ) ) / _i ) = ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) / _i ) )
17 3 8 16 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sinh ` ( A + B ) ) = ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) / _i ) )
18 11 sincld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( _i x. A ) ) e. CC )
19 13 coscld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( _i x. B ) ) e. CC )
20 18 19 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) e. CC )
21 11 coscld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( _i x. A ) ) e. CC )
22 13 sincld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( _i x. B ) ) e. CC )
23 21 22 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) e. CC )
24 ine0 
 |-  _i =/= 0
25 4 24 pm3.2i 
 |-  ( _i e. CC /\ _i =/= 0 )
26 divdir 
 |-  ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) e. CC /\ ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) e. CC /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) / _i ) = ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) / _i ) + ( ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) / _i ) ) )
27 25 26 mp3an3 
 |-  ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) e. CC /\ ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) e. CC ) -> ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) / _i ) = ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) / _i ) + ( ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) / _i ) ) )
28 20 23 27 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) / _i ) = ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) / _i ) + ( ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) / _i ) ) )
29 24 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> _i =/= 0 )
30 18 19 9 29 div23d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) / _i ) = ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( cos ` ( _i x. B ) ) ) )
31 21 22 9 29 divassd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) / _i ) = ( ( cos ` ( _i x. A ) ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) )
32 30 31 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( sin ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) / _i ) + ( ( ( cos ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) / _i ) ) = ( ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) )
33 17 28 32 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sinh ` ( A + B ) ) = ( ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) )
34 sinhval-named 
 |-  ( A e. CC -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
35 coshval-named 
 |-  ( B e. CC -> ( cosh ` B ) = ( cos ` ( _i x. B ) ) )
36 34 35 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. ( cosh ` B ) ) = ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( cos ` ( _i x. B ) ) ) )
37 coshval-named 
 |-  ( A e. CC -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
38 sinhval-named 
 |-  ( B e. CC -> ( sinh ` B ) = ( ( sin ` ( _i x. B ) ) / _i ) )
39 37 38 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cosh ` A ) x. ( sinh ` B ) ) = ( ( cos ` ( _i x. A ) ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) )
40 36 39 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( sinh ` A ) x. ( cosh ` B ) ) + ( ( cosh ` A ) x. ( sinh ` B ) ) ) = ( ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( cos ` ( _i x. B ) ) ) + ( ( cos ` ( _i x. A ) ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) )
41 33 40 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sinh ` ( A + B ) ) = ( ( ( sinh ` A ) x. ( cosh ` B ) ) + ( ( cosh ` A ) x. ( sinh ` B ) ) ) )