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 ) )