This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 + 𝑇 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑥 ) )