Metamath Proof Explorer

Theorem tanval3

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

Ref Expression
Assertion tanval3 ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) − 1 ) / ( i · ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → 𝐴 ∈ ℂ )
3 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4 1 2 3 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · 𝐴 ) ∈ ℂ )
5 efcl ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
6 4 5 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
7 negicn ⊢ - i ∈ ℂ
8 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
9 7 2 8 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( - i · 𝐴 ) ∈ ℂ )
10 efcl ⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
11 9 10 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
12 6 11 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
13 6 11 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
14 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ) → ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ∈ ℂ )
15 1 13 14 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ∈ ℂ )
16 2z ⊢ 2 ∈ ℤ
17 efexp ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 2 ∈ ℤ ) → ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) )
18 4 16 17 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) )
19 6 sqvald ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
20 18 19 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
21 mulneg1 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = - ( i · 𝐴 ) )
22 1 2 21 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( - i · 𝐴 ) = - ( i · 𝐴 ) )
23 22 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( - i · 𝐴 ) ) = ( exp ‘ - ( i · 𝐴 ) ) )
24 23 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ - ( i · 𝐴 ) ) ) )
25 efcan ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ - ( i · 𝐴 ) ) ) = 1 )
26 4 25 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ - ( i · 𝐴 ) ) ) = 1 )
27 24 26 eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → 1 = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
28 20 27 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) ) )
29 6 6 11 adddid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) + ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) ) )
30 28 29 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) )
31 30 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ) = ( i · ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
32 1 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → i ∈ ℂ )
33 32 6 13 mul12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
34 31 33 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
35 2cn ⊢ 2 ∈ ℂ
36 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 2 · ( i · 𝐴 ) ) ∈ ℂ )
37 35 4 36 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( 2 · ( i · 𝐴 ) ) ∈ ℂ )
38 efcl ⊢ ( ( 2 · ( i · 𝐴 ) ) ∈ ℂ → ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) ∈ ℂ )
39 37 38 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) ∈ ℂ )
40 ax-1cn ⊢ 1 ∈ ℂ
41 addcl ⊢ ( ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ∈ ℂ )
42 39 40 41 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ∈ ℂ )
43 ine0 ⊢ i ≠ 0
44 43 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → i ≠ 0 )
45 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 )
46 32 42 44 45 mulne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ) ≠ 0 )
47 34 46 eqnetrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ≠ 0 )
48 6 15 47 mulne0bbd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ≠ 0 )
49 efne0 ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ≠ 0 )
50 4 49 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( exp ‘ ( i · 𝐴 ) ) ≠ 0 )
51 12 15 6 48 50 divcan5d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
52 20 27 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) − 1 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) ) )
53 6 6 11 subdid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) ) )
54 52 53 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) − 1 ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) )
55 54 34 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) − 1 ) / ( i · ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ) / ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) )
56 cosval ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
57 56 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
58 2cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → 2 ∈ ℂ )
59 32 13 48 mulne0bbd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ≠ 0 )
60 2ne0 ⊢ 2 ≠ 0
61 60 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → 2 ≠ 0 )
62 13 58 59 61 divne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ≠ 0 )
63 57 62 eqnetrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( cos ‘ 𝐴 ) ≠ 0 )
64 tanval2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
65 63 64 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( i · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
66 51 55 65 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) − 1 ) / ( i · ( ( exp ‘ ( 2 · ( i · 𝐴 ) ) ) + 1 ) ) ) )