# 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 ${⊢}{N}\in ℤ\to {\int }_{\left(0,1\right)}{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }{N}{x}}d{x}=if\left({N}=0,1,0\right)$

### Proof

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