Step | Hyp | Ref
| Expression |
1 | | oveq1 7177 |
. . . . . . . . . . 11
⊢ (𝑁 = 0 → (𝑁 · 𝑥) = (0 · 𝑥)) |
2 | 1 | oveq2d 7186 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → ((i · (2
· π)) · (𝑁
· 𝑥)) = ((i ·
(2 · π)) · (0 · 𝑥))) |
3 | 2 | fveq2d 6678 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (exp‘((i
· (2 · π)) · (𝑁 · 𝑥))) = (exp‘((i · (2 ·
π)) · (0 · 𝑥)))) |
4 | | ioossre 12882 |
. . . . . . . . . . . . . . . 16
⊢ (0(,)1)
⊆ ℝ |
5 | | ax-resscn 10672 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℂ |
6 | 4, 5 | sstri 3886 |
. . . . . . . . . . . . . . 15
⊢ (0(,)1)
⊆ ℂ |
7 | 6 | sseli 3873 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0(,)1) → 𝑥 ∈
ℂ) |
8 | 7 | mul02d 10916 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0(,)1) → (0
· 𝑥) =
0) |
9 | 8 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0(,)1) → ((i
· (2 · π)) · (0 · 𝑥)) = ((i · (2 · π)) ·
0)) |
10 | | ax-icn 10674 |
. . . . . . . . . . . . . 14
⊢ i ∈
ℂ |
11 | | 2cn 11791 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
12 | | picn 25204 |
. . . . . . . . . . . . . . 15
⊢ π
∈ ℂ |
13 | 11, 12 | mulcli 10726 |
. . . . . . . . . . . . . 14
⊢ (2
· π) ∈ ℂ |
14 | 10, 13 | mulcli 10726 |
. . . . . . . . . . . . 13
⊢ (i
· (2 · π)) ∈ ℂ |
15 | 14 | mul01i 10908 |
. . . . . . . . . . . 12
⊢ ((i
· (2 · π)) · 0) = 0 |
16 | 9, 15 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0(,)1) → ((i
· (2 · π)) · (0 · 𝑥)) = 0) |
17 | 16 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0(,)1) →
(exp‘((i · (2 · π)) · (0 · 𝑥))) =
(exp‘0)) |
18 | | ef0 15536 |
. . . . . . . . . 10
⊢
(exp‘0) = 1 |
19 | 17, 18 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0(,)1) →
(exp‘((i · (2 · π)) · (0 · 𝑥))) = 1) |
20 | 3, 19 | sylan9eq 2793 |
. . . . . . . 8
⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · (𝑁 · 𝑥))) = 1) |
21 | 20 | ralrimiva 3096 |
. . . . . . 7
⊢ (𝑁 = 0 → ∀𝑥 ∈ (0(,)1)(exp‘((i
· (2 · π)) · (𝑁 · 𝑥))) = 1) |
22 | | itgeq2 24530 |
. . . . . . 7
⊢
(∀𝑥 ∈
(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) = 1 → ∫(0(,)1)(exp‘((i
· (2 · π)) · (𝑁 · 𝑥))) d𝑥 = ∫(0(,)1)1 d𝑥) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (𝑁 = 0 →
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = ∫(0(,)1)1 d𝑥) |
24 | | ioombl 24317 |
. . . . . . . 8
⊢ (0(,)1)
∈ dom vol |
25 | | 0re 10721 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
26 | | 1re 10719 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
27 | | ioovolcl 24322 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → (vol‘(0(,)1)) ∈
ℝ) |
28 | 25, 26, 27 | mp2an 692 |
. . . . . . . 8
⊢
(vol‘(0(,)1)) ∈ ℝ |
29 | | ax-1cn 10673 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
30 | | itgconst 24571 |
. . . . . . . 8
⊢ (((0(,)1)
∈ dom vol ∧ (vol‘(0(,)1)) ∈ ℝ ∧ 1 ∈ ℂ)
→ ∫(0(,)1)1 d𝑥 =
(1 · (vol‘(0(,)1)))) |
31 | 24, 28, 29, 30 | mp3an 1462 |
. . . . . . 7
⊢
∫(0(,)1)1 d𝑥 =
(1 · (vol‘(0(,)1))) |
32 | | 0le1 11241 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
33 | | volioo 24321 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) →
(vol‘(0(,)1)) = (1 − 0)) |
34 | 25, 26, 32, 33 | mp3an 1462 |
. . . . . . . . 9
⊢
(vol‘(0(,)1)) = (1 − 0) |
35 | 29 | subid1i 11036 |
. . . . . . . . 9
⊢ (1
− 0) = 1 |
36 | 34, 35 | eqtri 2761 |
. . . . . . . 8
⊢
(vol‘(0(,)1)) = 1 |
37 | 36 | oveq2i 7181 |
. . . . . . 7
⊢ (1
· (vol‘(0(,)1))) = (1 · 1) |
38 | 29 | mulid1i 10723 |
. . . . . . 7
⊢ (1
· 1) = 1 |
39 | 31, 37, 38 | 3eqtri 2765 |
. . . . . 6
⊢
∫(0(,)1)1 d𝑥 =
1 |
40 | 23, 39 | eqtrdi 2789 |
. . . . 5
⊢ (𝑁 = 0 →
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = 1) |
41 | 40 | adantl 485 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 = 0) →
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = 1) |
42 | 41 | eqcomd 2744 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 = 0) → 1 =
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥) |
43 | | ioomax 12896 |
. . . . . . 7
⊢
(-∞(,)+∞) = ℝ |
44 | 43 | eqcomi 2747 |
. . . . . 6
⊢ ℝ =
(-∞(,)+∞) |
45 | | 0red 10722 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 0 ∈
ℝ) |
46 | | 1red 10720 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 1 ∈
ℝ) |
47 | 32 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 0 ≤
1) |
48 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ℝ
⊆ ℂ) |
49 | 48 | sselda 3877 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) |
50 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → i ∈
ℂ) |
51 | | 2cnd 11794 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 2 ∈
ℂ) |
52 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → π ∈
ℂ) |
53 | 51, 52 | mulcld 10739 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (2 ·
π) ∈ ℂ) |
54 | 50, 53 | mulcld 10739 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (i ·
(2 · π)) ∈ ℂ) |
55 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 𝑁 ∈
ℤ) |
56 | 55 | zcnd 12169 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 𝑁 ∈
ℂ) |
57 | 54, 56 | mulcld 10739 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((i ·
(2 · π)) · 𝑁) ∈ ℂ) |
58 | 57 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℂ) → ((i
· (2 · π)) · 𝑁) ∈ ℂ) |
59 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
60 | 58, 59 | mulcld 10739 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℂ) → (((i
· (2 · π)) · 𝑁) · 𝑦) ∈ ℂ) |
61 | 60 | efcld 32141 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℂ) →
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) ∈ ℂ) |
62 | 49, 61 | syldan 594 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) →
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) ∈ ℂ) |
63 | 57 | adantr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) → ((i
· (2 · π)) · 𝑁) ∈ ℂ) |
64 | | ine0 11153 |
. . . . . . . . . . . 12
⊢ i ≠
0 |
65 | | 2ne0 11820 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
66 | | pipos 25205 |
. . . . . . . . . . . . . 14
⊢ 0 <
π |
67 | 25, 66 | gtneii 10830 |
. . . . . . . . . . . . 13
⊢ π ≠
0 |
68 | 11, 12, 65, 67 | mulne0i 11361 |
. . . . . . . . . . . 12
⊢ (2
· π) ≠ 0 |
69 | 10, 13, 64, 68 | mulne0i 11361 |
. . . . . . . . . . 11
⊢ (i
· (2 · π)) ≠ 0 |
70 | 69 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (i ·
(2 · π)) ≠ 0) |
71 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ¬ 𝑁 = 0) |
72 | 71 | neqned 2941 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 𝑁 ≠ 0) |
73 | 54, 56, 70, 72 | mulne0d 11370 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((i ·
(2 · π)) · 𝑁) ≠ 0) |
74 | 73 | adantr 484 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) → ((i
· (2 · π)) · 𝑁) ≠ 0) |
75 | 62, 63, 74 | divcld 11494 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) →
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)) ∈
ℂ) |
76 | 75 | fmpttd 6889 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))):ℝ⟶ℂ) |
77 | | reelprrecn 10707 |
. . . . . . . . . 10
⊢ ℝ
∈ {ℝ, ℂ} |
78 | 77 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ℝ
∈ {ℝ, ℂ}) |
79 | | cnelprrecn 10708 |
. . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} |
80 | 79 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ℂ
∈ {ℝ, ℂ}) |
81 | 63, 49 | mulcld 10739 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) → (((i
· (2 · π)) · 𝑁) · 𝑦) ∈ ℂ) |
82 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) |
83 | 82 | efcld 32141 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑧 ∈ ℂ) →
(exp‘𝑧) ∈
ℂ) |
84 | 57 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑧 ∈ ℂ) → ((i
· (2 · π)) · 𝑁) ∈ ℂ) |
85 | 73 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑧 ∈ ℂ) → ((i
· (2 · π)) · 𝑁) ≠ 0) |
86 | 83, 84, 85 | divcld 11494 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑧 ∈ ℂ) →
((exp‘𝑧) / ((i
· (2 · π)) · 𝑁)) ∈ ℂ) |
87 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) → 1 ∈
ℝ) |
88 | 78 | dvmptid 24709 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℝ D
(𝑦 ∈ ℝ ↦
𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
89 | 78, 49, 87, 88, 57 | dvmptcmul 24716 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℝ D
(𝑦 ∈ ℝ ↦
(((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑦 ∈ ℝ ↦ (((i · (2
· π)) · 𝑁)
· 1))) |
90 | 63 | mulid1d 10736 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) → (((i
· (2 · π)) · 𝑁) · 1) = ((i · (2 ·
π)) · 𝑁)) |
91 | 90 | mpteq2dva 5125 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦ (((i
· (2 · π)) · 𝑁) · 1)) = (𝑦 ∈ ℝ ↦ ((i · (2
· π)) · 𝑁))) |
92 | 89, 91 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℝ D
(𝑦 ∈ ℝ ↦
(((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑦 ∈ ℝ ↦ ((i · (2
· π)) · 𝑁))) |
93 | | dvef 24732 |
. . . . . . . . . . 11
⊢ (ℂ
D exp) = exp |
94 | | eff 15527 |
. . . . . . . . . . . . . 14
⊢
exp:ℂ⟶ℂ |
95 | 94 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
exp:ℂ⟶ℂ) |
96 | 95 | feqmptd 6737 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → exp = (𝑧 ∈ ℂ ↦
(exp‘𝑧))) |
97 | 96 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℂ D
exp) = (ℂ D (𝑧 ∈
ℂ ↦ (exp‘𝑧)))) |
98 | 93, 97, 96 | 3eqtr3a 2797 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℂ D
(𝑧 ∈ ℂ ↦
(exp‘𝑧))) = (𝑧 ∈ ℂ ↦
(exp‘𝑧))) |
99 | 80, 83, 83, 98, 57, 73 | dvmptdivc 24717 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℂ D
(𝑧 ∈ ℂ ↦
((exp‘𝑧) / ((i
· (2 · π)) · 𝑁)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑧) / ((i · (2 ·
π)) · 𝑁)))) |
100 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑧 = (((i · (2 ·
π)) · 𝑁) ·
𝑦) → (exp‘𝑧) = (exp‘(((i · (2
· π)) · 𝑁)
· 𝑦))) |
101 | 100 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝑧 = (((i · (2 ·
π)) · 𝑁) ·
𝑦) → ((exp‘𝑧) / ((i · (2 ·
π)) · 𝑁)) =
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))) |
102 | 78, 80, 81, 63, 86, 86, 92, 99, 101, 101 | dvmptco 24724 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℝ D
(𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))) = (𝑦 ∈ ℝ ↦ (((exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)) · ((i ·
(2 · π)) · 𝑁)))) |
103 | 62, 63, 74 | divcan1d 11495 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 ∈ ℝ) →
(((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)) · ((i ·
(2 · π)) · 𝑁)) = (exp‘(((i · (2 ·
π)) · 𝑁) ·
𝑦))) |
104 | 103 | mpteq2dva 5125 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦
(((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)) · ((i ·
(2 · π)) · 𝑁))) = (𝑦 ∈ ℝ ↦ (exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)))) |
105 | 102, 104 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℝ D
(𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))) = (𝑦 ∈ ℝ ↦ (exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)))) |
106 | | efcn 25190 |
. . . . . . . . 9
⊢ exp
∈ (ℂ–cn→ℂ) |
107 | 106 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → exp ∈
(ℂ–cn→ℂ)) |
108 | | resmpt 5879 |
. . . . . . . . . 10
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (((i · (2
· π)) · 𝑁)
· 𝑦))) |
109 | 5, 108 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℂ ↦ (((i
· (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) = (𝑦 ∈ ℝ ↦ (((i · (2
· π)) · 𝑁)
· 𝑦))) |
110 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ ↦ (((i
· (2 · π)) · 𝑁) · 𝑦)) = (𝑦 ∈ ℂ ↦ (((i · (2
· π)) · 𝑁)
· 𝑦)) |
111 | 110 | mulc1cncf 23657 |
. . . . . . . . . . 11
⊢ (((i
· (2 · π)) · 𝑁) ∈ ℂ → (𝑦 ∈ ℂ ↦ (((i · (2
· π)) · 𝑁)
· 𝑦)) ∈
(ℂ–cn→ℂ)) |
112 | 57, 111 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℂ ↦ (((i
· (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ)) |
113 | | rescncf 23649 |
. . . . . . . . . . 11
⊢ (ℝ
⊆ ℂ → ((𝑦
∈ ℂ ↦ (((i · (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ) → ((𝑦 ∈ ℂ ↦ (((i · (2
· π)) · 𝑁)
· 𝑦)) ↾
ℝ) ∈ (ℝ–cn→ℂ))) |
114 | 5, 113 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℂ ↦ (((i
· (2 · π)) · 𝑁) · 𝑦)) ∈ (ℂ–cn→ℂ) → ((𝑦 ∈ ℂ ↦ (((i · (2
· π)) · 𝑁)
· 𝑦)) ↾
ℝ) ∈ (ℝ–cn→ℂ))) |
115 | 112, 114 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℂ ↦ (((i
· (2 · π)) · 𝑁) · 𝑦)) ↾ ℝ) ∈
(ℝ–cn→ℂ)) |
116 | 109, 115 | eqeltrrd 2834 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦ (((i
· (2 · π)) · 𝑁) · 𝑦)) ∈ (ℝ–cn→ℂ)) |
117 | 107, 116 | cncfmpt1f 23666 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦))) ∈ (ℝ–cn→ℂ)) |
118 | 105, 117 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (ℝ D
(𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))) ∈
(ℝ–cn→ℂ)) |
119 | 44, 45, 46, 47, 76, 118 | ftc2re 32148 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
∫(0(,)1)((ℝ D (𝑦
∈ ℝ ↦ ((exp‘(((i · (2 · π)) ·
𝑁) · 𝑦)) / ((i · (2 ·
π)) · 𝑁))))‘𝑥) d𝑥 = (((𝑦 ∈ ℝ ↦ ((exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘1) −
((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘0))) |
120 | 4 | sseli 3873 |
. . . . . . . 8
⊢ (𝑥 ∈ (0(,)1) → 𝑥 ∈
ℝ) |
121 | 105 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (ℝ
D (𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))) = (𝑦 ∈ ℝ ↦ (exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)))) |
122 | 121 | fveq1d 6676 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) →
((ℝ D (𝑦 ∈
ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))))‘𝑥) = ((𝑦 ∈ ℝ ↦ (exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)))‘𝑥)) |
123 | | oveq2 7178 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((i · (2 · π))
· 𝑁) · 𝑦) = (((i · (2 ·
π)) · 𝑁) ·
𝑥)) |
124 | 123 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (exp‘(((i · (2 ·
π)) · 𝑁) ·
𝑦)) = (exp‘(((i
· (2 · π)) · 𝑁) · 𝑥))) |
125 | 124 | cbvmptv 5133 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ ↦
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑥 ∈ ℝ ↦ (exp‘(((i
· (2 · π)) · 𝑁) · 𝑥))) |
126 | 125 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦))) = (𝑥 ∈ ℝ ↦ (exp‘(((i
· (2 · π)) · 𝑁) · 𝑥)))) |
127 | 57 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((i
· (2 · π)) · 𝑁) ∈ ℂ) |
128 | 48 | sselda 3877 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℂ) |
129 | 127, 128 | mulcld 10739 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (((i
· (2 · π)) · 𝑁) · 𝑥) ∈ ℂ) |
130 | 129 | efcld 32141 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) →
(exp‘(((i · (2 · π)) · 𝑁) · 𝑥)) ∈ ℂ) |
131 | 126, 130 | fvmpt2d 6788 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((𝑦 ∈ ℝ ↦
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))‘𝑥) = (exp‘(((i · (2 ·
π)) · 𝑁) ·
𝑥))) |
132 | 14 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (i
· (2 · π)) ∈ ℂ) |
133 | 56 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → 𝑁 ∈
ℂ) |
134 | 132, 133,
128 | mulassd 10742 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → (((i
· (2 · π)) · 𝑁) · 𝑥) = ((i · (2 · π)) ·
(𝑁 · 𝑥))) |
135 | 134 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) →
(exp‘(((i · (2 · π)) · 𝑁) · 𝑥)) = (exp‘((i · (2 ·
π)) · (𝑁 ·
𝑥)))) |
136 | 131, 135 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) → ((𝑦 ∈ ℝ ↦
(exp‘(((i · (2 · π)) · 𝑁) · 𝑦)))‘𝑥) = (exp‘((i · (2 ·
π)) · (𝑁 ·
𝑥)))) |
137 | 122, 136 | eqtrd 2773 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ ℝ) →
((ℝ D (𝑦 ∈
ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))))‘𝑥) = (exp‘((i · (2
· π)) · (𝑁
· 𝑥)))) |
138 | 120, 137 | sylan2 596 |
. . . . . . 7
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑥 ∈ (0(,)1)) →
((ℝ D (𝑦 ∈
ℝ ↦ ((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))))‘𝑥) = (exp‘((i · (2
· π)) · (𝑁
· 𝑥)))) |
139 | 138 | ralrimiva 3096 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ∀𝑥 ∈ (0(,)1)((ℝ D
(𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))))‘𝑥) = (exp‘((i · (2
· π)) · (𝑁
· 𝑥)))) |
140 | | itgeq2 24530 |
. . . . . 6
⊢
(∀𝑥 ∈
(0(,)1)((ℝ D (𝑦
∈ ℝ ↦ ((exp‘(((i · (2 · π)) ·
𝑁) · 𝑦)) / ((i · (2 ·
π)) · 𝑁))))‘𝑥) = (exp‘((i · (2 ·
π)) · (𝑁 ·
𝑥))) →
∫(0(,)1)((ℝ D (𝑦
∈ ℝ ↦ ((exp‘(((i · (2 · π)) ·
𝑁) · 𝑦)) / ((i · (2 ·
π)) · 𝑁))))‘𝑥) d𝑥 = ∫(0(,)1)(exp‘((i · (2
· π)) · (𝑁
· 𝑥))) d𝑥) |
141 | 139, 140 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
∫(0(,)1)((ℝ D (𝑦
∈ ℝ ↦ ((exp‘(((i · (2 · π)) ·
𝑁) · 𝑦)) / ((i · (2 ·
π)) · 𝑁))))‘𝑥) d𝑥 = ∫(0(,)1)(exp‘((i · (2
· π)) · (𝑁
· 𝑥))) d𝑥) |
142 | | eqidd 2739 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁))) = (𝑦 ∈ ℝ ↦ ((exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))) |
143 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 1) → 𝑦 = 1) |
144 | 143 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 1) → (((i · (2
· π)) · 𝑁)
· 𝑦) = (((i ·
(2 · π)) · 𝑁) · 1)) |
145 | 144 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 1) → (exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) = (exp‘(((i · (2 ·
π)) · 𝑁) ·
1))) |
146 | 145 | oveq1d 7185 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 1) → ((exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)) = ((exp‘(((i
· (2 · π)) · 𝑁) · 1)) / ((i · (2 ·
π)) · 𝑁))) |
147 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 1 ∈
ℂ) |
148 | 57, 147 | mulcld 10739 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (((i ·
(2 · π)) · 𝑁) · 1) ∈
ℂ) |
149 | 148 | efcld 32141 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘(((i · (2 · π)) · 𝑁) · 1)) ∈
ℂ) |
150 | 149, 57, 73 | divcld 11494 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 ·
π)) · 𝑁)) ∈
ℂ) |
151 | 142, 146,
46, 150 | fvmptd 6782 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘1) =
((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 ·
π)) · 𝑁))) |
152 | 57 | mulid1d 10736 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (((i ·
(2 · π)) · 𝑁) · 1) = ((i · (2 ·
π)) · 𝑁)) |
153 | 152 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘(((i · (2 · π)) · 𝑁) · 1)) = (exp‘((i · (2
· π)) · 𝑁))) |
154 | | ef2kpi 25223 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ →
(exp‘((i · (2 · π)) · 𝑁)) = 1) |
155 | 55, 154 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘((i · (2 · π)) · 𝑁)) = 1) |
156 | 153, 155 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘(((i · (2 · π)) · 𝑁) · 1)) = 1) |
157 | 156 | oveq1d 7185 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
((exp‘(((i · (2 · π)) · 𝑁) · 1)) / ((i · (2 ·
π)) · 𝑁)) = (1 /
((i · (2 · π)) · 𝑁))) |
158 | 151, 157 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘1) = (1 / ((i
· (2 · π)) · 𝑁))) |
159 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 0) → 𝑦 = 0) |
160 | 159 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 0) → (((i · (2
· π)) · 𝑁)
· 𝑦) = (((i ·
(2 · π)) · 𝑁) · 0)) |
161 | 160 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 0) → (exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) = (exp‘(((i · (2 ·
π)) · 𝑁) ·
0))) |
162 | 161 | oveq1d 7185 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) ∧ 𝑦 = 0) → ((exp‘(((i
· (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)) = ((exp‘(((i
· (2 · π)) · 𝑁) · 0)) / ((i · (2 ·
π)) · 𝑁))) |
163 | 5, 45 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 0 ∈
ℂ) |
164 | 57, 163 | mulcld 10739 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (((i ·
(2 · π)) · 𝑁) · 0) ∈
ℂ) |
165 | 164 | efcld 32141 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘(((i · (2 · π)) · 𝑁) · 0)) ∈
ℂ) |
166 | 165, 57, 73 | divcld 11494 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 ·
π)) · 𝑁)) ∈
ℂ) |
167 | 142, 162,
45, 166 | fvmptd 6782 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘0) =
((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 ·
π)) · 𝑁))) |
168 | 57 | mul01d 10917 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (((i ·
(2 · π)) · 𝑁) · 0) = 0) |
169 | 168 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘(((i · (2 · π)) · 𝑁) · 0)) =
(exp‘0)) |
170 | 169, 18 | eqtrdi 2789 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
(exp‘(((i · (2 · π)) · 𝑁) · 0)) = 1) |
171 | 170 | oveq1d 7185 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
((exp‘(((i · (2 · π)) · 𝑁) · 0)) / ((i · (2 ·
π)) · 𝑁)) = (1 /
((i · (2 · π)) · 𝑁))) |
172 | 167, 171 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘0) = (1 / ((i
· (2 · π)) · 𝑁))) |
173 | 158, 172 | oveq12d 7188 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘1) −
((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘0)) = ((1 / ((i
· (2 · π)) · 𝑁)) − (1 / ((i · (2 ·
π)) · 𝑁)))) |
174 | 157, 150 | eqeltrrd 2834 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (1 / ((i
· (2 · π)) · 𝑁)) ∈ ℂ) |
175 | 174 | subidd 11063 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → ((1 / ((i
· (2 · π)) · 𝑁)) − (1 / ((i · (2 ·
π)) · 𝑁))) =
0) |
176 | 173, 175 | eqtrd 2773 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → (((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘1) −
((𝑦 ∈ ℝ ↦
((exp‘(((i · (2 · π)) · 𝑁) · 𝑦)) / ((i · (2 · π)) ·
𝑁)))‘0)) =
0) |
177 | 119, 141,
176 | 3eqtr3d 2781 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) →
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = 0) |
178 | 177 | eqcomd 2744 |
. . 3
⊢ ((𝑁 ∈ ℤ ∧ ¬
𝑁 = 0) → 0 =
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥) |
179 | 42, 178 | ifeqda 4450 |
. 2
⊢ (𝑁 ∈ ℤ → if(𝑁 = 0, 1, 0) =
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥) |
180 | 179 | eqcomd 2744 |
1
⊢ (𝑁 ∈ ℤ →
∫(0(,)1)(exp‘((i · (2 · π)) · (𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, 1, 0)) |