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	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( - i · ( sin ‘ ( i · 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sinhval-named	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( ( sin ‘ ( i · 𝐴 ) ) / i ) )
2		ax-icn	⊢ i ∈ ℂ
3		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4	2 3	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
5	4	sincld	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ )
6		ine0	⊢ i ≠ 0
7		divrec2	⊢ ( ( ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( ( 1 / i ) · ( sin ‘ ( i · 𝐴 ) ) ) )
8	2 6 7	mp3an23	⊢ ( ( sin ‘ ( i · 𝐴 ) ) ∈ ℂ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( ( 1 / i ) · ( sin ‘ ( i · 𝐴 ) ) ) )
9	5 8	syl	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( i · 𝐴 ) ) / i ) = ( ( 1 / i ) · ( sin ‘ ( i · 𝐴 ) ) ) )
10		irec	⊢ ( 1 / i ) = - i
11	10	oveq1i	⊢ ( ( 1 / i ) · ( sin ‘ ( i · 𝐴 ) ) ) = ( - i · ( sin ‘ ( i · 𝐴 ) ) )
12	11	a1i	⊢ ( 𝐴 ∈ ℂ → ( ( 1 / i ) · ( sin ‘ ( i · 𝐴 ) ) ) = ( - i · ( sin ‘ ( i · 𝐴 ) ) ) )
13	1 9 12	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) = ( - i · ( sin ‘ ( i · 𝐴 ) ) ) )