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 0 1 e i 2 π N x dx = if N = 0 1 0

Proof

Step Hyp Ref Expression
1 oveq1 N = 0 N x = 0 x
2 1 oveq2d N = 0 i 2 π N x = i 2 π 0 x
3 2 fveq2d N = 0 e i 2 π N x = e i 2 π 0 x
4 ioossre 0 1
5 ax-resscn
6 4 5 sstri 0 1
7 6 sseli x 0 1 x
8 7 mul02d x 0 1 0 x = 0
9 8 oveq2d x 0 1 i 2 π 0 x = 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 syl6eq x 0 1 i 2 π 0 x = 0
17 16 fveq2d x 0 1 e i 2 π 0 x = e 0
18 ef0 e 0 = 1
19 17 18 syl6eq x 0 1 e i 2 π 0 x = 1
20 3 19 sylan9eq N = 0 x 0 1 e i 2 π N x = 1
21 20 ralrimiva N = 0 x 0 1 e i 2 π N x = 1
22 itgeq2 x 0 1 e i 2 π N x = 1 0 1 e i 2 π N x dx = 0 1 1 dx
23 21 22 syl N = 0 0 1 e i 2 π N x dx = 0 1 1 dx
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 dx = 1 vol 0 1
31 24 28 29 30 mp3an 0 1 1 dx = 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 mulid1i 1 1 = 1
39 31 37 38 3eqtri 0 1 1 dx = 1
40 23 39 syl6eq N = 0 0 1 e i 2 π N x dx = 1
41 40 adantl N N = 0 0 1 e i 2 π N x dx = 1
42 41 eqcomd N N = 0 1 = 0 1 e i 2 π N x dx
43 ioomax −∞ +∞ =
44 43 eqcomi = −∞ +∞
45 0red N ¬ N = 0 0
46 1red N ¬ N = 0 1
47 32 a1i N ¬ N = 0 0 1
48 5 a1i N ¬ N = 0
49 48 sselda N ¬ N = 0 y y
50 10 a1i N ¬ N = 0 i
51 2cnd N ¬ N = 0 2
52 12 a1i N ¬ N = 0 π
53 51 52 mulcld N ¬ N = 0 2 π
54 50 53 mulcld N ¬ N = 0 i 2 π
55 simpl N ¬ N = 0 N
56 55 zcnd N ¬ N = 0 N
57 54 56 mulcld N ¬ N = 0 i 2 π N
58 57 adantr N ¬ N = 0 y i 2 π N
59 simpr N ¬ N = 0 y y
60 58 59 mulcld N ¬ N = 0 y i 2 π N y
61 60 efcld N ¬ N = 0 y e i 2 π N y
62 49 61 syldan N ¬ N = 0 y e i 2 π N y
63 57 adantr N ¬ N = 0 y i 2 π N
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 N ¬ N = 0 i 2 π 0
71 simpr N ¬ N = 0 ¬ N = 0
72 71 neqned N ¬ N = 0 N 0
73 54 56 70 72 mulne0d N ¬ N = 0 i 2 π N 0
74 73 adantr N ¬ N = 0 y i 2 π N 0
75 62 63 74 divcld N ¬ N = 0 y e i 2 π N y i 2 π N
76 75 fmpttd N ¬ N = 0 y e i 2 π N y i 2 π N :
77 reelprrecn
78 77 a1i N ¬ N = 0
79 cnelprrecn
80 79 a1i N ¬ N = 0
81 63 49 mulcld N ¬ N = 0 y i 2 π N y
82 simpr N ¬ N = 0 z z
83 82 efcld N ¬ N = 0 z e z
84 57 adantr N ¬ N = 0 z i 2 π N
85 73 adantr N ¬ N = 0 z i 2 π N 0
86 83 84 85 divcld N ¬ N = 0 z e z i 2 π N
87 26 a1i N ¬ N = 0 y 1
88 78 dvmptid N ¬ N = 0 dy y d y = y 1
89 78 49 87 88 57 dvmptcmul N ¬ N = 0 dy i 2 π N y d y = y i 2 π N 1
90 63 mulid1d N ¬ N = 0 y i 2 π N 1 = i 2 π N
91 90 mpteq2dva N ¬ N = 0 y i 2 π N 1 = y i 2 π N
92 89 91 eqtrd N ¬ N = 0 dy i 2 π N y d y = y i 2 π N
93 dvef D exp = exp
94 eff exp :
95 94 a1i N ¬ N = 0 exp :
96 95 feqmptd N ¬ N = 0 exp = z e z
97 96 oveq2d N ¬ N = 0 D exp = dz e z d z
98 93 97 96 3eqtr3a N ¬ N = 0 dz e z d z = z e z
99 80 83 83 98 57 73 dvmptdivc N ¬ N = 0 dz e z i 2 π N d z = z e z i 2 π N
100 fveq2 z = i 2 π N y e z = e i 2 π N y
101 100 oveq1d z = i 2 π N y e z i 2 π N = e i 2 π N y i 2 π N
102 78 80 81 63 86 86 92 99 101 101 dvmptco N ¬ N = 0 dy e i 2 π N y i 2 π N d y = y e i 2 π N y i 2 π N i 2 π N
103 62 63 74 divcan1d N ¬ N = 0 y e i 2 π N y i 2 π N i 2 π N = e i 2 π N y
104 103 mpteq2dva N ¬ N = 0 y e i 2 π N y i 2 π N i 2 π N = y e i 2 π N y
105 102 104 eqtrd N ¬ N = 0 dy e i 2 π N y i 2 π N d y = y e i 2 π N y
106 efcn exp : cn
107 106 a1i N ¬ N = 0 exp : cn
108 resmpt y i 2 π N y = y i 2 π N y
109 5 108 mp1i N ¬ N = 0 y i 2 π N y = y i 2 π N y
110 eqid y i 2 π N y = y i 2 π N y
111 110 mulc1cncf i 2 π N y i 2 π N y : cn
112 57 111 syl N ¬ N = 0 y i 2 π N y : cn
113 rescncf y i 2 π N y : cn y i 2 π N y : cn
114 5 113 mp1i N ¬ N = 0 y i 2 π N y : cn y i 2 π N y : cn
115 112 114 mpd N ¬ N = 0 y i 2 π N y : cn
116 109 115 eqeltrrd N ¬ N = 0 y i 2 π N y : cn
117 107 116 cncfmpt1f N ¬ N = 0 y e i 2 π N y : cn
118 105 117 eqeltrd N ¬ N = 0 dy e i 2 π N y i 2 π N d y : cn
119 44 45 46 47 76 118 ftc2re N ¬ N = 0 0 1 dy e i 2 π N y i 2 π N d y x dx = y e i 2 π N y i 2 π N 1 y e i 2 π N y i 2 π N 0
120 4 sseli x 0 1 x
121 105 adantr N ¬ N = 0 x dy e i 2 π N y i 2 π N d y = y e i 2 π N y
122 121 fveq1d N ¬ N = 0 x dy e i 2 π N y i 2 π N d y x = y e i 2 π N y x
123 oveq2 y = x i 2 π N y = i 2 π N x
124 123 fveq2d y = x e i 2 π N y = e i 2 π N x
125 124 cbvmptv y e i 2 π N y = x e i 2 π N x
126 125 a1i N ¬ N = 0 y e i 2 π N y = x e i 2 π N x
127 57 adantr N ¬ N = 0 x i 2 π N
128 48 sselda N ¬ N = 0 x x
129 127 128 mulcld N ¬ N = 0 x i 2 π N x
130 129 efcld N ¬ N = 0 x e i 2 π N x
131 126 130 fvmpt2d N ¬ N = 0 x y e i 2 π N y x = e i 2 π N x
132 14 a1i N ¬ N = 0 x i 2 π
133 56 adantr N ¬ N = 0 x N
134 132 133 128 mulassd N ¬ N = 0 x i 2 π N x = i 2 π N x
135 134 fveq2d N ¬ N = 0 x e i 2 π N x = e i 2 π N x
136 131 135 eqtrd N ¬ N = 0 x y e i 2 π N y x = e i 2 π N x
137 122 136 eqtrd N ¬ N = 0 x dy e i 2 π N y i 2 π N d y x = e i 2 π N x
138 120 137 sylan2 N ¬ N = 0 x 0 1 dy e i 2 π N y i 2 π N d y x = e i 2 π N x
139 138 ralrimiva N ¬ N = 0 x 0 1 dy e i 2 π N y i 2 π N d y x = e i 2 π N x
140 itgeq2 x 0 1 dy e i 2 π N y i 2 π N d y x = e i 2 π N x 0 1 dy e i 2 π N y i 2 π N d y x dx = 0 1 e i 2 π N x dx
141 139 140 syl N ¬ N = 0 0 1 dy e i 2 π N y i 2 π N d y x dx = 0 1 e i 2 π N x dx
142 eqidd N ¬ N = 0 y e i 2 π N y i 2 π N = y e i 2 π N y i 2 π N
143 simpr N ¬ N = 0 y = 1 y = 1
144 143 oveq2d N ¬ N = 0 y = 1 i 2 π N y = i 2 π N 1
145 144 fveq2d N ¬ N = 0 y = 1 e i 2 π N y = e i 2 π N 1
146 145 oveq1d N ¬ N = 0 y = 1 e i 2 π N y i 2 π N = e i 2 π N 1 i 2 π N
147 29 a1i N ¬ N = 0 1
148 57 147 mulcld N ¬ N = 0 i 2 π N 1
149 148 efcld N ¬ N = 0 e i 2 π N 1
150 149 57 73 divcld N ¬ N = 0 e i 2 π N 1 i 2 π N
151 142 146 46 150 fvmptd N ¬ N = 0 y e i 2 π N y i 2 π N 1 = e i 2 π N 1 i 2 π N
152 57 mulid1d N ¬ N = 0 i 2 π N 1 = i 2 π N
153 152 fveq2d N ¬ N = 0 e i 2 π N 1 = e i 2 π N
154 ef2kpi N e i 2 π N = 1
155 55 154 syl N ¬ N = 0 e i 2 π N = 1
156 153 155 eqtrd N ¬ N = 0 e i 2 π N 1 = 1
157 156 oveq1d N ¬ N = 0 e i 2 π N 1 i 2 π N = 1 i 2 π N
158 151 157 eqtrd N ¬ N = 0 y e i 2 π N y i 2 π N 1 = 1 i 2 π N
159 simpr N ¬ N = 0 y = 0 y = 0
160 159 oveq2d N ¬ N = 0 y = 0 i 2 π N y = i 2 π N 0
161 160 fveq2d N ¬ N = 0 y = 0 e i 2 π N y = e i 2 π N 0
162 161 oveq1d N ¬ N = 0 y = 0 e i 2 π N y i 2 π N = e i 2 π N 0 i 2 π N
163 5 45 sseldi N ¬ N = 0 0
164 57 163 mulcld N ¬ N = 0 i 2 π N 0
165 164 efcld N ¬ N = 0 e i 2 π N 0
166 165 57 73 divcld N ¬ N = 0 e i 2 π N 0 i 2 π N
167 142 162 45 166 fvmptd N ¬ N = 0 y e i 2 π N y i 2 π N 0 = e i 2 π N 0 i 2 π N
168 57 mul01d N ¬ N = 0 i 2 π N 0 = 0
169 168 fveq2d N ¬ N = 0 e i 2 π N 0 = e 0
170 169 18 syl6eq N ¬ N = 0 e i 2 π N 0 = 1
171 170 oveq1d N ¬ N = 0 e i 2 π N 0 i 2 π N = 1 i 2 π N
172 167 171 eqtrd N ¬ N = 0 y e i 2 π N y i 2 π N 0 = 1 i 2 π N
173 158 172 oveq12d N ¬ N = 0 y e i 2 π N y i 2 π N 1 y e i 2 π N y i 2 π N 0 = 1 i 2 π N 1 i 2 π N
174 157 150 eqeltrrd N ¬ N = 0 1 i 2 π N
175 174 subidd N ¬ N = 0 1 i 2 π N 1 i 2 π N = 0
176 173 175 eqtrd N ¬ N = 0 y e i 2 π N y i 2 π N 1 y e i 2 π N y i 2 π N 0 = 0
177 119 141 176 3eqtr3d N ¬ N = 0 0 1 e i 2 π N x dx = 0
178 177 eqcomd N ¬ N = 0 0 = 0 1 e i 2 π N x dx
179 42 178 ifeqda N if N = 0 1 0 = 0 1 e i 2 π N x dx
180 179 eqcomd N 0 1 e i 2 π N x dx = if N = 0 1 0