Metamath Proof Explorer

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