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