Theorem dirkerper 32124

Description: the Dirichlet Kernel has period 2 pi. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
dirkerper.1	|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
dirkerper.2	|- T = ( 2 x. pi )

Assertion

Ref	Expression
dirkerper	|- ( ( N e. NN /\ x e. RR ) -> ( ( D ` N ) ` ( x + T ) ) = ( ( D ` N ) ` x ) )

Distinct variable groups:   y, N   y, n

Allowed substitution hints:   D( x, y, n)   T( x, y, n)   N( x, n)

Proof of Theorem dirkerper

Step	Hyp	Ref	Expression
1		dirkerper.2	. . . . . . . . . . . . 13 |- T = ( 2 x. pi )
2	1	eqcomi 2470	. . . . . . . . . . . 12 |- ( 2 x. pi ) = T
3	2	oveq2i 6307	. . . . . . . . . . 11 |- ( 1 x. ( 2 x. pi ) ) = ( 1 x. T )
4		2re 10626	. . . . . . . . . . . . . . 15 |- 2 e. RR
5		pire 23068	. . . . . . . . . . . . . . 15 |- pi e. RR
6	4, 5	remulcli 9627	. . . . . . . . . . . . . 14 |- ( 2 x. pi ) e. RR
7	1, 6	eqeltri 2541	. . . . . . . . . . . . 13 |- T e. RR
8	7	recni 9625	. . . . . . . . . . . 12 |- T e. CC
9	8	mulid2i 9616	. . . . . . . . . . 11 |- ( 1 x. T ) = T
10	3, 9	eqtri 2486	. . . . . . . . . 10 |- ( 1 x. ( 2 x. pi ) ) = T
11	10	oveq2i 6307	. . . . . . . . 9 |- ( x + ( 1 x. ( 2 x. pi ) ) ) = ( x + T )
12	11	eqcomi 2470	. . . . . . . 8 |- ( x + T ) = ( x + ( 1 x. ( 2 x. pi ) ) )
13	12	oveq1i 6306	. . . . . . 7 |- ( ( x + T ) mod ( 2 x. pi ) ) = ( ( x + ( 1 x. ( 2 x. pi ) ) ) mod ( 2 x. pi ) )
14	13	a1i 11	. . . . . 6 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( x + T ) mod ( 2 x. pi ) ) = ( ( x + ( 1 x. ( 2 x. pi ) ) ) mod ( 2 x. pi ) ) )
15		id 22	. . . . . . . 8 |- ( x e. RR -> x e. RR )
16	15	ad2antlr 726	. . . . . . 7 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> x e. RR )
17		2rp 11250	. . . . . . . . 9 |- 2 e. RR+
18		pirp 23071	. . . . . . . . 9 |- pi e. RR+
19		rpmulcl 11266	. . . . . . . . 9 |- ( ( 2 e. RR+ /\ pi e. RR+ ) -> ( 2 x. pi ) e. RR+ )
20	17, 18, 19	mp2an 672	. . . . . . . 8 |- ( 2 x. pi ) e. RR+
21	20	a1i 11	. . . . . . 7 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> ( 2 x. pi ) e. RR+ )
22		1z 10915	. . . . . . . 8 |- 1 e. ZZ
23	22	a1i 11	. . . . . . 7 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> 1 e. ZZ )
24		modcyc 12034	. . . . . . 7 |- ( ( x e. RR /\ ( 2 x. pi ) e. RR+ /\ 1 e. ZZ ) -> ( ( x + ( 1 x. ( 2 x. pi ) ) ) mod ( 2 x. pi ) ) = ( x mod ( 2 x. pi ) ) )
25	16, 21, 23, 24	syl3anc 1228	. . . . . 6 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( x + ( 1 x. ( 2 x. pi ) ) ) mod ( 2 x. pi ) ) = ( x mod ( 2 x. pi ) ) )
26		simpr 461	. . . . . 6 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> ( x mod ( 2 x. pi ) ) = 0 )
27	14, 25, 26	3eqtrd 2502	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( x + T ) mod ( 2 x. pi ) ) = 0 )
28	27	iftrued 3952	. . . 4 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) )
29		iftrue 3950	. . . . 5 |- ( ( x mod ( 2 x. pi ) ) = 0 -> if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) )
30	29	adantl 466	. . . 4 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) )
31	28, 30	eqtr4d 2501	. . 3 |- ( ( ( N e. NN /\ x e. RR ) /\ ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) )
32		iffalse 3953	. . . . 5 |- ( -. ( x mod ( 2 x. pi ) ) = 0 -> if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) )
33	32	adantl 466	. . . 4 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) )
34		nncn 10564	. . . . . . . . . 10 |- ( N e. NN -> N e. CC )
35		halfcn 10776	. . . . . . . . . . 11 |- ( 1 / 2 ) e. CC
36	35	a1i 11	. . . . . . . . . 10 |- ( N e. NN -> ( 1 / 2 ) e. CC )
37	34, 36	addcld 9632	. . . . . . . . 9 |- ( N e. NN -> ( N + ( 1 / 2 ) ) e. CC )
38	37	adantr 465	. . . . . . . 8 |- ( ( N e. NN /\ x e. RR ) -> ( N + ( 1 / 2 ) ) e. CC )
39		recn 9599	. . . . . . . . 9 |- ( x e. RR -> x e. CC )
40	39	adantl 466	. . . . . . . 8 |- ( ( N e. NN /\ x e. RR ) -> x e. CC )
41	38, 40	mulcld 9633	. . . . . . 7 |- ( ( N e. NN /\ x e. RR ) -> ( ( N + ( 1 / 2 ) ) x. x ) e. CC )
42	41	sincld 13968	. . . . . 6 |- ( ( N e. NN /\ x e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) e. CC )
43	42	adantr 465	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) e. CC )
44	6	recni 9625	. . . . . . . 8 |- ( 2 x. pi ) e. CC
45	44	a1i 11	. . . . . . 7 |- ( ( N e. NN /\ x e. RR ) -> ( 2 x. pi ) e. CC )
46	40	halfcld 10804	. . . . . . . 8 |- ( ( N e. NN /\ x e. RR ) -> ( x / 2 ) e. CC )
47	46	sincld 13968	. . . . . . 7 |- ( ( N e. NN /\ x e. RR ) -> ( sin ` ( x / 2 ) ) e. CC )
48	45, 47	mulcld 9633	. . . . . 6 |- ( ( N e. NN /\ x e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) e. CC )
49	48	adantr 465	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) e. CC )
50		dirkerdenne0 32121	. . . . . 6 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) =/= 0 )
51	50	adantll 713	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) =/= 0 )
52	43, 49, 51	div2negd 10356	. . . 4 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / -u ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) )
53	13	a1i 11	. . . . . . . . . . 11 |- ( x e. RR -> ( ( x + T ) mod ( 2 x. pi ) ) = ( ( x + ( 1 x. ( 2 x. pi ) ) ) mod ( 2 x. pi ) ) )
54	20, 22, 24	mp3an23 1316	. . . . . . . . . . 11 |- ( x e. RR -> ( ( x + ( 1 x. ( 2 x. pi ) ) ) mod ( 2 x. pi ) ) = ( x mod ( 2 x. pi ) ) )
55	53, 54	eqtrd 2498	. . . . . . . . . 10 |- ( x e. RR -> ( ( x + T ) mod ( 2 x. pi ) ) = ( x mod ( 2 x. pi ) ) )
56	55	adantr 465	. . . . . . . . 9 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( x + T ) mod ( 2 x. pi ) ) = ( x mod ( 2 x. pi ) ) )
57		simpr 461	. . . . . . . . . 10 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> -. ( x mod ( 2 x. pi ) ) = 0 )
58	57	neqned 2660	. . . . . . . . 9 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( x mod ( 2 x. pi ) ) =/= 0 )
59	56, 58	eqnetrd 2750	. . . . . . . 8 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( x + T ) mod ( 2 x. pi ) ) =/= 0 )
60	59	neneqd 2659	. . . . . . 7 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> -. ( ( x + T ) mod ( 2 x. pi ) ) = 0 )
61		iffalse 3953	. . . . . . . 8 |- ( -. ( ( x + T ) mod ( 2 x. pi ) ) = 0 -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) )
62	1	oveq2i 6307	. . . . . . . . . . 11 |- ( x + T ) = ( x + ( 2 x. pi ) )
63	62	oveq2i 6307	. . . . . . . . . 10 |- ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) = ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) )
64	63	fveq2i 5875	. . . . . . . . 9 |- ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) )
65	62	oveq1i 6306	. . . . . . . . . . 11 |- ( ( x + T ) / 2 ) = ( ( x + ( 2 x. pi ) ) / 2 )
66	65	fveq2i 5875	. . . . . . . . . 10 |- ( sin ` ( ( x + T ) / 2 ) ) = ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) )
67	66	oveq2i 6307	. . . . . . . . 9 |- ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) )
68	64, 67	oveq12i 6308	. . . . . . . 8 |- ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) )
69	61, 68	syl6eq 2514	. . . . . . 7 |- ( -. ( ( x + T ) mod ( 2 x. pi ) ) = 0 -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) ) )
70	60, 69	syl 16	. . . . . 6 |- ( ( x e. RR /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) ) )
71	70	adantll 713	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) ) )
72	44	a1i 11	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( 2 x. pi ) e. CC )
73	34, 36, 72	adddird 9638	. . . . . . . . . . . . 13 |- ( N e. NN -> ( ( N + ( 1 / 2 ) ) x. ( 2 x. pi ) ) = ( ( N x. ( 2 x. pi ) ) + ( ( 1 / 2 ) x. ( 2 x. pi ) ) ) )
74		ax-1cn 9567	. . . . . . . . . . . . . . . 16 |- 1 e. CC
75		2cnne0 10771	. . . . . . . . . . . . . . . 16 |- ( 2 e. CC /\ 2 =/= 0 )
76		2cn 10627	. . . . . . . . . . . . . . . . 17 |- 2 e. CC
77		picn 23069	. . . . . . . . . . . . . . . . 17 |- pi e. CC
78	76, 77	mulcli 9618	. . . . . . . . . . . . . . . 16 |- ( 2 x. pi ) e. CC
79		div32 10248	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 x. pi ) e. CC ) -> ( ( 1 / 2 ) x. ( 2 x. pi ) ) = ( 1 x. ( ( 2 x. pi ) / 2 ) ) )
80	74, 75, 78, 79	mp3an 1324	. . . . . . . . . . . . . . 15 |- ( ( 1 / 2 ) x. ( 2 x. pi ) ) = ( 1 x. ( ( 2 x. pi ) / 2 ) )
81		2ne0 10649	. . . . . . . . . . . . . . . . . 18 |- 2 =/= 0
82	78, 76, 81	divcli 10307	. . . . . . . . . . . . . . . . 17 |- ( ( 2 x. pi ) / 2 ) e. CC
83	82	mulid2i 9616	. . . . . . . . . . . . . . . 16 |- ( 1 x. ( ( 2 x. pi ) / 2 ) ) = ( ( 2 x. pi ) / 2 )
84	77, 76, 81	divcan3i 10311	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. pi ) / 2 ) = pi
85	83, 84	eqtri 2486	. . . . . . . . . . . . . . 15 |- ( 1 x. ( ( 2 x. pi ) / 2 ) ) = pi
86	80, 85	eqtri 2486	. . . . . . . . . . . . . 14 |- ( ( 1 / 2 ) x. ( 2 x. pi ) ) = pi
87	86	oveq2i 6307	. . . . . . . . . . . . 13 |- ( ( N x. ( 2 x. pi ) ) + ( ( 1 / 2 ) x. ( 2 x. pi ) ) ) = ( ( N x. ( 2 x. pi ) ) + pi )
88	73, 87	syl6eq 2514	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( N + ( 1 / 2 ) ) x. ( 2 x. pi ) ) = ( ( N x. ( 2 x. pi ) ) + pi ) )
89	88	oveq2d 6312	. . . . . . . . . . 11 |- ( N e. NN -> ( ( ( N + ( 1 / 2 ) ) x. x ) + ( ( N + ( 1 / 2 ) ) x. ( 2 x. pi ) ) ) = ( ( ( N + ( 1 / 2 ) ) x. x ) + ( ( N x. ( 2 x. pi ) ) + pi ) ) )
90	89	adantr 465	. . . . . . . . . 10 |- ( ( N e. NN /\ x e. RR ) -> ( ( ( N + ( 1 / 2 ) ) x. x ) + ( ( N + ( 1 / 2 ) ) x. ( 2 x. pi ) ) ) = ( ( ( N + ( 1 / 2 ) ) x. x ) + ( ( N x. ( 2 x. pi ) ) + pi ) ) )
91	38, 40, 45	adddid 9637	. . . . . . . . . 10 |- ( ( N e. NN /\ x e. RR ) -> ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) = ( ( ( N + ( 1 / 2 ) ) x. x ) + ( ( N + ( 1 / 2 ) ) x. ( 2 x. pi ) ) ) )
92	34, 72	mulcld 9633	. . . . . . . . . . . 12 |- ( N e. NN -> ( N x. ( 2 x. pi ) ) e. CC )
93	92	adantr 465	. . . . . . . . . . 11 |- ( ( N e. NN /\ x e. RR ) -> ( N x. ( 2 x. pi ) ) e. CC )
94	77	a1i 11	. . . . . . . . . . 11 |- ( ( N e. NN /\ x e. RR ) -> pi e. CC )
95	41, 93, 94	addassd 9635	. . . . . . . . . 10 |- ( ( N e. NN /\ x e. RR ) -> ( ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) + pi ) = ( ( ( N + ( 1 / 2 ) ) x. x ) + ( ( N x. ( 2 x. pi ) ) + pi ) ) )
96	90, 91, 95	3eqtr4d 2508	. . . . . . . . 9 |- ( ( N e. NN /\ x e. RR ) -> ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) = ( ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) + pi ) )
97	96	fveq2d 5876	. . . . . . . 8 |- ( ( N e. NN /\ x e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) = ( sin ` ( ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) + pi ) ) )
98	41, 93	addcld 9632	. . . . . . . . 9 |- ( ( N e. NN /\ x e. RR ) -> ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) e. CC )
99		sinppi 23099	. . . . . . . . 9 |- ( ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) e. CC -> ( sin ` ( ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) + pi ) ) = -u ( sin ` ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) ) )
100	98, 99	syl 16	. . . . . . . 8 |- ( ( N e. NN /\ x e. RR ) -> ( sin ` ( ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) + pi ) ) = -u ( sin ` ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) ) )
101		simpl 457	. . . . . . . . . . 11 |- ( ( N e. NN /\ x e. RR ) -> N e. NN )
102	101	nnzd 10989	. . . . . . . . . 10 |- ( ( N e. NN /\ x e. RR ) -> N e. ZZ )
103		sinper 23091	. . . . . . . . . 10 |- ( ( ( ( N + ( 1 / 2 ) ) x. x ) e. CC /\ N e. ZZ ) -> ( sin ` ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) )
104	41, 102, 103	syl2anc 661	. . . . . . . . 9 |- ( ( N e. NN /\ x e. RR ) -> ( sin ` ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) )
105	104	negeqd 9833	. . . . . . . 8 |- ( ( N e. NN /\ x e. RR ) -> -u ( sin ` ( ( ( N + ( 1 / 2 ) ) x. x ) + ( N x. ( 2 x. pi ) ) ) ) = -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) )
106	97, 100, 105	3eqtrd 2502	. . . . . . 7 |- ( ( N e. NN /\ x e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) = -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) )
107	44	a1i 11	. . . . . . . . . . . . 13 |- ( x e. RR -> ( 2 x. pi ) e. CC )
108	76	a1i 11	. . . . . . . . . . . . 13 |- ( x e. RR -> 2 e. CC )
109	81	a1i 11	. . . . . . . . . . . . 13 |- ( x e. RR -> 2 =/= 0 )
110	39, 107, 108, 109	divdird 10379	. . . . . . . . . . . 12 |- ( x e. RR -> ( ( x + ( 2 x. pi ) ) / 2 ) = ( ( x / 2 ) + ( ( 2 x. pi ) / 2 ) ) )
111	84	a1i 11	. . . . . . . . . . . . 13 |- ( x e. RR -> ( ( 2 x. pi ) / 2 ) = pi )
112	111	oveq2d 6312	. . . . . . . . . . . 12 |- ( x e. RR -> ( ( x / 2 ) + ( ( 2 x. pi ) / 2 ) ) = ( ( x / 2 ) + pi ) )
113	110, 112	eqtrd 2498	. . . . . . . . . . 11 |- ( x e. RR -> ( ( x + ( 2 x. pi ) ) / 2 ) = ( ( x / 2 ) + pi ) )
114	113	fveq2d 5876	. . . . . . . . . 10 |- ( x e. RR -> ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) = ( sin ` ( ( x / 2 ) + pi ) ) )
115	39	halfcld 10804	. . . . . . . . . . 11 |- ( x e. RR -> ( x / 2 ) e. CC )
116		sinppi 23099	. . . . . . . . . . 11 |- ( ( x / 2 ) e. CC -> ( sin ` ( ( x / 2 ) + pi ) ) = -u ( sin ` ( x / 2 ) ) )
117	115, 116	syl 16	. . . . . . . . . 10 |- ( x e. RR -> ( sin ` ( ( x / 2 ) + pi ) ) = -u ( sin ` ( x / 2 ) ) )
118	114, 117	eqtrd 2498	. . . . . . . . 9 |- ( x e. RR -> ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) = -u ( sin ` ( x / 2 ) ) )
119	118	oveq2d 6312	. . . . . . . 8 |- ( x e. RR -> ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) = ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) )
120	119	adantl 466	. . . . . . 7 |- ( ( N e. NN /\ x e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) = ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) )
121	106, 120	oveq12d 6314	. . . . . 6 |- ( ( N e. NN /\ x e. RR ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) ) = ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) ) )
122	121	adantr 465	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + ( 2 x. pi ) ) / 2 ) ) ) ) = ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) ) )
123	115	sincld 13968	. . . . . . . 8 |- ( x e. RR -> ( sin ` ( x / 2 ) ) e. CC )
124	107, 123	mulneg2d 10031	. . . . . . 7 |- ( x e. RR -> ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) = -u ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) )
125	124	oveq2d 6312	. . . . . 6 |- ( x e. RR -> ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) ) = ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / -u ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) )
126	125	ad2antlr 726	. . . . 5 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. -u ( sin ` ( x / 2 ) ) ) ) = ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / -u ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) )
127	71, 122, 126	3eqtrrd 2503	. . . 4 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> ( -u ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / -u ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) = if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) )
128	33, 52, 127	3eqtr2rd 2505	. . 3 |- ( ( ( N e. NN /\ x e. RR ) /\ -. ( x mod ( 2 x. pi ) ) = 0 ) -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) )
129	31, 128	pm2.61dan 791	. 2 |- ( ( N e. NN /\ x e. RR ) -> if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) = if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) )
130	7	a1i 11	. . . 4 |- ( x e. RR -> T e. RR )
131	15, 130	readdcld 9640	. . 3 |- ( x e. RR -> ( x + T ) e. RR )
132		dirkerper.1	. . . 4 |- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
133	132	dirkerval2 32122	. . 3 |- ( ( N e. NN /\ ( x + T ) e. RR ) -> ( ( D ` N ) ` ( x + T ) ) = if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) )
134	131, 133	sylan2 474	. 2 |- ( ( N e. NN /\ x e. RR ) -> ( ( D ` N ) ` ( x + T ) ) = if ( ( ( x + T ) mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( x + T ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( x + T ) / 2 ) ) ) ) ) )
135	132	dirkerval2 32122	. 2 |- ( ( N e. NN /\ x e. RR ) -> ( ( D ` N ) ` x ) = if ( ( x mod ( 2 x. pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. x ) ) / ( ( 2 x. pi ) x. ( sin ` ( x / 2 ) ) ) ) ) )
136	129, 134, 135	3eqtr4d 2508	1 |- ( ( N e. NN /\ x e. RR ) -> ( ( D ` N ) ` ( x + T ) ) = ( ( D ` N ) ` x ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   = wceq 1395   e. wcel 1819   =/= wne 2652   ifcif 3944   |-> cmpt 4515   ` cfv 5594  (class class class)co 6296   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510   + caddc 9512   x. cmul 9514   -ucneg 9825   / cdiv 10227   NNcn 10556   2c2 10606   ZZcz 10885   RR+crp 11245   mod cmo 11999   sincsin 13902   picpi 13905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587  ax-addf 9588  ax-mulf 9589

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-ixp 7489  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-fi 7889  df-sup 7919  df-oi 7953  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-q 11208  df-rp 11246  df-xneg 11343  df-xadd 11344  df-xmul 11345  df-ioo 11558  df-ioc 11559  df-ico 11560  df-icc 11561  df-fz 11698  df-fzo 11822  df-fl 11932  df-mod 12000  df-seq 12111  df-exp 12170  df-fac 12357  df-bc 12384  df-hash 12409  df-shft 13003  df-cj 13035  df-re 13036  df-im 13037  df-sqrt 13171  df-abs 13172  df-limsup 13397  df-clim 13414  df-rlim 13415  df-sum 13612  df-ef 13906  df-sin 13908  df-cos 13909  df-pi 13911  df-struct 14737  df-ndx 14738  df-slot 14739  df-base 14740  df-sets 14741  df-ress 14742  df-plusg 14816  df-mulr 14817  df-starv 14818  df-sca 14819  df-vsca 14820  df-ip 14821  df-tset 14822  df-ple 14823  df-ds 14825  df-unif 14826  df-hom 14827  df-cco 14828  df-rest 14931  df-topn 14932  df-0g 14950  df-gsum 14951  df-topgen 14952  df-pt 14953  df-prds 14956  df-xrs 15010  df-qtop 15015  df-imas 15016  df-xps 15018  df-mre 15094  df-mrc 15095  df-acs 15097  df-mgm 16090  df-sgrp 16129  df-mnd 16139  df-submnd 16185  df-mulg 16278  df-cntz 16573  df-cmn 17018  df-psmet 18629  df-xmet 18630  df-met 18631  df-bl 18632  df-mopn 18633  df-fbas 18634  df-fg 18635  df-cnfld 18639  df-top 19617  df-bases 19619  df-topon 19620  df-topsp 19621  df-cld 19738  df-ntr 19739  df-cls 19740  df-nei 19817  df-lp 19855  df-perf 19856  df-cn 19946  df-cnp 19947  df-haus 20034  df-tx 20280  df-hmeo 20473  df-fil 20564  df-fm 20656  df-flim 20657  df-flf 20658  df-xms 21040  df-ms 21041  df-tms 21042  df-cncf 21599  df-limc 22487  df-dv 22488

This theorem is referenced by:  fourierdlem111  32246