Metamath Proof Explorer

Theorem tanval2

Description: Express the tangent function directly in terms of exp . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion tanval2 ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tanval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
2 2cn ⊢ 2 ∈ ℂ
3 ax-icn ⊢ i ∈ ℂ
4 2 3 mulcomi ⊢ ( 2 · i ) = ( i · 2 )
5 4 oveq2i ⊢ ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · 2 ) )
6 sinval ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
8 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
9 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
10 3 8 9 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( i · 𝐴 ) ∈ ℂ )
11 efcl ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
12 10 11 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
13 negicn ⊢ - i ∈ ℂ
14 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
15 13 8 14 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( - i · 𝐴 ) ∈ ℂ )
16 efcl ⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
17 15 16 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
18 12 17 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
19 3 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → i ∈ ℂ )
20 2 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → 2 ∈ ℂ )
21 ine0 ⊢ i ≠ 0
22 21 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → i ≠ 0 )
23 2ne0 ⊢ 2 ≠ 0
24 23 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → 2 ≠ 0 )
25 18 19 20 22 24 divdiv1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · 2 ) ) )
26 5 7 25 3eqtr4a ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( sin ‘ 𝐴 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / 2 ) )
27 cosval ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
28 27 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
29 26 28 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) = ( ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / 2 ) / ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) )
30 1 29 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / 2 ) / ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) )
31 18 19 22 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) ∈ ℂ )
32 12 17 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
33 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ≠ 0 )
34 28 33 eqnetrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ≠ 0 )
35 32 20 24 diveq0ad ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
36 35 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ≠ 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ≠ 0 ) )
37 34 36 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ≠ 0 )
38 31 32 20 37 24 divcan7d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / 2 ) / ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) )
39 18 19 32 22 37 divdiv1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / i ) / ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
40 30 38 39 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )