Proof of Theorem tanval2
Step | Hyp | Ref
| Expression |
1 | | tanval 15837 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
2 | | 2cn 12048 |
. . . . . . 7
⊢ 2 ∈
ℂ |
3 | | ax-icn 10930 |
. . . . . . 7
⊢ i ∈
ℂ |
4 | 2, 3 | mulcomi 10983 |
. . . . . 6
⊢ (2
· i) = (i · 2) |
5 | 4 | oveq2i 7286 |
. . . . 5
⊢
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i ·
2)) |
6 | | sinval 15831 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) |
8 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 𝐴 ∈
ℂ) |
9 | | mulcl 10955 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
10 | 3, 8, 9 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (i · 𝐴)
∈ ℂ) |
11 | | efcl 15792 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (exp‘(i · 𝐴)) ∈ ℂ) |
13 | | negicn 11222 |
. . . . . . . . 9
⊢ -i ∈
ℂ |
14 | | mulcl 10955 |
. . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
15 | 13, 8, 14 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (-i · 𝐴)
∈ ℂ) |
16 | | efcl 15792 |
. . . . . . . 8
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
18 | 12, 17 | subcld 11332 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈
ℂ) |
19 | 3 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ i ∈ ℂ) |
20 | 2 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 2 ∈ ℂ) |
21 | | ine0 11410 |
. . . . . . 7
⊢ i ≠
0 |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ i ≠ 0) |
23 | | 2ne0 12077 |
. . . . . . 7
⊢ 2 ≠
0 |
24 | 23 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 2 ≠ 0) |
25 | 18, 19, 20, 22, 24 | divdiv1d 11782 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) = (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / (i · 2))) |
26 | 5, 7, 25 | 3eqtr4a 2804 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (sin‘𝐴) =
((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2)) |
27 | | cosval 15832 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
28 | 27 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
29 | 26, 28 | oveq12d 7293 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((sin‘𝐴) /
(cos‘𝐴)) =
(((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) / (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2))) |
30 | 1, 29 | eqtrd 2778 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) / (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2))) |
31 | 18, 19, 22 | divcld 11751 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) ∈
ℂ) |
32 | 12, 17 | addcld 10994 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈
ℂ) |
33 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (cos‘𝐴) ≠
0) |
34 | 28, 33 | eqnetrrd 3012 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) ≠
0) |
35 | 32, 20, 24 | diveq0ad 11761 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) = 0 ↔
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) = 0)) |
36 | 35 | necon3bid 2988 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) ≠ 0 ↔
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) ≠ 0)) |
37 | 34, 36 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ≠ 0) |
38 | 31, 32, 20, 37, 24 | divcan7d 11779 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(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 11782 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(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 2782 |
1
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i · ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴)))))) |