Proof of Theorem sinperlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zcn 12620 | . . . . . . . . 9
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) | 
| 2 |  | 2cn 12342 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 3 |  | picn 26502 | . . . . . . . . . 10
⊢ π
∈ ℂ | 
| 4 | 2, 3 | mulcli 11269 | . . . . . . . . 9
⊢ (2
· π) ∈ ℂ | 
| 5 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℂ ∧ (2
· π) ∈ ℂ) → (𝐾 · (2 · π)) ∈
ℂ) | 
| 6 | 1, 4, 5 | sylancl 586 | . . . . . . . 8
⊢ (𝐾 ∈ ℤ → (𝐾 · (2 · π))
∈ ℂ) | 
| 7 |  | ax-icn 11215 | . . . . . . . . 9
⊢ i ∈
ℂ | 
| 8 |  | adddi 11245 | . . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ (𝐾
· (2 · π)) ∈ ℂ) → (i · (𝐴 + (𝐾 · (2 · π)))) = ((i
· 𝐴) + (i ·
(𝐾 · (2 ·
π))))) | 
| 9 | 7, 8 | mp3an1 1449 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝐾 · (2 · π))
∈ ℂ) → (i · (𝐴 + (𝐾 · (2 · π)))) = ((i
· 𝐴) + (i ·
(𝐾 · (2 ·
π))))) | 
| 10 | 6, 9 | sylan2 593 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (i
· (𝐴 + (𝐾 · (2 · π)))) =
((i · 𝐴) + (i
· (𝐾 · (2
· π))))) | 
| 11 |  | mul12 11427 | . . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ 𝐾
∈ ℂ ∧ (2 · π) ∈ ℂ) → (i ·
(𝐾 · (2 ·
π))) = (𝐾 · (i
· (2 · π)))) | 
| 12 | 7, 4, 11 | mp3an13 1453 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℂ → (i
· (𝐾 · (2
· π))) = (𝐾
· (i · (2 · π)))) | 
| 13 | 1, 12 | syl 17 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (i
· (𝐾 · (2
· π))) = (𝐾
· (i · (2 · π)))) | 
| 14 | 7, 4 | mulcli 11269 | . . . . . . . . . . 11
⊢ (i
· (2 · π)) ∈ ℂ | 
| 15 |  | mulcom 11242 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ ℂ ∧ (i
· (2 · π)) ∈ ℂ) → (𝐾 · (i · (2 · π))) =
((i · (2 · π)) · 𝐾)) | 
| 16 | 1, 14, 15 | sylancl 586 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (𝐾 · (i · (2
· π))) = ((i · (2 · π)) · 𝐾)) | 
| 17 | 13, 16 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (i
· (𝐾 · (2
· π))) = ((i · (2 · π)) · 𝐾)) | 
| 18 | 17 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (i
· (𝐾 · (2
· π))) = ((i · (2 · π)) · 𝐾)) | 
| 19 | 18 | oveq2d 7448 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → ((i
· 𝐴) + (i ·
(𝐾 · (2 ·
π)))) = ((i · 𝐴)
+ ((i · (2 · π)) · 𝐾))) | 
| 20 | 10, 19 | eqtrd 2776 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (i
· (𝐴 + (𝐾 · (2 · π)))) =
((i · 𝐴) + ((i
· (2 · π)) · 𝐾))) | 
| 21 | 20 | fveq2d 6909 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(exp‘(i · (𝐴 +
(𝐾 · (2 ·
π))))) = (exp‘((i · 𝐴) + ((i · (2 · π)) ·
𝐾)))) | 
| 22 |  | mulcl 11240 | . . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 23 | 7, 22 | mpan 690 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) | 
| 24 |  | efper 26522 | . . . . . 6
⊢ (((i
· 𝐴) ∈ ℂ
∧ 𝐾 ∈ ℤ)
→ (exp‘((i · 𝐴) + ((i · (2 · π)) ·
𝐾))) = (exp‘(i
· 𝐴))) | 
| 25 | 23, 24 | sylan 580 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(exp‘((i · 𝐴)
+ ((i · (2 · π)) · 𝐾))) = (exp‘(i · 𝐴))) | 
| 26 | 21, 25 | eqtrd 2776 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(exp‘(i · (𝐴 +
(𝐾 · (2 ·
π))))) = (exp‘(i · 𝐴))) | 
| 27 |  | negicn 11510 | . . . . . . . . 9
⊢ -i ∈
ℂ | 
| 28 |  | adddi 11245 | . . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ (𝐾
· (2 · π)) ∈ ℂ) → (-i · (𝐴 + (𝐾 · (2 · π)))) = ((-i
· 𝐴) + (-i ·
(𝐾 · (2 ·
π))))) | 
| 29 | 27, 28 | mp3an1 1449 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝐾 · (2 · π))
∈ ℂ) → (-i · (𝐴 + (𝐾 · (2 · π)))) = ((-i
· 𝐴) + (-i ·
(𝐾 · (2 ·
π))))) | 
| 30 | 6, 29 | sylan2 593 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (-i
· (𝐴 + (𝐾 · (2 · π)))) =
((-i · 𝐴) + (-i
· (𝐾 · (2
· π))))) | 
| 31 | 17 | negeqd 11503 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → -(i
· (𝐾 · (2
· π))) = -((i · (2 · π)) · 𝐾)) | 
| 32 |  | mulneg1 11700 | . . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (𝐾
· (2 · π)) ∈ ℂ) → (-i · (𝐾 · (2 · π))) =
-(i · (𝐾 · (2
· π)))) | 
| 33 | 7, 6, 32 | sylancr 587 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → (-i
· (𝐾 · (2
· π))) = -(i · (𝐾 · (2 ·
π)))) | 
| 34 |  | mulneg2 11701 | . . . . . . . . . . 11
⊢ (((i
· (2 · π)) ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((i · (2
· π)) · -𝐾) = -((i · (2 · π))
· 𝐾)) | 
| 35 | 14, 1, 34 | sylancr 587 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → ((i
· (2 · π)) · -𝐾) = -((i · (2 · π))
· 𝐾)) | 
| 36 | 31, 33, 35 | 3eqtr4d 2786 | . . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (-i
· (𝐾 · (2
· π))) = ((i · (2 · π)) · -𝐾)) | 
| 37 | 36 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (-i
· (𝐾 · (2
· π))) = ((i · (2 · π)) · -𝐾)) | 
| 38 | 37 | oveq2d 7448 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → ((-i
· 𝐴) + (-i ·
(𝐾 · (2 ·
π)))) = ((-i · 𝐴)
+ ((i · (2 · π)) · -𝐾))) | 
| 39 | 30, 38 | eqtrd 2776 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (-i
· (𝐴 + (𝐾 · (2 · π)))) =
((-i · 𝐴) + ((i
· (2 · π)) · -𝐾))) | 
| 40 | 39 | fveq2d 6909 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(exp‘(-i · (𝐴
+ (𝐾 · (2 ·
π))))) = (exp‘((-i · 𝐴) + ((i · (2 · π)) ·
-𝐾)))) | 
| 41 |  | mulcl 11240 | . . . . . . 7
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) | 
| 42 | 27, 41 | mpan 690 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (-i
· 𝐴) ∈
ℂ) | 
| 43 |  | znegcl 12654 | . . . . . 6
⊢ (𝐾 ∈ ℤ → -𝐾 ∈
ℤ) | 
| 44 |  | efper 26522 | . . . . . 6
⊢ (((-i
· 𝐴) ∈ ℂ
∧ -𝐾 ∈ ℤ)
→ (exp‘((-i · 𝐴) + ((i · (2 · π)) ·
-𝐾))) = (exp‘(-i
· 𝐴))) | 
| 45 | 42, 43, 44 | syl2an 596 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(exp‘((-i · 𝐴)
+ ((i · (2 · π)) · -𝐾))) = (exp‘(-i · 𝐴))) | 
| 46 | 40, 45 | eqtrd 2776 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(exp‘(-i · (𝐴
+ (𝐾 · (2 ·
π))))) = (exp‘(-i · 𝐴))) | 
| 47 | 26, 46 | oveq12d 7450 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
((exp‘(i · (𝐴
+ (𝐾 · (2 ·
π)))))𝑂(exp‘(-i
· (𝐴 + (𝐾 · (2 · π))))))
= ((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴)))) | 
| 48 | 47 | oveq1d 7447 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(((exp‘(i · (𝐴
+ (𝐾 · (2 ·
π)))))𝑂(exp‘(-i
· (𝐴 + (𝐾 · (2 · π))))))
/ 𝐷) = (((exp‘(i
· 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷)) | 
| 49 |  | addcl 11238 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝐾 · (2 · π))
∈ ℂ) → (𝐴 +
(𝐾 · (2 ·
π))) ∈ ℂ) | 
| 50 | 6, 49 | sylan2 593 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐴 + (𝐾 · (2 · π))) ∈
ℂ) | 
| 51 |  | sinperlem.2 | . . 3
⊢ ((𝐴 + (𝐾 · (2 · π))) ∈ ℂ
→ (𝐹‘(𝐴 + (𝐾 · (2 · π)))) =
(((exp‘(i · (𝐴
+ (𝐾 · (2 ·
π)))))𝑂(exp‘(-i
· (𝐴 + (𝐾 · (2 · π))))))
/ 𝐷)) | 
| 52 | 50, 51 | syl 17 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) =
(((exp‘(i · (𝐴
+ (𝐾 · (2 ·
π)))))𝑂(exp‘(-i
· (𝐴 + (𝐾 · (2 · π))))))
/ 𝐷)) | 
| 53 |  | sinperlem.1 | . . 3
⊢ (𝐴 ∈ ℂ → (𝐹‘𝐴) = (((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷)) | 
| 54 | 53 | adantr 480 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘𝐴) = (((exp‘(i · 𝐴))𝑂(exp‘(-i · 𝐴))) / 𝐷)) | 
| 55 | 48, 52, 54 | 3eqtr4d 2786 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐹‘(𝐴 + (𝐾 · (2 · π)))) = (𝐹‘𝐴)) |