Theorem dirkerper

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

	Ref	Expression
Hypotheses	dirkerper.1	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
	dirkerper.2	⊢ 𝑇 = ( 2 · π )
Assertion	dirkerper	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 + 𝑇 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		dirkerper.1	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
2		dirkerper.2	⊢ 𝑇 = ( 2 · π )
3	2	eqcomi	⊢ ( 2 · π ) = 𝑇
4	3	oveq2i	⊢ ( 1 · ( 2 · π ) ) = ( 1 · 𝑇 )
5		2re	⊢ 2 ∈ ℝ
6		pire	⊢ π ∈ ℝ
7	5 6	remulcli	⊢ ( 2 · π ) ∈ ℝ
8	2 7	eqeltri	⊢ 𝑇 ∈ ℝ
9	8	recni	⊢ 𝑇 ∈ ℂ
10	9	mullidi	⊢ ( 1 · 𝑇 ) = 𝑇
11	4 10	eqtri	⊢ ( 1 · ( 2 · π ) ) = 𝑇
12	11	oveq2i	⊢ ( 𝑥 + ( 1 · ( 2 · π ) ) ) = ( 𝑥 + 𝑇 )
13	12	eqcomi	⊢ ( 𝑥 + 𝑇 ) = ( 𝑥 + ( 1 · ( 2 · π ) ) )
14	13	oveq1i	⊢ ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = ( ( 𝑥 + ( 1 · ( 2 · π ) ) ) mod ( 2 · π ) )
15	14	a1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = ( ( 𝑥 + ( 1 · ( 2 · π ) ) ) mod ( 2 · π ) ) )
16		id	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
17	16	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → 𝑥 ∈ ℝ )
18		2rp	⊢ 2 ∈ ℝ+
19		pirp	⊢ π ∈ ℝ+
20		rpmulcl	⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
21	18 19 20	mp2an	⊢ ( 2 · π ) ∈ ℝ+
22	21	a1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( 2 · π ) ∈ ℝ+ )
23		1z	⊢ 1 ∈ ℤ
24	23	a1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → 1 ∈ ℤ )
25		modcyc	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( 𝑥 + ( 1 · ( 2 · π ) ) ) mod ( 2 · π ) ) = ( 𝑥 mod ( 2 · π ) ) )
26	17 22 24 25	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 𝑥 + ( 1 · ( 2 · π ) ) ) mod ( 2 · π ) ) = ( 𝑥 mod ( 2 · π ) ) )
27		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( 𝑥 mod ( 2 · π ) ) = 0 )
28	15 26 27	3eqtrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 )
29	28	iftrued	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
30		iftrue	⊢ ( ( 𝑥 mod ( 2 · π ) ) = 0 → if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
31	30	adantl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
32	29 31	eqtr4d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) )
33		iffalse	⊢ ( ¬ ( 𝑥 mod ( 2 · π ) ) = 0 → if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
34	33	adantl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
35		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
36		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
37	36	a1i	⊢ ( 𝑁 ∈ ℕ → ( 1 / 2 ) ∈ ℂ )
38	35 37	addcld	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
39	38	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
40		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
41	40	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
42	39 41	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℂ )
43	42	sincld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ∈ ℂ )
44	43	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ∈ ℂ )
45	7	recni	⊢ ( 2 · π ) ∈ ℂ
46	45	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 2 · π ) ∈ ℂ )
47	41	halfcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 / 2 ) ∈ ℂ )
48	47	sincld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( 𝑥 / 2 ) ) ∈ ℂ )
49	46 48	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ℂ )
50	49	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ∈ ℂ )
51		dirkerdenne0	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ≠ 0 )
52	51	adantll	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ≠ 0 )
53	44 50 52	div2negd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / - ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
54	14	a1i	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = ( ( 𝑥 + ( 1 · ( 2 · π ) ) ) mod ( 2 · π ) ) )
55	21 23 25	mp3an23	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 + ( 1 · ( 2 · π ) ) ) mod ( 2 · π ) ) = ( 𝑥 mod ( 2 · π ) ) )
56	54 55	eqtrd	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = ( 𝑥 mod ( 2 · π ) ) )
57	56	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = ( 𝑥 mod ( 2 · π ) ) )
58		simpr	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ¬ ( 𝑥 mod ( 2 · π ) ) = 0 )
59	58	neqned	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( 𝑥 mod ( 2 · π ) ) ≠ 0 )
60	57 59	eqnetrd	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) ≠ 0 )
61	60	neneqd	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ¬ ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 )
62		iffalse	⊢ ( ¬ ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) )
63	2	oveq2i	⊢ ( 𝑥 + 𝑇 ) = ( 𝑥 + ( 2 · π ) )
64	63	oveq2i	⊢ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) )
65	64	fveq2i	⊢ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) )
66	63	oveq1i	⊢ ( ( 𝑥 + 𝑇 ) / 2 ) = ( ( 𝑥 + ( 2 · π ) ) / 2 )
67	66	fveq2i	⊢ ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) = ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) )
68	67	oveq2i	⊢ ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) )
69	65 68	oveq12i	⊢ ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) )
70	62 69	eqtrdi	⊢ ( ¬ ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) ) )
71	61 70	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) ) )
72	71	adantll	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) ) )
73	45	a1i	⊢ ( 𝑁 ∈ ℕ → ( 2 · π ) ∈ ℂ )
74	35 37 73	adddird	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) = ( ( 𝑁 · ( 2 · π ) ) + ( ( 1 / 2 ) · ( 2 · π ) ) ) )
75		ax-1cn	⊢ 1 ∈ ℂ
76		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
77		2cn	⊢ 2 ∈ ℂ
78		picn	⊢ π ∈ ℂ
79	77 78	mulcli	⊢ ( 2 · π ) ∈ ℂ
80		div32	⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 · π ) ∈ ℂ ) → ( ( 1 / 2 ) · ( 2 · π ) ) = ( 1 · ( ( 2 · π ) / 2 ) ) )
81	75 76 79 80	mp3an	⊢ ( ( 1 / 2 ) · ( 2 · π ) ) = ( 1 · ( ( 2 · π ) / 2 ) )
82		2ne0	⊢ 2 ≠ 0
83	79 77 82	divcli	⊢ ( ( 2 · π ) / 2 ) ∈ ℂ
84	83	mullidi	⊢ ( 1 · ( ( 2 · π ) / 2 ) ) = ( ( 2 · π ) / 2 )
85	78 77 82	divcan3i	⊢ ( ( 2 · π ) / 2 ) = π
86	84 85	eqtri	⊢ ( 1 · ( ( 2 · π ) / 2 ) ) = π
87	81 86	eqtri	⊢ ( ( 1 / 2 ) · ( 2 · π ) ) = π
88	87	oveq2i	⊢ ( ( 𝑁 · ( 2 · π ) ) + ( ( 1 / 2 ) · ( 2 · π ) ) ) = ( ( 𝑁 · ( 2 · π ) ) + π )
89	74 88	eqtrdi	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) = ( ( 𝑁 · ( 2 · π ) ) + π ) )
90	89	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( ( 𝑁 · ( 2 · π ) ) + π ) ) )
91	90	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( ( 𝑁 · ( 2 · π ) ) + π ) ) )
92	39 41 46	adddid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( ( 𝑁 + ( 1 / 2 ) ) · ( 2 · π ) ) ) )
93	35 73	mulcld	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 · ( 2 · π ) ) ∈ ℂ )
94	93	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑁 · ( 2 · π ) ) ∈ ℂ )
95	78	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → π ∈ ℂ )
96	42 94 95	addassd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) + π ) = ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( ( 𝑁 · ( 2 · π ) ) + π ) ) )
97	91 92 96	3eqtr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) = ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) + π ) )
98	97	fveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) = ( sin ‘ ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) + π ) ) )
99	42 94	addcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ∈ ℂ )
100		sinppi	⊢ ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ∈ ℂ → ( sin ‘ ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) + π ) ) = - ( sin ‘ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ) )
101	99 100	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) + π ) ) = - ( sin ‘ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ) )
102		simpl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → 𝑁 ∈ ℕ )
103	102	nnzd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → 𝑁 ∈ ℤ )
104		sinper	⊢ ( ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( sin ‘ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
105	42 103 104	syl2anc	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
106	105	negeqd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → - ( sin ‘ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) + ( 𝑁 · ( 2 · π ) ) ) ) = - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
107	98 101 106	3eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) = - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
108	45	a1i	⊢ ( 𝑥 ∈ ℝ → ( 2 · π ) ∈ ℂ )
109	77	a1i	⊢ ( 𝑥 ∈ ℝ → 2 ∈ ℂ )
110	82	a1i	⊢ ( 𝑥 ∈ ℝ → 2 ≠ 0 )
111	40 108 109 110	divdird	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 + ( 2 · π ) ) / 2 ) = ( ( 𝑥 / 2 ) + ( ( 2 · π ) / 2 ) ) )
112	85	a1i	⊢ ( 𝑥 ∈ ℝ → ( ( 2 · π ) / 2 ) = π )
113	112	oveq2d	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 / 2 ) + ( ( 2 · π ) / 2 ) ) = ( ( 𝑥 / 2 ) + π ) )
114	111 113	eqtrd	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 + ( 2 · π ) ) / 2 ) = ( ( 𝑥 / 2 ) + π ) )
115	114	fveq2d	⊢ ( 𝑥 ∈ ℝ → ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) = ( sin ‘ ( ( 𝑥 / 2 ) + π ) ) )
116	40	halfcld	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 / 2 ) ∈ ℂ )
117		sinppi	⊢ ( ( 𝑥 / 2 ) ∈ ℂ → ( sin ‘ ( ( 𝑥 / 2 ) + π ) ) = - ( sin ‘ ( 𝑥 / 2 ) ) )
118	116 117	syl	⊢ ( 𝑥 ∈ ℝ → ( sin ‘ ( ( 𝑥 / 2 ) + π ) ) = - ( sin ‘ ( 𝑥 / 2 ) ) )
119	115 118	eqtrd	⊢ ( 𝑥 ∈ ℝ → ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) = - ( sin ‘ ( 𝑥 / 2 ) ) )
120	119	oveq2d	⊢ ( 𝑥 ∈ ℝ → ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) = ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) )
121	120	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) = ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) )
122	107 121	oveq12d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) ) = ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
123	122	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + ( 2 · π ) ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + ( 2 · π ) ) / 2 ) ) ) ) = ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
124	116	sincld	⊢ ( 𝑥 ∈ ℝ → ( sin ‘ ( 𝑥 / 2 ) ) ∈ ℂ )
125	108 124	mulneg2d	⊢ ( 𝑥 ∈ ℝ → ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) = - ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) )
126	125	oveq2d	⊢ ( 𝑥 ∈ ℝ → ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / - ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
127	126	ad2antlr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · - ( sin ‘ ( 𝑥 / 2 ) ) ) ) = ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / - ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) )
128	72 123 127	3eqtrrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → ( - ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / - ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) = if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) )
129	34 53 128	3eqtr2rd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝑥 mod ( 2 · π ) ) = 0 ) → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) )
130	32 129	pm2.61dan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) = if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) )
131	8	a1i	⊢ ( 𝑥 ∈ ℝ → 𝑇 ∈ ℝ )
132	16 131	readdcld	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 𝑇 ) ∈ ℝ )
133	1	dirkerval2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 + 𝑇 ) ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 + 𝑇 ) ) = if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) )
134	132 133	sylan2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 + 𝑇 ) ) = if ( ( ( 𝑥 + 𝑇 ) mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( 𝑥 + 𝑇 ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( 𝑥 + 𝑇 ) / 2 ) ) ) ) ) )
135	1	dirkerval2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑥 ) = if ( ( 𝑥 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑥 / 2 ) ) ) ) ) )
136	130 134 135	3eqtr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 + 𝑇 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑥 ) )