Proof of Theorem tanval3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ax-icn 11215 | . . . . . 6
⊢ i ∈
ℂ | 
| 2 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → 𝐴 ∈ ℂ) | 
| 3 |  | mulcl 11240 | . . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 4 | 1, 2, 3 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i · 𝐴) ∈
ℂ) | 
| 5 |  | efcl 16119 | . . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) | 
| 6 | 4, 5 | syl 17 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(i
· 𝐴)) ∈
ℂ) | 
| 7 |  | negicn 11510 | . . . . . 6
⊢ -i ∈
ℂ | 
| 8 |  | mulcl 11240 | . . . . . 6
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) | 
| 9 | 7, 2, 8 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (-i · 𝐴) ∈
ℂ) | 
| 10 |  | efcl 16119 | . . . . 5
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) | 
| 11 | 9, 10 | syl 17 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(-i
· 𝐴)) ∈
ℂ) | 
| 12 | 6, 11 | subcld 11621 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) −
(exp‘(-i · 𝐴))) ∈ ℂ) | 
| 13 | 6, 11 | addcld 11281 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) ∈ ℂ) | 
| 14 |  | mulcl 11240 | . . . 4
⊢ ((i
∈ ℂ ∧ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ) → (i
· ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))) ∈
ℂ) | 
| 15 | 1, 13, 14 | sylancr 587 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))) ∈ ℂ) | 
| 16 |  | 2z 12651 | . . . . . . . . . . 11
⊢ 2 ∈
ℤ | 
| 17 |  | efexp 16138 | . . . . . . . . . . 11
⊢ (((i
· 𝐴) ∈ ℂ
∧ 2 ∈ ℤ) → (exp‘(2 · (i · 𝐴))) = ((exp‘(i ·
𝐴))↑2)) | 
| 18 | 4, 16, 17 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(2
· (i · 𝐴))) =
((exp‘(i · 𝐴))↑2)) | 
| 19 | 6 | sqvald 14184 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴))↑2) =
((exp‘(i · 𝐴))
· (exp‘(i · 𝐴)))) | 
| 20 | 18, 19 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(2
· (i · 𝐴))) =
((exp‘(i · 𝐴))
· (exp‘(i · 𝐴)))) | 
| 21 |  | mulneg1 11700 | . . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) = -(i · 𝐴)) | 
| 22 | 1, 2, 21 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (-i · 𝐴) = -(i · 𝐴)) | 
| 23 | 22 | fveq2d 6909 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(-i
· 𝐴)) =
(exp‘-(i · 𝐴))) | 
| 24 | 23 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) ·
(exp‘(-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘-(i
· 𝐴)))) | 
| 25 |  | efcan 16133 | . . . . . . . . . . 11
⊢ ((i
· 𝐴) ∈ ℂ
→ ((exp‘(i · 𝐴)) · (exp‘-(i · 𝐴))) = 1) | 
| 26 | 4, 25 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) ·
(exp‘-(i · 𝐴))) = 1) | 
| 27 | 24, 26 | eqtr2d 2777 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → 1 = ((exp‘(i
· 𝐴)) ·
(exp‘(-i · 𝐴)))) | 
| 28 | 20, 27 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(2
· (i · 𝐴))) +
1) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) + ((exp‘(i ·
𝐴)) · (exp‘(-i
· 𝐴))))) | 
| 29 | 6, 6, 11 | adddid 11286 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))) = (((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴))) +
((exp‘(i · 𝐴))
· (exp‘(-i · 𝐴))))) | 
| 30 | 28, 29 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(2
· (i · 𝐴))) +
1) = ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴))))) | 
| 31 | 30 | oveq2d 7448 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i ·
((exp‘(2 · (i · 𝐴))) + 1)) = (i · ((exp‘(i
· 𝐴)) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))))) | 
| 32 | 1 | a1i 11 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → i ∈
ℂ) | 
| 33 | 32, 6, 13 | mul12d 11471 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i ·
((exp‘(i · 𝐴))
· ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))))) = ((exp‘(i ·
𝐴)) · (i ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))))) | 
| 34 | 31, 33 | eqtrd 2776 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i ·
((exp‘(2 · (i · 𝐴))) + 1)) = ((exp‘(i · 𝐴)) · (i ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))))) | 
| 35 |  | 2cn 12342 | . . . . . . . . 9
⊢ 2 ∈
ℂ | 
| 36 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (2 · (i
· 𝐴)) ∈
ℂ) | 
| 37 | 35, 4, 36 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (2 · (i
· 𝐴)) ∈
ℂ) | 
| 38 |  | efcl 16119 | . . . . . . . 8
⊢ ((2
· (i · 𝐴))
∈ ℂ → (exp‘(2 · (i · 𝐴))) ∈ ℂ) | 
| 39 | 37, 38 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(2
· (i · 𝐴)))
∈ ℂ) | 
| 40 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 41 |  | addcl 11238 | . . . . . . 7
⊢
(((exp‘(2 · (i · 𝐴))) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((exp‘(2 · (i · 𝐴))) + 1) ∈ ℂ) | 
| 42 | 39, 40, 41 | sylancl 586 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(2
· (i · 𝐴))) +
1) ∈ ℂ) | 
| 43 |  | ine0 11699 | . . . . . . 7
⊢ i ≠
0 | 
| 44 | 43 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → i ≠
0) | 
| 45 |  | simpr 484 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(2
· (i · 𝐴))) +
1) ≠ 0) | 
| 46 | 32, 42, 44, 45 | mulne0d 11916 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i ·
((exp‘(2 · (i · 𝐴))) + 1)) ≠ 0) | 
| 47 | 34, 46 | eqnetrrd 3008 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) · (i
· ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))))) ≠ 0) | 
| 48 | 6, 15, 47 | mulne0bbd 11920 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (i ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))) ≠ 0) | 
| 49 |  | efne0 16134 | . . . 4
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ≠ 0) | 
| 50 | 4, 49 | syl 17 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (exp‘(i
· 𝐴)) ≠
0) | 
| 51 | 12, 15, 6, 48, 50 | divcan5d 12070 | . 2
⊢ ((𝐴 ∈ ℂ ∧
((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 7450 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(2
· (i · 𝐴)))
− 1) = (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i
· 𝐴)) ·
(exp‘(-i · 𝐴))))) | 
| 53 | 6, 6, 11 | subdid 11720 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) ·
((exp‘(i · 𝐴))
− (exp‘(-i · 𝐴)))) = (((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (exp‘(-i · 𝐴))))) | 
| 54 | 52, 53 | eqtr4d 2779 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(2
· (i · 𝐴)))
− 1) = ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (exp‘(-i
· 𝐴))))) | 
| 55 | 54, 34 | oveq12d 7450 | . 2
⊢ ((𝐴 ∈ ℂ ∧
((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 16160 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) | 
| 57 | 56 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (cos‘𝐴) = (((exp‘(i ·
𝐴)) + (exp‘(-i
· 𝐴))) /
2)) | 
| 58 |  | 2cnd 12345 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → 2 ∈
ℂ) | 
| 59 | 32, 13, 48 | mulne0bbd 11920 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) ≠ 0) | 
| 60 |  | 2ne0 12371 | . . . . . 6
⊢ 2 ≠
0 | 
| 61 | 60 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → 2 ≠
0) | 
| 62 | 13, 58, 59, 61 | divne0d 12060 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))) / 2) ≠ 0) | 
| 63 | 57, 62 | eqnetrd 3007 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (cos‘𝐴) ≠ 0) | 
| 64 |  | tanval2 16170 | . . 3
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
(((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (i · ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴)))))) | 
| 65 | 63, 64 | syldan 591 | . 2
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (tan‘𝐴) = (((exp‘(i ·
𝐴)) − (exp‘(-i
· 𝐴))) / (i ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))))) | 
| 66 | 51, 55, 65 | 3eqtr4rd 2787 | 1
⊢ ((𝐴 ∈ ℂ ∧
((exp‘(2 · (i · 𝐴))) + 1) ≠ 0) → (tan‘𝐴) = (((exp‘(2 · (i
· 𝐴))) − 1) /
(i · ((exp‘(2 · (i · 𝐴))) + 1)))) |