This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgexpif

Description: The basis for the circle method in the form of trigonometric sums. Proposition of Nathanson p. 123. (Contributed by Thierry Arnoux, 2-Dec-2021)

Ref Expression
Assertion itgexpif ( 𝑁 ∈ ℤ → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = if ( 𝑁 = 0 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑥 ) = ( 0 · 𝑥 ) )
2 1 oveq2d ⊢ ( 𝑁 = 0 → ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) = ( ( i · ( 2 · π ) ) · ( 0 · 𝑥 ) ) )
3 2 fveq2d ⊢ ( 𝑁 = 0 → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 0 · 𝑥 ) ) ) )
4 ioossre ⊢ ( 0 (,) 1 ) ⊆ ℝ
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 4 5 sstri ⊢ ( 0 (,) 1 ) ⊆ ℂ
7 6 sseli ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → 𝑥 ∈ ℂ )
8 7 mul02d ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → ( 0 · 𝑥 ) = 0 )
9 8 oveq2d ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → ( ( i · ( 2 · π ) ) · ( 0 · 𝑥 ) ) = ( ( i · ( 2 · π ) ) · 0 ) )
10 ax-icn ⊢ i ∈ ℂ
11 2cn ⊢ 2 ∈ ℂ
12 picn ⊢ π ∈ ℂ
13 11 12 mulcli ⊢ ( 2 · π ) ∈ ℂ
14 10 13 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
15 14 mul01i ⊢ ( ( i · ( 2 · π ) ) · 0 ) = 0
16 9 15 eqtrdi ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → ( ( i · ( 2 · π ) ) · ( 0 · 𝑥 ) ) = 0 )
17 16 fveq2d ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 0 · 𝑥 ) ) ) = ( exp ‘ 0 ) )
18 ef0 ⊢ ( exp ‘ 0 ) = 1
19 17 18 eqtrdi ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 0 · 𝑥 ) ) ) = 1 )
20 3 19 sylan9eq ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) = 1 )
21 20 ralrimiva ⊢ ( 𝑁 = 0 → ∀ 𝑥 ∈ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) = 1 )
22 itgeq2 ⊢ ( ∀ 𝑥 ∈ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) = 1 → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) 1 d 𝑥 )
23 21 22 syl ⊢ ( 𝑁 = 0 → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) 1 d 𝑥 )
24 ioombl ⊢ ( 0 (,) 1 ) ∈ dom vol
25 0re ⊢ 0 ∈ ℝ
26 1re ⊢ 1 ∈ ℝ
27 ioovolcl ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( vol ‘ ( 0 (,) 1 ) ) ∈ ℝ )
28 25 26 27 mp2an ⊢ ( vol ‘ ( 0 (,) 1 ) ) ∈ ℝ
29 ax-1cn ⊢ 1 ∈ ℂ
30 itgconst ⊢ ( ( ( 0 (,) 1 ) ∈ dom vol ∧ ( vol ‘ ( 0 (,) 1 ) ) ∈ ℝ ∧ 1 ∈ ℂ ) → ∫ ( 0 (,) 1 ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) 1 ) ) ) )
31 24 28 29 30 mp3an ⊢ ∫ ( 0 (,) 1 ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) 1 ) ) )
32 0le1 ⊢ 0 ≤ 1
33 volioo ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1 ) → ( vol ‘ ( 0 (,) 1 ) ) = ( 1 − 0 ) )
34 25 26 32 33 mp3an ⊢ ( vol ‘ ( 0 (,) 1 ) ) = ( 1 − 0 )
35 29 subid1i ⊢ ( 1 − 0 ) = 1
36 34 35 eqtri ⊢ ( vol ‘ ( 0 (,) 1 ) ) = 1
37 36 oveq2i ⊢ ( 1 · ( vol ‘ ( 0 (,) 1 ) ) ) = ( 1 · 1 )
38 29 mulridi ⊢ ( 1 · 1 ) = 1
39 31 37 38 3eqtri ⊢ ∫ ( 0 (,) 1 ) 1 d 𝑥 = 1
40 23 39 eqtrdi ⊢ ( 𝑁 = 0 → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = 1 )
41 40 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 = 0 ) → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = 1 )
42 41 eqcomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 = 0 ) → 1 = ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
43 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
44 43 eqcomi ⊢ ℝ = ( -∞ (,) +∞ )
45 0red ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 0 ∈ ℝ )
46 1red ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 1 ∈ ℝ )
47 32 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 0 ≤ 1 )
48 5 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ℝ ⊆ ℂ )
49 48 sselda ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
50 10 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → i ∈ ℂ )
51 2cnd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 2 ∈ ℂ )
52 12 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → π ∈ ℂ )
53 51 52 mulcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 2 · π ) ∈ ℂ )
54 50 53 mulcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( i · ( 2 · π ) ) ∈ ℂ )
55 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 𝑁 ∈ ℤ )
56 55 zcnd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 𝑁 ∈ ℂ )
57 54 56 mulcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ∈ ℂ )
58 57 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ∈ ℂ )
59 simpr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
60 58 59 mulcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℂ ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ∈ ℂ )
61 60 efcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℂ ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ℂ )
62 49 61 syldan ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ℂ )
63 57 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ∈ ℂ )
64 ine0 ⊢ i ≠ 0
65 2ne0 ⊢ 2 ≠ 0
66 pipos ⊢ 0 < π
67 25 66 gtneii ⊢ π ≠ 0
68 11 12 65 67 mulne0i ⊢ ( 2 · π ) ≠ 0
69 10 13 64 68 mulne0i ⊢ ( i · ( 2 · π ) ) ≠ 0
70 69 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( i · ( 2 · π ) ) ≠ 0 )
71 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ¬ 𝑁 = 0 )
72 71 neqned ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 𝑁 ≠ 0 )
73 54 56 70 72 mulne0d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ≠ 0 )
74 73 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ≠ 0 )
75 62 63 74 divcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ∈ ℂ )
76 75 fmpttd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) : ℝ ⟶ ℂ )
77 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
78 77 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ℝ ∈ { ℝ , ℂ } )
79 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
80 79 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ℂ ∈ { ℝ , ℂ } )
81 63 49 mulcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ∈ ℂ )
82 simpr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
83 82 efcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑧 ∈ ℂ ) → ( exp ‘ 𝑧 ) ∈ ℂ )
84 57 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑧 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ∈ ℂ )
85 73 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑧 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ≠ 0 )
86 83 84 85 divcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑧 ∈ ℂ ) → ( ( exp ‘ 𝑧 ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ∈ ℂ )
87 26 a1i ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℝ )
88 78 dvmptid ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
89 78 49 87 88 57 dvmptcmul ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) )
90 63 mulridd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) = ( ( i · ( 2 · π ) ) · 𝑁 ) )
91 90 mpteq2dva ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) = ( 𝑦 ∈ ℝ ↦ ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
92 89 91 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
93 dvef ⊢ ( ℂ D exp ) = exp
94 eff ⊢ exp : ℂ ⟶ ℂ
95 94 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → exp : ℂ ⟶ ℂ )
96 95 feqmptd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → exp = ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑧 ) ) )
97 96 oveq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℂ D exp ) = ( ℂ D ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑧 ) ) ) )
98 93 97 96 3eqtr3a ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( exp ‘ 𝑧 ) ) )
99 80 83 83 98 57 73 dvmptdivc ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( ( exp ‘ 𝑧 ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( exp ‘ 𝑧 ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) )
100 fveq2 ⊢ ( 𝑧 = ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) → ( exp ‘ 𝑧 ) = ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) )
101 100 oveq1d ⊢ ( 𝑧 = ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) → ( ( exp ‘ 𝑧 ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) = ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
102 78 80 81 63 86 86 92 99 101 101 dvmptco ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) · ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) )
103 62 63 74 divcan1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) · ( ( i · ( 2 · π ) ) · 𝑁 ) ) = ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) )
104 103 mpteq2dva ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) · ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) )
105 102 104 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) )
106 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
107 106 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → exp ∈ ( ℂ –cn→ ℂ ) )
108 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) )
109 5 108 mp1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ↾ ℝ ) = ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) )
110 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) )
111 110 mulc1cncf ⊢ ( ( ( i · ( 2 · π ) ) · 𝑁 ) ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) )
112 57 111 syl ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) )
113 rescncf ⊢ ( ℝ ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) )
114 5 113 mp1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) ) )
115 112 114 mpd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℂ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ↾ ℝ ) ∈ ( ℝ –cn→ ℂ ) )
116 109 115 eqeltrrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ∈ ( ℝ –cn→ ℂ ) )
117 107 116 cncfmpt1f ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
118 105 117 eqeltrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) ∈ ( ℝ –cn→ ℂ ) )
119 44 45 46 47 76 118 ftc2re ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 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 ⊢ ( 𝑥 ∈ ( 0 (,) 1 ) → 𝑥 ∈ ℝ )
121 105 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) )
122 121 fveq1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) ‘ 𝑥 ) )
123 oveq2 ⊢ ( 𝑦 = 𝑥 → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) = ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) )
124 123 fveq2d ⊢ ( 𝑦 = 𝑥 → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) = ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ) )
125 124 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ) )
126 125 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ) ) )
127 57 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( i · ( 2 · π ) ) · 𝑁 ) ∈ ℂ )
128 48 sselda ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
129 127 128 mulcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ∈ ℂ )
130 129 efcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ) ∈ ℂ )
131 126 130 fvmpt2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) ‘ 𝑥 ) = ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ) )
132 14 a1i ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( i · ( 2 · π ) ) ∈ ℂ )
133 56 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → 𝑁 ∈ ℂ )
134 132 133 128 mulassd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) = ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) )
135 134 fveq2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑥 ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) )
136 131 135 eqtrd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) ) ‘ 𝑥 ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) )
137 122 136 eqtrd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) ‘ 𝑥 ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) )
138 120 137 sylan2 ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) ‘ 𝑥 ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) )
139 138 ralrimiva ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ∀ 𝑥 ∈ ( 0 (,) 1 ) ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) ‘ 𝑥 ) = ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) )
140 itgeq2 ⊢ ( ∀ 𝑥 ∈ ( 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 ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ∫ ( 0 (,) 1 ) ( ( ℝ D ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
142 eqidd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) )
143 simpr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 1 ) → 𝑦 = 1 )
144 143 oveq2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 1 ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) = ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) )
145 144 fveq2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 1 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) = ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) )
146 145 oveq1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 1 ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) = ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
147 29 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 1 ∈ ℂ )
148 57 147 mulcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ∈ ℂ )
149 148 efcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) ∈ ℂ )
150 149 57 73 divcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ∈ ℂ )
151 142 146 46 150 fvmptd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 1 ) = ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
152 57 mulridd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) = ( ( i · ( 2 · π ) ) · 𝑁 ) )
153 152 fveq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) = ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
154 ef2kpi ⊢ ( 𝑁 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑁 ) ) = 1 )
155 55 154 syl ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑁 ) ) = 1 )
156 153 155 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) = 1 )
157 156 oveq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 1 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) = ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
158 151 157 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 1 ) = ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
159 simpr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 0 ) → 𝑦 = 0 )
160 159 oveq2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 0 ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) = ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) )
161 160 fveq2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) = ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) )
162 161 oveq1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) ∧ 𝑦 = 0 ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) = ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
163 5 45 sselid ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 0 ∈ ℂ )
164 57 163 mulcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ∈ ℂ )
165 164 efcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) ∈ ℂ )
166 165 57 73 divcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ∈ ℂ )
167 142 162 45 166 fvmptd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 0 ) = ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
168 57 mul01d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) = 0 )
169 168 fveq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) = ( exp ‘ 0 ) )
170 169 18 eqtrdi ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) = 1 )
171 170 oveq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 0 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) = ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
172 167 171 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 0 ) = ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) )
173 158 172 oveq12d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 1 ) − ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 0 ) ) = ( ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) − ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) )
174 157 150 eqeltrrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ∈ ℂ )
175 174 subidd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) − ( 1 / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) = 0 )
176 173 175 eqtrd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ( ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 1 ) − ( ( 𝑦 ∈ ℝ ↦ ( ( exp ‘ ( ( ( i · ( 2 · π ) ) · 𝑁 ) · 𝑦 ) ) / ( ( i · ( 2 · π ) ) · 𝑁 ) ) ) ‘ 0 ) ) = 0 )
177 119 141 176 3eqtr3d ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = 0 )
178 177 eqcomd ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 = 0 ) → 0 = ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
179 42 178 ifeqda ⊢ ( 𝑁 ∈ ℤ → if ( 𝑁 = 0 , 1 , 0 ) = ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
180 179 eqcomd ⊢ ( 𝑁 ∈ ℤ → ∫ ( 0 (,) 1 ) ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑁 · 𝑥 ) ) ) d 𝑥 = if ( 𝑁 = 0 , 1 , 0 ) )