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_{(0, 1)} e^{i 2 π N x} d x = if (N = 0, 1, 0)$

Proof

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

Metamath Proof Explorer

Theorem itgexpif

Proof