Proof of Theorem tanval2
Step | Hyp | Ref
| Expression |
1 | | tanval 15586 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
2 | | 2cn 11804 |
. . . . . . 7
⊢ 2 ∈
ℂ |
3 | | ax-icn 10687 |
. . . . . . 7
⊢ i ∈
ℂ |
4 | 2, 3 | mulcomi 10740 |
. . . . . 6
⊢ (2
· i) = (i · 2) |
5 | 4 | oveq2i 7194 |
. . . . 5
⊢
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i ·
2)) |
6 | | sinval 15580 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) |
8 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 𝐴 ∈
ℂ) |
9 | | mulcl 10712 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
10 | 3, 8, 9 | sylancr 590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (i · 𝐴)
∈ ℂ) |
11 | | efcl 15541 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (exp‘(i · 𝐴)) ∈ ℂ) |
13 | | negicn 10978 |
. . . . . . . . 9
⊢ -i ∈
ℂ |
14 | | mulcl 10712 |
. . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
15 | 13, 8, 14 | sylancr 590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (-i · 𝐴)
∈ ℂ) |
16 | | efcl 15541 |
. . . . . . . 8
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
18 | 12, 17 | subcld 11088 |
. . . . . 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 11166 |
. . . . . . 7
⊢ i ≠
0 |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ i ≠ 0) |
23 | | 2ne0 11833 |
. . . . . . 7
⊢ 2 ≠
0 |
24 | 23 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 2 ≠ 0) |
25 | 18, 19, 20, 22, 24 | divdiv1d 11538 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) = (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / (i · 2))) |
26 | 5, 7, 25 | 3eqtr4a 2800 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (sin‘𝐴) =
((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2)) |
27 | | cosval 15581 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
28 | 27 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
29 | 26, 28 | oveq12d 7201 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((sin‘𝐴) /
(cos‘𝐴)) =
(((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) / (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2))) |
30 | 1, 29 | eqtrd 2774 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) / (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2))) |
31 | 18, 19, 22 | divcld 11507 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) ∈
ℂ) |
32 | 12, 17 | addcld 10751 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈
ℂ) |
33 | | simpr 488 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (cos‘𝐴) ≠
0) |
34 | 28, 33 | eqnetrrd 3003 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) ≠
0) |
35 | 32, 20, 24 | diveq0ad 11517 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) = 0 ↔
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) = 0)) |
36 | 35 | necon3bid 2979 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) ≠ 0 ↔
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) ≠ 0)) |
37 | 34, 36 | mpbid 235 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ≠ 0) |
38 | 31, 32, 20, 37, 24 | divcan7d 11535 |
. 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 11538 |
. 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 2778 |
1
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i · ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴)))))) |