Proof of Theorem tanval2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tanval 16165 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) | 
| 2 |  | 2cn 12342 | . . . . . . 7
⊢ 2 ∈
ℂ | 
| 3 |  | ax-icn 11215 | . . . . . . 7
⊢ i ∈
ℂ | 
| 4 | 2, 3 | mulcomi 11270 | . . . . . 6
⊢ (2
· i) = (i · 2) | 
| 5 | 4 | oveq2i 7443 | . . . . 5
⊢
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i ·
2)) | 
| 6 |  | sinval 16159 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (sin‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 ·
i))) | 
| 8 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 𝐴 ∈
ℂ) | 
| 9 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 10 | 3, 8, 9 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (i · 𝐴)
∈ ℂ) | 
| 11 |  | efcl 16119 | . . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) | 
| 12 | 10, 11 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (exp‘(i · 𝐴)) ∈ ℂ) | 
| 13 |  | negicn 11510 | . . . . . . . . 9
⊢ -i ∈
ℂ | 
| 14 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) | 
| 15 | 13, 8, 14 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (-i · 𝐴)
∈ ℂ) | 
| 16 |  | efcl 16119 | . . . . . . . 8
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) | 
| 17 | 15, 16 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (exp‘(-i · 𝐴)) ∈ ℂ) | 
| 18 | 12, 17 | subcld 11621 | . . . . . 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 11699 | . . . . . . 7
⊢ i ≠
0 | 
| 22 | 21 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ i ≠ 0) | 
| 23 |  | 2ne0 12371 | . . . . . . 7
⊢ 2 ≠
0 | 
| 24 | 23 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ 2 ≠ 0) | 
| 25 | 18, 19, 20, 22, 24 | divdiv1d 12075 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) = (((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) / (i · 2))) | 
| 26 | 5, 7, 25 | 3eqtr4a 2802 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (sin‘𝐴) =
((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2)) | 
| 27 |  | cosval 16160 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) | 
| 28 | 27 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) | 
| 29 | 26, 28 | oveq12d 7450 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((sin‘𝐴) /
(cos‘𝐴)) =
(((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) / (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2))) | 
| 30 | 1, 29 | eqtrd 2776 | . 2
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) / 2) / (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2))) | 
| 31 | 18, 19, 22 | divcld 12044 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / i) ∈
ℂ) | 
| 32 | 12, 17 | addcld 11281 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈
ℂ) | 
| 33 |  | simpr 484 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (cos‘𝐴) ≠
0) | 
| 34 | 28, 33 | eqnetrrd 3008 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) ≠
0) | 
| 35 | 32, 20, 24 | diveq0ad 12054 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) = 0 ↔
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) = 0)) | 
| 36 | 35 | necon3bid 2984 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) ≠ 0 ↔
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))) ≠ 0)) | 
| 37 | 34, 36 | mpbid 232 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ≠ 0) | 
| 38 | 31, 32, 20, 37, 24 | divcan7d 12072 | . 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 12075 | . 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 2780 | 1
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i · ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴)))))) |