Theorem dirkertrigeqlem3 46936

Description: Trigonometric equality lemma for the Dirichlet kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
dirkertrigeqlem3.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
dirkertrigeqlem3.k	⊢ (𝜑 → 𝐾 ∈ ℤ)
dirkertrigeqlem3.a	⊢ 𝐴 = (((2 · 𝐾) + 1) · π)

Assertion

Ref	Expression
dirkertrigeqlem3	⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))

Distinct variable groups:   𝑛,𝑁   𝜑,𝑛

Allowed substitution hints:   𝐴(𝑛)   𝐾(𝑛)

Proof of Theorem dirkertrigeqlem3

Step	Hyp	Ref	Expression
1		dirkertrigeqlem3.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (((2 · 𝐾) + 1) · π)
2	1	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴 = (((2 · 𝐾) + 1) · π))
3	2	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) = (𝑛 · (((2 · 𝐾) + 1) · π)))
4		elfzelz 13582	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
5	4	zcnd 12730	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
6	5	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
7		2cnd 12347	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 2 ∈ ℂ)
8		dirkertrigeqlem3.k	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℤ)
9	8	zcnd 12730	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℂ)
10	9	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐾 ∈ ℂ)
11	7, 10	mulcld 11257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (2 · 𝐾) ∈ ℂ)
12		1cnd 11230	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ)
13	11, 12	addcld 11256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) + 1) ∈ ℂ)
14		picn 26701	. . . . . . . . . . . . . 14 ⊢ π ∈ ℂ
15	14	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
16	13, 15	mulcld 11257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) + 1) · π) ∈ ℂ)
17	6, 16	mulcomd 11258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · (((2 · 𝐾) + 1) · π)) = ((((2 · 𝐾) + 1) · π) · 𝑛))
18	13, 15, 6	mulassd 11260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((((2 · 𝐾) + 1) · π) · 𝑛) = (((2 · 𝐾) + 1) · (π · 𝑛)))
19	15, 6	mulcld 11257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (π · 𝑛) ∈ ℂ)
20	11, 12, 19	adddird 11262	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) + 1) · (π · 𝑛)) = (((2 · 𝐾) · (π · 𝑛)) + (1 · (π · 𝑛))))
21	11, 19	mulcld 11257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) · (π · 𝑛)) ∈ ℂ)
22	12, 19	mulcld 11257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (1 · (π · 𝑛)) ∈ ℂ)
23	21, 22	addcomd 11440	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) · (π · 𝑛)) + (1 · (π · 𝑛))) = ((1 · (π · 𝑛)) + ((2 · 𝐾) · (π · 𝑛))))
24	14	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → π ∈ ℂ)
25	24, 5	mulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → (π · 𝑛) ∈ ℂ)
26	25	mullidd 11255	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → (1 · (π · 𝑛)) = (π · 𝑛))
27	26	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (1 · (π · 𝑛)) = (π · 𝑛))
28	7, 10, 15, 6	mul4d 11450	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) · (π · 𝑛)) = ((2 · π) · (𝐾 · 𝑛)))
29	7, 15	mulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (2 · π) ∈ ℂ)
30	10, 6	mulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐾 · 𝑛) ∈ ℂ)
31	29, 30	mulcomd 11258	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · π) · (𝐾 · 𝑛)) = ((𝐾 · 𝑛) · (2 · π)))
32	28, 31	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) · (π · 𝑛)) = ((𝐾 · 𝑛) · (2 · π)))
33	27, 32	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1 · (π · 𝑛)) + ((2 · 𝐾) · (π · 𝑛))) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π))))
34	23, 33	eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) · (π · 𝑛)) + (1 · (π · 𝑛))) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π))))
35	18, 20, 34	3eqtrd 2801	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((((2 · 𝐾) + 1) · π) · 𝑛) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π))))
36	3, 17, 35	3eqtrd 2801	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π))))
37	36	fveq2d 6886	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) = (cos‘((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π)))))
38	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐾 ∈ ℤ)
39	4	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℤ)
40	38, 39	zmulcld 12735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐾 · 𝑛) ∈ ℤ)
41		cosper 26727	. . . . . . . . . 10 ⊢ (((π · 𝑛) ∈ ℂ ∧ (𝐾 · 𝑛) ∈ ℤ) → (cos‘((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π)))) = (cos‘(π · 𝑛)))
42	19, 40, 41	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π)))) = (cos‘(π · 𝑛)))
43	37, 42	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) = (cos‘(π · 𝑛)))
44	43	sumeq2dv 15793	. . . . . . 7 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) = Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)))
45	44	oveq2d 7433	. . . . . 6 ⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))))
46	45	oveq1d 7432	. . . . 5 ⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π))
47	46	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π))
48		dirkertrigeqlem3.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
49	48	nncnd 12277	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
50		2cnd 12347	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℂ)
51		2ne0 12375	. . . . . . . . . . . . . 14 ⊢ 2 ≠ 0
52	51	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ≠ 0)
53	49, 50, 52	divcan2d 12021	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · (𝑁 / 2)) = 𝑁)
54	53	eqcomd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = (2 · (𝑁 / 2)))
55	54	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) = (1...(2 · (𝑁 / 2))))
56	55	sumeq1d 15791	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛)))
57	56	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛)))
58	14	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → π ∈ ℂ)
59		elfzelz 13582	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → 𝑛 ∈ ℤ)
60	59	zcnd 12730	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → 𝑛 ∈ ℂ)
61	58, 60	mulcomd 11258	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → (π · 𝑛) = (𝑛 · π))
62	61	fveq2d 6886	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → (cos‘(π · 𝑛)) = (cos‘(𝑛 · π)))
63	62	rgen 3080	. . . . . . . . . 10 ⊢ ∀𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛)) = (cos‘(𝑛 · π))
64	63	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ∀𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛)) = (cos‘(𝑛 · π)))
65	64	sumeq2d 15792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(𝑛 · π)))
66		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝑁 mod 2) = 0)
67	48	nnred 12276	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
68	67	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 𝑁 ∈ ℝ)
69		2rp 13051	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ+
70		mod0 13941	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 2 ∈ ℝ+) → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈ ℤ))
71	68, 69, 70	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈ ℤ))
72	66, 71	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝑁 / 2) ∈ ℤ)
73		2re 12343	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
74	73	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℝ)
75	48	nngt0d 12313	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑁)
76		2pos 12373	. . . . . . . . . . . . 13 ⊢ 0 < 2
77	76	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 2)
78	67, 74, 75, 77	divgt0d 12178	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < (𝑁 / 2))
79	78	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 0 < (𝑁 / 2))
80		elnnz 12629	. . . . . . . . . 10 ⊢ ((𝑁 / 2) ∈ ℕ ↔ ((𝑁 / 2) ∈ ℤ ∧ 0 < (𝑁 / 2)))
81	72, 79, 80	sylanbrc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝑁 / 2) ∈ ℕ)
82		dirkertrigeqlem1 46934	. . . . . . . . 9 ⊢ ((𝑁 / 2) ∈ ℕ → Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(𝑛 · π)) = 0)
83	81, 82	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(𝑛 · π)) = 0)
84	57, 65, 83	3eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = 0)
85	84	oveq2d 7433	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) = ((1 / 2) + 0))
86		halfcn 12486	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
87	86	addridi 11425	. . . . . 6 ⊢ ((1 / 2) + 0) = (1 / 2)
88	85, 87	eqtrdi 2813	. . . . 5 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) = (1 / 2))
89	88	oveq1d 7432	. . . 4 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π) = ((1 / 2) / π))
90		ax-1cn 11186	. . . . . 6 ⊢ 1 ∈ ℂ
91		2cnne0 12481	. . . . . 6 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
92		pire 26699	. . . . . . . 8 ⊢ π ∈ ℝ
93		pipos 26703	. . . . . . . 8 ⊢ 0 < π
94	92, 93	gt0ne0ii 11778	. . . . . . 7 ⊢ π ≠ 0
95	14, 94	pm3.2i 476	. . . . . 6 ⊢ (π ∈ ℂ ∧ π ≠ 0)
96		divdiv1 11954	. . . . . 6 ⊢ ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → ((1 / 2) / π) = (1 / (2 · π)))
97	90, 91, 95, 96	mp3an 1490	. . . . 5 ⊢ ((1 / 2) / π) = (1 / (2 · π))
98	97	a1i 11	. . . 4 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((1 / 2) / π) = (1 / (2 · π)))
99	47, 89, 98	3eqtrd 2801	. . 3 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (1 / (2 · π)))
100	1	oveq2i 7428	. . . . . . . . . 10 ⊢ ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 + (1 / 2)) · (((2 · 𝐾) + 1) · π))
101	100	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 + (1 / 2)) · (((2 · 𝐾) + 1) · π)))
102	86	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
103	49, 102	addcld 11256	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ)
104	50, 9	mulcld 11257	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝐾) ∈ ℂ)
105		peano2cn 11410	. . . . . . . . . . 11 ⊢ ((2 · 𝐾) ∈ ℂ → ((2 · 𝐾) + 1) ∈ ℂ)
106	104, 105	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝐾) + 1) ∈ ℂ)
107	14	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → π ∈ ℂ)
108	103, 106, 107	mulassd 11260	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) · π) = ((𝑁 + (1 / 2)) · (((2 · 𝐾) + 1) · π)))
109		1cnd 11230	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℂ)
110	49, 102, 104, 109	muladdd 11700	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) = (((𝑁 · (2 · 𝐾)) + (1 · (1 / 2))) + ((𝑁 · 1) + ((2 · 𝐾) · (1 / 2)))))
111	49, 50, 9	mul12d 11447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · (2 · 𝐾)) = (2 · (𝑁 · 𝐾)))
112	102	mullidd 11255	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · (1 / 2)) = (1 / 2))
113	111, 112	oveq12d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 · (2 · 𝐾)) + (1 · (1 / 2))) = ((2 · (𝑁 · 𝐾)) + (1 / 2)))
114	49	mulridd 11254	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · 1) = 𝑁)
115	50, 9	mulcomd 11258	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝐾) = (𝐾 · 2))
116	115	oveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · 𝐾) · (1 / 2)) = ((𝐾 · 2) · (1 / 2)))
117	9, 50, 102	mulassd 11260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐾 · 2) · (1 / 2)) = (𝐾 · (2 · (1 / 2))))
118		2thalfe1 12376	. . . . . . . . . . . . . . . . . 18 ⊢ (2 · (1 / 2)) = 1
119	118	oveq2i 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 · (2 · (1 / 2))) = (𝐾 · 1)
120	9	mulridd 11254	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 · 1) = 𝐾)
121	119, 120	eqtrid 2809	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 · (2 · (1 / 2))) = 𝐾)
122	116, 117, 121	3eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · 𝐾) · (1 / 2)) = 𝐾)
123	114, 122	oveq12d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 · 1) + ((2 · 𝐾) · (1 / 2))) = (𝑁 + 𝐾))
124	113, 123	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑁 · (2 · 𝐾)) + (1 · (1 / 2))) + ((𝑁 · 1) + ((2 · 𝐾) · (1 / 2)))) = (((2 · (𝑁 · 𝐾)) + (1 / 2)) + (𝑁 + 𝐾)))
125	49, 9	mulcld 11257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 · 𝐾) ∈ ℂ)
126	50, 125	mulcld 11257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · (𝑁 · 𝐾)) ∈ ℂ)
127	49, 9	addcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 + 𝐾) ∈ ℂ)
128	126, 102, 127	addassd 11259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝑁 · 𝐾)) + (1 / 2)) + (𝑁 + 𝐾)) = ((2 · (𝑁 · 𝐾)) + ((1 / 2) + (𝑁 + 𝐾))))
129	110, 124, 128	3eqtrd 2801	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) = ((2 · (𝑁 · 𝐾)) + ((1 / 2) + (𝑁 + 𝐾))))
130	102, 127	addcld 11256	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1 / 2) + (𝑁 + 𝐾)) ∈ ℂ)
131	126, 130	addcomd 11440	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (𝑁 · 𝐾)) + ((1 / 2) + (𝑁 + 𝐾))) = (((1 / 2) + (𝑁 + 𝐾)) + (2 · (𝑁 · 𝐾))))
132	50, 125	mulcomd 11258	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑁 · 𝐾)) = ((𝑁 · 𝐾) · 2))
133	132	oveq2d 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → (((1 / 2) + (𝑁 + 𝐾)) + (2 · (𝑁 · 𝐾))) = (((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2)))
134	129, 131, 133	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) = (((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2)))
135	134	oveq1d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) · π) = ((((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2)) · π))
136	125, 50	mulcld 11257	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 · 𝐾) · 2) ∈ ℂ)
137	130, 136, 107	adddird 11262	. . . . . . . . . 10 ⊢ (𝜑 → ((((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2)) · π) = ((((1 / 2) + (𝑁 + 𝐾)) · π) + (((𝑁 · 𝐾) · 2) · π)))
138	125, 50, 107	mulassd 11260	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 · 𝐾) · 2) · π) = ((𝑁 · 𝐾) · (2 · π)))
139	138	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → ((((1 / 2) + (𝑁 + 𝐾)) · π) + (((𝑁 · 𝐾) · 2) · π)) = ((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π))))
140	135, 137, 139	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) · π) = ((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π))))
141	101, 108, 140	3eqtr2d 2803	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π))))
142	141	fveq2d 6886	. . . . . . 7 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) = (sin‘((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π)))))
143	130, 107	mulcld 11257	. . . . . . . 8 ⊢ (𝜑 → (((1 / 2) + (𝑁 + 𝐾)) · π) ∈ ℂ)
144	48	nnzd 12645	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
145	144, 8	zmulcld 12735	. . . . . . . 8 ⊢ (𝜑 → (𝑁 · 𝐾) ∈ ℤ)
146		sinper 26726	. . . . . . . 8 ⊢ (((((1 / 2) + (𝑁 + 𝐾)) · π) ∈ ℂ ∧ (𝑁 · 𝐾) ∈ ℤ) → (sin‘((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π)))) = (sin‘(((1 / 2) + (𝑁 + 𝐾)) · π)))
147	143, 145, 146	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (sin‘((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π)))) = (sin‘(((1 / 2) + (𝑁 + 𝐾)) · π)))
148	102, 127	addcomd 11440	. . . . . . . . . 10 ⊢ (𝜑 → ((1 / 2) + (𝑁 + 𝐾)) = ((𝑁 + 𝐾) + (1 / 2)))
149	49, 9, 102	addassd 11259	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + 𝐾) + (1 / 2)) = (𝑁 + (𝐾 + (1 / 2))))
150	9, 102	addcld 11256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾 + (1 / 2)) ∈ ℂ)
151	49, 150	addcomd 11440	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + (𝐾 + (1 / 2))) = ((𝐾 + (1 / 2)) + 𝑁))
152	148, 149, 151	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝜑 → ((1 / 2) + (𝑁 + 𝐾)) = ((𝐾 + (1 / 2)) + 𝑁))
153	152	oveq1d 7432	. . . . . . . 8 ⊢ (𝜑 → (((1 / 2) + (𝑁 + 𝐾)) · π) = (((𝐾 + (1 / 2)) + 𝑁) · π))
154	153	fveq2d 6886	. . . . . . 7 ⊢ (𝜑 → (sin‘(((1 / 2) + (𝑁 + 𝐾)) · π)) = (sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)))
155	142, 147, 154	3eqtrd 2801	. . . . . 6 ⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) = (sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)))
156	1	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = (((2 · 𝐾) + 1) · π))
157	156	oveq1d 7432	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 / 2) = ((((2 · 𝐾) + 1) · π) / 2))
158	106, 107, 50, 52	div23d 12056	. . . . . . . . 9 ⊢ (𝜑 → ((((2 · 𝐾) + 1) · π) / 2) = ((((2 · 𝐾) + 1) / 2) · π))
159	104, 109, 50, 52	divdird 12057	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝐾) + 1) / 2) = (((2 · 𝐾) / 2) + (1 / 2)))
160	9, 50, 52	divcan3d 12024	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝐾) / 2) = 𝐾)
161	160	oveq1d 7432	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 𝐾) / 2) + (1 / 2)) = (𝐾 + (1 / 2)))
162	159, 161	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · 𝐾) + 1) / 2) = (𝐾 + (1 / 2)))
163	162	oveq1d 7432	. . . . . . . . 9 ⊢ (𝜑 → ((((2 · 𝐾) + 1) / 2) · π) = ((𝐾 + (1 / 2)) · π))
164	157, 158, 163	3eqtrd 2801	. . . . . . . 8 ⊢ (𝜑 → (𝐴 / 2) = ((𝐾 + (1 / 2)) · π))
165	164	fveq2d 6886	. . . . . . 7 ⊢ (𝜑 → (sin‘(𝐴 / 2)) = (sin‘((𝐾 + (1 / 2)) · π)))
166	165	oveq2d 7433	. . . . . 6 ⊢ (𝜑 → ((2 · π) · (sin‘(𝐴 / 2))) = ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π))))
167	155, 166	oveq12d 7435	. . . . 5 ⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))) = ((sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
168	167	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))) = ((sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
169	150, 49, 107	adddird 11262	. . . . . . 7 ⊢ (𝜑 → (((𝐾 + (1 / 2)) + 𝑁) · π) = (((𝐾 + (1 / 2)) · π) + (𝑁 · π)))
170	169	fveq2d 6886	. . . . . 6 ⊢ (𝜑 → (sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) = (sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))))
171	170	oveq1d 7432	. . . . 5 ⊢ (𝜑 → ((sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
172	171	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
173	49	halfcld 12517	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
174	50, 173	mulcomd 11258	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (𝑁 / 2)) = ((𝑁 / 2) · 2))
175	53, 174	eqtr3d 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 = ((𝑁 / 2) · 2))
176	175	oveq1d 7432	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 · π) = (((𝑁 / 2) · 2) · π))
177	173, 50, 107	mulassd 11260	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑁 / 2) · 2) · π) = ((𝑁 / 2) · (2 · π)))
178	176, 177	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · π) = ((𝑁 / 2) · (2 · π)))
179	178	oveq2d 7433	. . . . . . . . 9 ⊢ (𝜑 → (((𝐾 + (1 / 2)) · π) + (𝑁 · π)) = (((𝐾 + (1 / 2)) · π) + ((𝑁 / 2) · (2 · π))))
180	179	fveq2d 6886	. . . . . . . 8 ⊢ (𝜑 → (sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) = (sin‘(((𝐾 + (1 / 2)) · π) + ((𝑁 / 2) · (2 · π)))))
181	180	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) = (sin‘(((𝐾 + (1 / 2)) · π) + ((𝑁 / 2) · (2 · π)))))
182	9	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 𝐾 ∈ ℂ)
183		1cnd 11230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 1 ∈ ℂ)
184	183	halfcld 12517	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (1 / 2) ∈ ℂ)
185	182, 184	addcld 11256	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝐾 + (1 / 2)) ∈ ℂ)
186	14	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → π ∈ ℂ)
187	185, 186	mulcld 11257	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((𝐾 + (1 / 2)) · π) ∈ ℂ)
188		sinper 26726	. . . . . . . 8 ⊢ ((((𝐾 + (1 / 2)) · π) ∈ ℂ ∧ (𝑁 / 2) ∈ ℤ) → (sin‘(((𝐾 + (1 / 2)) · π) + ((𝑁 / 2) · (2 · π)))) = (sin‘((𝐾 + (1 / 2)) · π)))
189	187, 72, 188	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) + ((𝑁 / 2) · (2 · π)))) = (sin‘((𝐾 + (1 / 2)) · π)))
190	181, 189	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) = (sin‘((𝐾 + (1 / 2)) · π)))
191	50, 107	mulcld 11257	. . . . . . . 8 ⊢ (𝜑 → (2 · π) ∈ ℂ)
192	150, 107	mulcld 11257	. . . . . . . . 9 ⊢ (𝜑 → ((𝐾 + (1 / 2)) · π) ∈ ℂ)
193	192	sincld 16224	. . . . . . . 8 ⊢ (𝜑 → (sin‘((𝐾 + (1 / 2)) · π)) ∈ ℂ)
194	191, 193	mulcomd 11258	. . . . . . 7 ⊢ (𝜑 → ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π))) = ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π)))
195	194	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π))) = ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π)))
196	190, 195	oveq12d 7435	. . . . 5 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = ((sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))))
197	94	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ≠ 0)
198	150, 107, 197	divcan4d 12025	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐾 + (1 / 2)) · π) / π) = (𝐾 + (1 / 2)))
199	8	zred 12729	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ ℝ)
200	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ+)
201	200	rpreccld 13100	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℝ+)
202	199, 201	ltaddrpd 13123	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 < (𝐾 + (1 / 2)))
203		1red 11237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ ℝ)
204	203	rehalfcld 12519	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
205		halflt1 12489	. . . . . . . . . . . . . 14 ⊢ (1 / 2) < 1
206	205	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 / 2) < 1)
207	204, 203, 199, 206	ltadd2dd 11397	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 + (1 / 2)) < (𝐾 + 1))
208		btwnnz 12701	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℤ ∧ 𝐾 < (𝐾 + (1 / 2)) ∧ (𝐾 + (1 / 2)) < (𝐾 + 1)) → ¬ (𝐾 + (1 / 2)) ∈ ℤ)
209	8, 202, 207, 208	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐾 + (1 / 2)) ∈ ℤ)
210	198, 209	eqneltrd 2882	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (((𝐾 + (1 / 2)) · π) / π) ∈ ℤ)
211		sineq0 26769	. . . . . . . . . . 11 ⊢ (((𝐾 + (1 / 2)) · π) ∈ ℂ → ((sin‘((𝐾 + (1 / 2)) · π)) = 0 ↔ (((𝐾 + (1 / 2)) · π) / π) ∈ ℤ))
212	192, 211	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((sin‘((𝐾 + (1 / 2)) · π)) = 0 ↔ (((𝐾 + (1 / 2)) · π) / π) ∈ ℤ))
213	210, 212	mtbird 328	. . . . . . . . 9 ⊢ (𝜑 → ¬ (sin‘((𝐾 + (1 / 2)) · π)) = 0)
214	213	neqned 2964	. . . . . . . 8 ⊢ (𝜑 → (sin‘((𝐾 + (1 / 2)) · π)) ≠ 0)
215	50, 107, 52, 197	mulne0d 11894	. . . . . . . 8 ⊢ (𝜑 → (2 · π) ≠ 0)
216	193, 193, 191, 214, 215	divdiv1d 12050	. . . . . . 7 ⊢ (𝜑 → (((sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) / (2 · π)) = ((sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))))
217	193, 214	dividd 12017	. . . . . . . 8 ⊢ (𝜑 → ((sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) = 1)
218	217	oveq1d 7432	. . . . . . 7 ⊢ (𝜑 → (((sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) / (2 · π)) = (1 / (2 · π)))
219	216, 218	eqtr3d 2799	. . . . . 6 ⊢ (𝜑 → ((sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))) = (1 / (2 · π)))
220	219	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))) = (1 / (2 · π)))
221	196, 220	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = (1 / (2 · π)))
222	168, 172, 221	3eqtrrd 2802	. . 3 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (1 / (2 · π)) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
223	99, 222	eqtrd 2797	. 2 ⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
224	46	adantr 486	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π))
225	144	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → 𝑁 ∈ ℤ)
226		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ¬ (𝑁 mod 2) = 0)
227	226	neqned 2964	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (𝑁 mod 2) ≠ 0)
228		oddfl 46119	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 2) ≠ 0) → 𝑁 = ((2 · (⌊‘(𝑁 / 2))) + 1))
229	225, 227, 228	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → 𝑁 = ((2 · (⌊‘(𝑁 / 2))) + 1))
230	229	oveq2d 7433	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (1...𝑁) = (1...((2 · (⌊‘(𝑁 / 2))) + 1)))
231	230	sumeq1d 15791	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)))
232		fvoveq1 7440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 = 1 → (⌊‘(𝑁 / 2)) = (⌊‘(1 / 2)))
233		halffl 46137	. . . . . . . . . . . . . . . . 17 ⊢ (⌊‘(1 / 2)) = 0
234	232, 233	eqtrdi 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 = 1 → (⌊‘(𝑁 / 2)) = 0)
235	234	oveq2d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝑁 = 1 → (2 · (⌊‘(𝑁 / 2))) = (2 · 0))
236		2t0e0 12439	. . . . . . . . . . . . . . 15 ⊢ (2 · 0) = 0
237	235, 236	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ (𝑁 = 1 → (2 · (⌊‘(𝑁 / 2))) = 0)
238	237	oveq1d 7432	. . . . . . . . . . . . 13 ⊢ (𝑁 = 1 → ((2 · (⌊‘(𝑁 / 2))) + 1) = (0 + 1))
239	90	addlidi 11426	. . . . . . . . . . . . 13 ⊢ (0 + 1) = 1
240	238, 239	eqtrdi 2813	. . . . . . . . . . . 12 ⊢ (𝑁 = 1 → ((2 · (⌊‘(𝑁 / 2))) + 1) = 1)
241	240	oveq2d 7433	. . . . . . . . . . 11 ⊢ (𝑁 = 1 → (1...((2 · (⌊‘(𝑁 / 2))) + 1)) = (1...1))
242	241	sumeq1d 15791	. . . . . . . . . 10 ⊢ (𝑁 = 1 → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...1)(cos‘(π · 𝑛)))
243		1z 12652	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
244		coscl 16221	. . . . . . . . . . . . 13 ⊢ (π ∈ ℂ → (cos‘π) ∈ ℂ)
245	14, 244	ax-mp 5	. . . . . . . . . . . 12 ⊢ (cos‘π) ∈ ℂ
246		oveq2 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 1 → (π · 𝑛) = (π · 1))
247	14	mulridi 11241	. . . . . . . . . . . . . . 15 ⊢ (π · 1) = π
248	246, 247	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 1 → (π · 𝑛) = π)
249	248	fveq2d 6886	. . . . . . . . . . . . 13 ⊢ (𝑛 = 1 → (cos‘(π · 𝑛)) = (cos‘π))
250	249	fsum1 15837	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℤ ∧ (cos‘π) ∈ ℂ) → Σ𝑛 ∈ (1...1)(cos‘(π · 𝑛)) = (cos‘π))
251	243, 245, 250	mp2an 705	. . . . . . . . . . 11 ⊢ Σ𝑛 ∈ (1...1)(cos‘(π · 𝑛)) = (cos‘π)
252	251	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 = 1 → Σ𝑛 ∈ (1...1)(cos‘(π · 𝑛)) = (cos‘π))
253		cospi 26717	. . . . . . . . . . 11 ⊢ (cos‘π) = -1
254	253	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 = 1 → (cos‘π) = -1)
255	242, 252, 254	3eqtrd 2801	. . . . . . . . 9 ⊢ (𝑁 = 1 → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = -1)
256	255	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = 1) → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = -1)
257		2nn 12342	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
258	257	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ∈ ℕ)
259	67	rehalfcld 12519	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ)
260	259	flcld 13863	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⌊‘(𝑁 / 2)) ∈ ℤ)
261	260	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (⌊‘(𝑁 / 2)) ∈ ℤ)
262		2div2e1 12409	. . . . . . . . . . . . . . 15 ⊢ (2 / 2) = 1
263	73	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ∈ ℝ)
264	67	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 𝑁 ∈ ℝ)
265	69	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ∈ ℝ+)
266		neqne 2965	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑁 = 1 → 𝑁 ≠ 1)
267		nnne1ge2 46132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 2 ≤ 𝑁)
268	48, 266, 267	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ≤ 𝑁)
269	263, 264, 265, 268	lediv1dd 13148	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (2 / 2) ≤ (𝑁 / 2))
270	262, 269	eqbrtrrid 5145	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 1 ≤ (𝑁 / 2))
271	259	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (𝑁 / 2) ∈ ℝ)
272		flge 13870	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 / 2) ∈ ℝ ∧ 1 ∈ ℤ) → (1 ≤ (𝑁 / 2) ↔ 1 ≤ (⌊‘(𝑁 / 2))))
273	271, 243, 272	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (1 ≤ (𝑁 / 2) ↔ 1 ≤ (⌊‘(𝑁 / 2))))
274	270, 273	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 1 ≤ (⌊‘(𝑁 / 2)))
275		elnnz1 12648	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑁 / 2)) ∈ ℕ ↔ ((⌊‘(𝑁 / 2)) ∈ ℤ ∧ 1 ≤ (⌊‘(𝑁 / 2))))
276	261, 274, 275	sylanbrc 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (⌊‘(𝑁 / 2)) ∈ ℕ)
277	258, 276	nnmulcld 12317	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (2 · (⌊‘(𝑁 / 2))) ∈ ℕ)
278		nnuz 12930	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
279	277, 278	eleqtrdi 2872	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (2 · (⌊‘(𝑁 / 2))) ∈ (ℤ≥‘1))
280	14	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))) → π ∈ ℂ)
281		elfzelz 13582	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1)) → 𝑛 ∈ ℤ)
282	281	zcnd 12730	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1)) → 𝑛 ∈ ℂ)
283	282	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))) → 𝑛 ∈ ℂ)
284	280, 283	mulcld 11257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))) → (π · 𝑛) ∈ ℂ)
285	284	coscld 16225	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))) → (cos‘(π · 𝑛)) ∈ ℂ)
286		oveq2 7425	. . . . . . . . . . 11 ⊢ (𝑛 = ((2 · (⌊‘(𝑁 / 2))) + 1) → (π · 𝑛) = (π · ((2 · (⌊‘(𝑁 / 2))) + 1)))
287	286	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝑛 = ((2 · (⌊‘(𝑁 / 2))) + 1) → (cos‘(π · 𝑛)) = (cos‘(π · ((2 · (⌊‘(𝑁 / 2))) + 1))))
288	279, 285, 287	fsump1 15846	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = (Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(π · 𝑛)) + (cos‘(π · ((2 · (⌊‘(𝑁 / 2))) + 1)))))
289	14	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2)))) → π ∈ ℂ)
290		elfzelz 13582	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2)))) → 𝑛 ∈ ℤ)
291	290	zcnd 12730	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2)))) → 𝑛 ∈ ℂ)
292	289, 291	mulcomd 11258	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2)))) → (π · 𝑛) = (𝑛 · π))
293	292	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2)))) → (cos‘(π · 𝑛)) = (cos‘(𝑛 · π)))
294	293	sumeq2i 15789	. . . . . . . . . . 11 ⊢ Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(𝑛 · π))
295		dirkertrigeqlem1 46934	. . . . . . . . . . . 12 ⊢ ((⌊‘(𝑁 / 2)) ∈ ℕ → Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(𝑛 · π)) = 0)
296	276, 295	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(𝑛 · π)) = 0)
297	294, 296	eqtrid 2809	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(π · 𝑛)) = 0)
298	260	zcnd 12730	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘(𝑁 / 2)) ∈ ℂ)
299	50, 298	mulcld 11257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (⌊‘(𝑁 / 2))) ∈ ℂ)
300	107, 299, 109	adddid 11261	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (π · ((2 · (⌊‘(𝑁 / 2))) + 1)) = ((π · (2 · (⌊‘(𝑁 / 2)))) + (π · 1)))
301	107, 50, 298	mul13d 46121	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π · (2 · (⌊‘(𝑁 / 2)))) = ((⌊‘(𝑁 / 2)) · (2 · π)))
302	247	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (π · 1) = π)
303	301, 302	oveq12d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((π · (2 · (⌊‘(𝑁 / 2)))) + (π · 1)) = (((⌊‘(𝑁 / 2)) · (2 · π)) + π))
304	298, 191	mulcld 11257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((⌊‘(𝑁 / 2)) · (2 · π)) ∈ ℂ)
305	304, 107	addcomd 11440	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((⌊‘(𝑁 / 2)) · (2 · π)) + π) = (π + ((⌊‘(𝑁 / 2)) · (2 · π))))
306	300, 303, 305	3eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (𝜑 → (π · ((2 · (⌊‘(𝑁 / 2))) + 1)) = (π + ((⌊‘(𝑁 / 2)) · (2 · π))))
307	306	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (𝜑 → (cos‘(π · ((2 · (⌊‘(𝑁 / 2))) + 1))) = (cos‘(π + ((⌊‘(𝑁 / 2)) · (2 · π)))))
308		cosper 26727	. . . . . . . . . . . . 13 ⊢ ((π ∈ ℂ ∧ (⌊‘(𝑁 / 2)) ∈ ℤ) → (cos‘(π + ((⌊‘(𝑁 / 2)) · (2 · π)))) = (cos‘π))
309	107, 260, 308	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → (cos‘(π + ((⌊‘(𝑁 / 2)) · (2 · π)))) = (cos‘π))
310	253	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (cos‘π) = -1)
311	307, 309, 310	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → (cos‘(π · ((2 · (⌊‘(𝑁 / 2))) + 1))) = -1)
312	311	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (cos‘(π · ((2 · (⌊‘(𝑁 / 2))) + 1))) = -1)
313	297, 312	oveq12d 7435	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (Σ𝑛 ∈ (1...(2 · (⌊‘(𝑁 / 2))))(cos‘(π · 𝑛)) + (cos‘(π · ((2 · (⌊‘(𝑁 / 2))) + 1)))) = (0 + -1))
314		neg1cn 12231	. . . . . . . . . . 11 ⊢ -1 ∈ ℂ
315	314	addlidi 11426	. . . . . . . . . 10 ⊢ (0 + -1) = -1
316	315	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (0 + -1) = -1)
317	288, 313, 316	3eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = -1)
318	256, 317	pm2.61dan 825	. . . . . . 7 ⊢ (𝜑 → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = -1)
319	318	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...((2 · (⌊‘(𝑁 / 2))) + 1))(cos‘(π · 𝑛)) = -1)
320	231, 319	eqtrd 2797	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = -1)
321	320	oveq2d 7433	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) = ((1 / 2) + -1))
322	321	oveq1d 7432	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π) = (((1 / 2) + -1) / π))
323	167, 171	eqtrd 2797	. . . . 5 ⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))) = ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
324	323	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))) = ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
325	229	oveq1d 7432	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (𝑁 · π) = (((2 · (⌊‘(𝑁 / 2))) + 1) · π))
326	299, 109, 107	adddird 11262	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (⌊‘(𝑁 / 2))) + 1) · π) = (((2 · (⌊‘(𝑁 / 2))) · π) + (1 · π)))
327	107	mullidd 11255	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 · π) = π)
328	327	oveq2d 7433	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (⌊‘(𝑁 / 2))) · π) + (1 · π)) = (((2 · (⌊‘(𝑁 / 2))) · π) + π))
329	299, 107	mulcld 11257	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (⌊‘(𝑁 / 2))) · π) ∈ ℂ)
330	329, 107	addcomd 11440	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · (⌊‘(𝑁 / 2))) · π) + π) = (π + ((2 · (⌊‘(𝑁 / 2))) · π)))
331	326, 328, 330	3eqtrd 2801	. . . . . . . . . 10 ⊢ (𝜑 → (((2 · (⌊‘(𝑁 / 2))) + 1) · π) = (π + ((2 · (⌊‘(𝑁 / 2))) · π)))
332	331	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((2 · (⌊‘(𝑁 / 2))) + 1) · π) = (π + ((2 · (⌊‘(𝑁 / 2))) · π)))
333	50, 298	mulcomd 11258	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · (⌊‘(𝑁 / 2))) = ((⌊‘(𝑁 / 2)) · 2))
334	333	oveq1d 7432	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · (⌊‘(𝑁 / 2))) · π) = (((⌊‘(𝑁 / 2)) · 2) · π))
335	298, 50, 107	mulassd 11260	. . . . . . . . . . . 12 ⊢ (𝜑 → (((⌊‘(𝑁 / 2)) · 2) · π) = ((⌊‘(𝑁 / 2)) · (2 · π)))
336	334, 335	eqtrd 2797	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · (⌊‘(𝑁 / 2))) · π) = ((⌊‘(𝑁 / 2)) · (2 · π)))
337	336	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝜑 → (π + ((2 · (⌊‘(𝑁 / 2))) · π)) = (π + ((⌊‘(𝑁 / 2)) · (2 · π))))
338	337	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (π + ((2 · (⌊‘(𝑁 / 2))) · π)) = (π + ((⌊‘(𝑁 / 2)) · (2 · π))))
339	325, 332, 338	3eqtrd 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (𝑁 · π) = (π + ((⌊‘(𝑁 / 2)) · (2 · π))))
340	339	oveq2d 7433	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((𝐾 + (1 / 2)) · π) + (𝑁 · π)) = (((𝐾 + (1 / 2)) · π) + (π + ((⌊‘(𝑁 / 2)) · (2 · π)))))
341	192	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((𝐾 + (1 / 2)) · π) ∈ ℂ)
342	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → π ∈ ℂ)
343	304	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((⌊‘(𝑁 / 2)) · (2 · π)) ∈ ℂ)
344	341, 342, 343	addassd 11259	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π))) = (((𝐾 + (1 / 2)) · π) + (π + ((⌊‘(𝑁 / 2)) · (2 · π)))))
345	340, 344	eqtr4d 2800	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((𝐾 + (1 / 2)) · π) + (𝑁 · π)) = ((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π))))
346	345	fveq2d 6886	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) = (sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))))
347	346	oveq1d 7432	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = ((sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
348	192, 107	addcld 11256	. . . . . . . . 9 ⊢ (𝜑 → (((𝐾 + (1 / 2)) · π) + π) ∈ ℂ)
349		sinper 26726	. . . . . . . . 9 ⊢ (((((𝐾 + (1 / 2)) · π) + π) ∈ ℂ ∧ (⌊‘(𝑁 / 2)) ∈ ℤ) → (sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) = (sin‘(((𝐾 + (1 / 2)) · π) + π)))
350	348, 260, 349	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) = (sin‘(((𝐾 + (1 / 2)) · π) + π)))
351		sinppi 26734	. . . . . . . . 9 ⊢ (((𝐾 + (1 / 2)) · π) ∈ ℂ → (sin‘(((𝐾 + (1 / 2)) · π) + π)) = -(sin‘((𝐾 + (1 / 2)) · π)))
352	192, 351	syl 18	. . . . . . . 8 ⊢ (𝜑 → (sin‘(((𝐾 + (1 / 2)) · π) + π)) = -(sin‘((𝐾 + (1 / 2)) · π)))
353	350, 352	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → (sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) = -(sin‘((𝐾 + (1 / 2)) · π)))
354	353	oveq1d 7432	. . . . . 6 ⊢ (𝜑 → ((sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = (-(sin‘((𝐾 + (1 / 2)) · π)) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))))
355	194	oveq2d 7433	. . . . . 6 ⊢ (𝜑 → (-(sin‘((𝐾 + (1 / 2)) · π)) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = (-(sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))))
356	193, 193, 214	divnegd 12032	. . . . . . . . 9 ⊢ (𝜑 → -((sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) = (-(sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))))
357	217	negeqd 11479	. . . . . . . . 9 ⊢ (𝜑 → -((sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) = -1)
358	356, 357	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → (-(sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) = -1)
359	358	oveq1d 7432	. . . . . . 7 ⊢ (𝜑 → ((-(sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) / (2 · π)) = (-1 / (2 · π)))
360	193	negcld 11584	. . . . . . . 8 ⊢ (𝜑 → -(sin‘((𝐾 + (1 / 2)) · π)) ∈ ℂ)
361	360, 193, 191, 214, 215	divdiv1d 12050	. . . . . . 7 ⊢ (𝜑 → ((-(sin‘((𝐾 + (1 / 2)) · π)) / (sin‘((𝐾 + (1 / 2)) · π))) / (2 · π)) = (-(sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))))
362	86, 90	negsubi 11564	. . . . . . . . . . 11 ⊢ ((1 / 2) + -1) = ((1 / 2) − 1)
363	90, 86	negsubdi2i 11572	. . . . . . . . . . 11 ⊢ -(1 − (1 / 2)) = ((1 / 2) − 1)
364		1mhlfehlf 12491	. . . . . . . . . . . . 13 ⊢ (1 − (1 / 2)) = (1 / 2)
365	364	negeqi 11478	. . . . . . . . . . . 12 ⊢ -(1 − (1 / 2)) = -(1 / 2)
366		2cn 12344	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
367		divneg 11934	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(1 / 2) = (-1 / 2))
368	90, 366, 51, 367	mp3an 1490	. . . . . . . . . . . 12 ⊢ -(1 / 2) = (-1 / 2)
369	365, 368	eqtri 2785	. . . . . . . . . . 11 ⊢ -(1 − (1 / 2)) = (-1 / 2)
370	362, 363, 369	3eqtr2i 2791	. . . . . . . . . 10 ⊢ ((1 / 2) + -1) = (-1 / 2)
371	370	oveq1i 7427	. . . . . . . . 9 ⊢ (((1 / 2) + -1) / π) = ((-1 / 2) / π)
372		divdiv1 11954	. . . . . . . . . 10 ⊢ ((-1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈ ℂ ∧ π ≠ 0)) → ((-1 / 2) / π) = (-1 / (2 · π)))
373	314, 91, 95, 372	mp3an 1490	. . . . . . . . 9 ⊢ ((-1 / 2) / π) = (-1 / (2 · π))
374	371, 373	eqtr2i 2786	. . . . . . . 8 ⊢ (-1 / (2 · π)) = (((1 / 2) + -1) / π)
375	374	a1i 11	. . . . . . 7 ⊢ (𝜑 → (-1 / (2 · π)) = (((1 / 2) + -1) / π))
376	359, 361, 375	3eqtr3d 2805	. . . . . 6 ⊢ (𝜑 → (-(sin‘((𝐾 + (1 / 2)) · π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2 · π))) = (((1 / 2) + -1) / π))
377	354, 355, 376	3eqtrd 2801	. . . . 5 ⊢ (𝜑 → ((sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = (((1 / 2) + -1) / π))
378	377	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((sin‘((((𝐾 + (1 / 2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) = (((1 / 2) + -1) / π))
379	324, 347, 378	3eqtrrd 2802	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + -1) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
380	224, 322, 379	3eqtrd 2801	. 2 ⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
381	223, 380	pm2.61dan 825	1 ⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078   class class class wbr 5107  ‘cfv 6537  (class class class)co 7417  ℂcc 11126  ℝcr 11127  0cc0 11128  1c1 11129   + caddc 11131   · cmul 11133   < clt 11271   ≤ cle 11272   − cmin 11469  -cneg 11470   / cdiv 11899  ℕcn 12261  2c2 12323  ℤcz 12619  ℤ_≥cuz 12891  ℝ⁺crp 13046  ...cfz 13565  ⌊cfl 13855   mod cmo 13934  Σcsu 15777  sincsin 16155  cosccos 16156  πcpi 16158

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-inf2 9624  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-pre-sup 11206  ax-addf 11207

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-of 7682  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8163  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-pm 8833  df-ixp 8909  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-fsupp 9336  df-fi 9385  df-sup 9416  df-inf 9417  df-oi 9486  df-card 9948  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900  df-nn 12262  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336  df-8 12337  df-9 12338  df-n0 12533  df-z 12620  df-dec 12741  df-uz 12892  df-q 13002  df-rp 13047  df-xneg 13167  df-xadd 13168  df-xmul 13169  df-ioo 13406  df-ioc 13407  df-ico 13408  df-icc 13409  df-fz 13566  df-fzo 13714  df-fl 13857  df-mod 13935  df-seq 14070  df-exp 14130  df-fac 14342  df-bc 14371  df-hash 14399  df-shft 15144  df-cj 15190  df-re 15191  df-im 15192  df-sqrt 15326  df-abs 15327  df-limsup 15562  df-clim 15579  df-rlim 15580  df-sum 15778  df-ef 16159  df-sin 16161  df-cos 16162  df-pi 16164  df-struct 17245  df-sets 17262  df-slot 17280  df-ndx 17292  df-base 17308  df-ress 17329  df-plusg 17361  df-mulr 17362  df-starv 17363  df-sca 17364  df-vsca 17365  df-ip 17366  df-tset 17367  df-ple 17368  df-ds 17370  df-unif 17371  df-hom 17372  df-cco 17373  df-rest 17513  df-topn 17514  df-0g 17532  df-gsum 17533  df-topgen 17534  df-pt 17535  df-prds 17538  df-xrs 17594  df-qtop 17599  df-imas 17600  df-xps 17602  df-mre 17676  df-mrc 17677  df-acs 17679  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-submnd 18898  df-mulg 19197  df-cntz 19450  df-cmn 19915  df-psmet 21583  df-xmet 21584  df-met 21585  df-bl 21586  df-mopn 21587  df-fbas 21588  df-fg 21589  df-cnfld 21592  df-top 23125  df-topon 23142  df-topsp 23164  df-bases 23177  df-cld 23250  df-ntr 23251  df-cls 23252  df-nei 23329  df-lp 23367  df-perf 23368  df-cn 23458  df-cnp 23459  df-haus 23546  df-tx 23794  df-hmeo 23987  df-fil 24078  df-fm 24170  df-flim 24171  df-flf 24172  df-xms 24552  df-ms 24553  df-tms 24554  df-cncf 25112  df-limc 26100  df-dv 26101

This theorem is used by:  dirkertrigeq  46937