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 
|- ( N e. ZZ -> S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( N x. x ) ) ) _d x = if ( N = 0 , 1 , 0 ) )

Proof

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