Theorem dirkertrigeq

Description: Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkertrigeq.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
	dirkertrigeq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dirkertrigeq.f	⊢ 𝐹 = ( 𝐷 ‘ 𝑁 )
	dirkertrigeq.h	⊢ 𝐻 = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
Assertion	dirkertrigeq	⊢ ( 𝜑 → 𝐹 = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		dirkertrigeq.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2		dirkertrigeq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		dirkertrigeq.f	⊢ 𝐹 = ( 𝐷 ‘ 𝑁 )
4		dirkertrigeq.h	⊢ 𝐻 = ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
5	3	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝐷 ‘ 𝑁 ) )
6	1	dirkerval	⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
7	2 6	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
8		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
9	2	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10	8 9	mulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
11		peano2cn	⊢ ( ( 2 · 𝑁 ) ∈ ℂ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
12	10 11	syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
13		picn	⊢ π ∈ ℂ
14	13	a1i	⊢ ( 𝜑 → π ∈ ℂ )
15		2ne0	⊢ 2 ≠ 0
16	15	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
17		pire	⊢ π ∈ ℝ
18		pipos	⊢ 0 < π
19	17 18	gt0ne0ii	⊢ π ≠ 0
20	19	a1i	⊢ ( 𝜑 → π ≠ 0 )
21	12 8 14 16 20	divdiv1d	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
22	21	eqcomd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
23	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
24		iftrue	⊢ ( ( 𝑠 mod ( 2 · π ) ) = 0 → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
25	24	adantl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
26		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
27	26	zcnd	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
28	27	adantl	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
29		recn	⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℂ )
30	29	ad2antrr	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
31		2cn	⊢ 2 ∈ ℂ
32	31 13	mulcli	⊢ ( 2 · π ) ∈ ℂ
33	32	a1i	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 · π ) ∈ ℂ )
34	31 13 15 19	mulne0i	⊢ ( 2 · π ) ≠ 0
35	34	a1i	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 · π ) ≠ 0 )
36	28 30 33 35	divassd	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) = ( 𝑘 · ( 𝑠 / ( 2 · π ) ) ) )
37	26	adantl	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
38		simpr	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 mod ( 2 · π ) ) = 0 )
39		simpl	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → 𝑠 ∈ ℝ )
40		2rp	⊢ 2 ∈ ℝ+
41		pirp	⊢ π ∈ ℝ+
42		rpmulcl	⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
43	40 41 42	mp2an	⊢ ( 2 · π ) ∈ ℝ+
44		mod0	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑠 mod ( 2 · π ) ) = 0 ↔ ( 𝑠 / ( 2 · π ) ) ∈ ℤ ) )
45	39 43 44	sylancl	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 𝑠 mod ( 2 · π ) ) = 0 ↔ ( 𝑠 / ( 2 · π ) ) ∈ ℤ ) )
46	38 45	mpbid	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 / ( 2 · π ) ) ∈ ℤ )
47	46	adantr	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 / ( 2 · π ) ) ∈ ℤ )
48	37 47	zmulcld	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · ( 𝑠 / ( 2 · π ) ) ) ∈ ℤ )
49	36 48	eqeltrd	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ )
50	27	adantl	⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
51	29	adantr	⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
52	50 51	mulcld	⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · 𝑠 ) ∈ ℂ )
53		coseq1	⊢ ( ( 𝑘 · 𝑠 ) ∈ ℂ → ( ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 ↔ ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ ) )
54	52 53	syl	⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 ↔ ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ ) )
55	54	adantlr	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 ↔ ( ( 𝑘 · 𝑠 ) / ( 2 · π ) ) ∈ ℤ ) )
56	49 55	mpbird	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 )
57	56	ralrimiva	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 )
58	57	adantll	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = 1 )
59	58	sumeq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 )
60		fzfid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 1 ... 𝑁 ) ∈ Fin )
61		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → 1 ∈ ℂ )
62		fsumconst	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) )
63	60 61 62	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) )
64	2	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
65		hashfz1	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
66	64 65	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
67	66	oveq1d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) = ( 𝑁 · 1 ) )
68	9	mulridd	⊢ ( 𝜑 → ( 𝑁 · 1 ) = 𝑁 )
69	67 68	eqtrd	⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) = 𝑁 )
70	69	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) · 1 ) = 𝑁 )
71	59 63 70	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = 𝑁 )
72	71	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( 1 / 2 ) + 𝑁 ) )
73	9	div1d	⊢ ( 𝜑 → ( 𝑁 / 1 ) = 𝑁 )
74	73	eqcomd	⊢ ( 𝜑 → 𝑁 = ( 𝑁 / 1 ) )
75	74	oveq2d	⊢ ( 𝜑 → ( ( 1 / 2 ) + 𝑁 ) = ( ( 1 / 2 ) + ( 𝑁 / 1 ) ) )
76		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
77		ax-1ne0	⊢ 1 ≠ 0
78	77	a1i	⊢ ( 𝜑 → 1 ≠ 0 )
79	76 8 9 76 16 78	divadddivd	⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 𝑁 / 1 ) ) = ( ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) / ( 2 · 1 ) ) )
80	76 76	mulcld	⊢ ( 𝜑 → ( 1 · 1 ) ∈ ℂ )
81	9 8	mulcld	⊢ ( 𝜑 → ( 𝑁 · 2 ) ∈ ℂ )
82	80 81	addcomd	⊢ ( 𝜑 → ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) = ( ( 𝑁 · 2 ) + ( 1 · 1 ) ) )
83	9 8	mulcomd	⊢ ( 𝜑 → ( 𝑁 · 2 ) = ( 2 · 𝑁 ) )
84	76	mulridd	⊢ ( 𝜑 → ( 1 · 1 ) = 1 )
85	83 84	oveq12d	⊢ ( 𝜑 → ( ( 𝑁 · 2 ) + ( 1 · 1 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
86	82 85	eqtrd	⊢ ( 𝜑 → ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) = ( ( 2 · 𝑁 ) + 1 ) )
87	8	mulridd	⊢ ( 𝜑 → ( 2 · 1 ) = 2 )
88	86 87	oveq12d	⊢ ( 𝜑 → ( ( ( 1 · 1 ) + ( 𝑁 · 2 ) ) / ( 2 · 1 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
89	75 79 88	3eqtrd	⊢ ( 𝜑 → ( ( 1 / 2 ) + 𝑁 ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
90	89	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / 2 ) + 𝑁 ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
91	72 90	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) )
92	91	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) / π ) )
93	23 25 92	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
94		iffalse	⊢ ( ¬ ( 𝑠 mod ( 2 · π ) ) = 0 → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
95	94	adantl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
96	13	a1i	⊢ ( 𝑠 ∈ ℝ → π ∈ ℂ )
97	19	a1i	⊢ ( 𝑠 ∈ ℝ → π ≠ 0 )
98	29 96 97	divcan1d	⊢ ( 𝑠 ∈ ℝ → ( ( 𝑠 / π ) · π ) = 𝑠 )
99	98	eqcomd	⊢ ( 𝑠 ∈ ℝ → 𝑠 = ( ( 𝑠 / π ) · π ) )
100	99	ad2antrr	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → 𝑠 = ( ( 𝑠 / π ) · π ) )
101		simpr	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 mod π ) = 0 )
102		simpl	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → 𝑠 ∈ ℝ )
103		mod0	⊢ ( ( 𝑠 ∈ ℝ ∧ π ∈ ℝ+ ) → ( ( 𝑠 mod π ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
104	102 41 103	sylancl	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 mod π ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
105	101 104	mpbid	⊢ ( ( 𝑠 ∈ ℝ ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) ∈ ℤ )
106	105	adantlr	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) ∈ ℤ )
107		rpreccl	⊢ ( π ∈ ℝ+ → ( 1 / π ) ∈ ℝ+ )
108	41 107	ax-mp	⊢ ( 1 / π ) ∈ ℝ+
109		moddi	⊢ ( ( ( 1 / π ) ∈ ℝ+ ∧ 𝑠 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) = ( ( ( 1 / π ) · 𝑠 ) mod ( ( 1 / π ) · ( 2 · π ) ) ) )
110	108 43 109	mp3an13	⊢ ( 𝑠 ∈ ℝ → ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) = ( ( ( 1 / π ) · 𝑠 ) mod ( ( 1 / π ) · ( 2 · π ) ) ) )
111	29 96 97	divrec2d	⊢ ( 𝑠 ∈ ℝ → ( 𝑠 / π ) = ( ( 1 / π ) · 𝑠 ) )
112	111	eqcomd	⊢ ( 𝑠 ∈ ℝ → ( ( 1 / π ) · 𝑠 ) = ( 𝑠 / π ) )
113	96 97	reccld	⊢ ( 𝑠 ∈ ℝ → ( 1 / π ) ∈ ℂ )
114	32	a1i	⊢ ( 𝑠 ∈ ℝ → ( 2 · π ) ∈ ℂ )
115	113 114	mulcomd	⊢ ( 𝑠 ∈ ℝ → ( ( 1 / π ) · ( 2 · π ) ) = ( ( 2 · π ) · ( 1 / π ) ) )
116		2cnd	⊢ ( 𝑠 ∈ ℝ → 2 ∈ ℂ )
117	116 96 113	mulassd	⊢ ( 𝑠 ∈ ℝ → ( ( 2 · π ) · ( 1 / π ) ) = ( 2 · ( π · ( 1 / π ) ) ) )
118	13 19	recidi	⊢ ( π · ( 1 / π ) ) = 1
119	118	oveq2i	⊢ ( 2 · ( π · ( 1 / π ) ) ) = ( 2 · 1 )
120	116	mulridd	⊢ ( 𝑠 ∈ ℝ → ( 2 · 1 ) = 2 )
121	119 120	eqtrid	⊢ ( 𝑠 ∈ ℝ → ( 2 · ( π · ( 1 / π ) ) ) = 2 )
122	115 117 121	3eqtrd	⊢ ( 𝑠 ∈ ℝ → ( ( 1 / π ) · ( 2 · π ) ) = 2 )
123	112 122	oveq12d	⊢ ( 𝑠 ∈ ℝ → ( ( ( 1 / π ) · 𝑠 ) mod ( ( 1 / π ) · ( 2 · π ) ) ) = ( ( 𝑠 / π ) mod 2 ) )
124	110 123	eqtr2d	⊢ ( 𝑠 ∈ ℝ → ( ( 𝑠 / π ) mod 2 ) = ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) )
125	124	adantr	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 𝑠 / π ) mod 2 ) = ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) )
126	113	adantr	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 1 / π ) ∈ ℂ )
127		id	⊢ ( 𝑠 ∈ ℝ → 𝑠 ∈ ℝ )
128	43	a1i	⊢ ( 𝑠 ∈ ℝ → ( 2 · π ) ∈ ℝ+ )
129	127 128	modcld	⊢ ( 𝑠 ∈ ℝ → ( 𝑠 mod ( 2 · π ) ) ∈ ℝ )
130	129	recnd	⊢ ( 𝑠 ∈ ℝ → ( 𝑠 mod ( 2 · π ) ) ∈ ℂ )
131	130	adantr	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 mod ( 2 · π ) ) ∈ ℂ )
132		ax-1cn	⊢ 1 ∈ ℂ
133	132 13 77 19	divne0i	⊢ ( 1 / π ) ≠ 0
134	133	a1i	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 1 / π ) ≠ 0 )
135		neqne	⊢ ( ¬ ( 𝑠 mod ( 2 · π ) ) = 0 → ( 𝑠 mod ( 2 · π ) ) ≠ 0 )
136	135	adantl	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( 𝑠 mod ( 2 · π ) ) ≠ 0 )
137	126 131 134 136	mulne0d	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 1 / π ) · ( 𝑠 mod ( 2 · π ) ) ) ≠ 0 )
138	125 137	eqnetrd	⊢ ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( 𝑠 / π ) mod 2 ) ≠ 0 )
139	138	adantr	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 / π ) mod 2 ) ≠ 0 )
140		oddfl	⊢ ( ( ( 𝑠 / π ) ∈ ℤ ∧ ( ( 𝑠 / π ) mod 2 ) ≠ 0 ) → ( 𝑠 / π ) = ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) )
141	106 139 140	syl2anc	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) = ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) )
142	141	oveq1d	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 / π ) · π ) = ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) )
143	100 142	eqtrd	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → 𝑠 = ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) )
144	143	oveq2d	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑘 · 𝑠 ) = ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) )
145	144	fveq2d	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( cos ‘ ( 𝑘 · 𝑠 ) ) = ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) )
146	145	sumeq2sdv	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) )
147	146	oveq2d	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) = ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) )
148	147	oveq1d	⊢ ( ( ( 𝑠 ∈ ℝ ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) )
149	148	adantlll	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) )
150	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod π ) = 0 ) → 𝑁 ∈ ℕ )
151	17	a1i	⊢ ( 𝑠 ∈ ℝ → π ∈ ℝ )
152	127 151 97	redivcld	⊢ ( 𝑠 ∈ ℝ → ( 𝑠 / π ) ∈ ℝ )
153	152	rehalfcld	⊢ ( 𝑠 ∈ ℝ → ( ( 𝑠 / π ) / 2 ) ∈ ℝ )
154	153	flcld	⊢ ( 𝑠 ∈ ℝ → ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ∈ ℤ )
155	154	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod π ) = 0 ) → ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ∈ ℤ )
156		eqid	⊢ ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) = ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π )
157	150 155 156	dirkertrigeqlem3	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) )
158	157	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) )
159	141	adantlll	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( 𝑠 / π ) = ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) )
160	159	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) = ( 𝑠 / π ) )
161	160	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) = ( ( 𝑠 / π ) · π ) )
162	161	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) )
163	162	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) )
164	161	fvoveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) = ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) )
165	164	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) )
166	163 165	oveq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) )
167	98	oveq2d	⊢ ( 𝑠 ∈ ℝ → ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) )
168	167	fveq2d	⊢ ( 𝑠 ∈ ℝ → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
169	98	fvoveq1d	⊢ ( 𝑠 ∈ ℝ → ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) = ( sin ‘ ( 𝑠 / 2 ) ) )
170	169	oveq2d	⊢ ( 𝑠 ∈ ℝ → ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) )
171	168 170	oveq12d	⊢ ( 𝑠 ∈ ℝ → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
172	171	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
173	172	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( 𝑠 / π ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( 𝑠 / π ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
174	166 173	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) ) ) / ( ( 2 · π ) · ( sin ‘ ( ( ( ( 2 · ( ⌊ ‘ ( ( 𝑠 / π ) / 2 ) ) ) + 1 ) · π ) / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
175	149 158 174	3eqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
176		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → 𝑠 ∈ ℝ )
177		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ¬ ( 𝑠 mod π ) = 0 )
178	176 41 103	sylancl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( 𝑠 mod π ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
179	177 178	mtbid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ¬ ( 𝑠 / π ) ∈ ℤ )
180	176	recnd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → 𝑠 ∈ ℂ )
181		sineq0	⊢ ( 𝑠 ∈ ℂ → ( ( sin ‘ 𝑠 ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
182	180 181	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ 𝑠 ) = 0 ↔ ( 𝑠 / π ) ∈ ℤ ) )
183	179 182	mtbird	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ¬ ( sin ‘ 𝑠 ) = 0 )
184	183	neqned	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( sin ‘ 𝑠 ) ≠ 0 )
185	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → 𝑁 ∈ ℕ )
186	176 184 185	dirkertrigeqlem2	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
187	186	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
188	187	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) ∧ ¬ ( 𝑠 mod π ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
189	175 188	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) )
190	95 189	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ ( 𝑠 mod ( 2 · π ) ) = 0 ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
191	93 190	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
192	191	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( ( 1 / 2 ) + Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑘 · 𝑠 ) ) ) / π ) ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
193	4 192	eqtr2id	⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = 𝐻 )
194	5 7 193	3eqtrd	⊢ ( 𝜑 → 𝐹 = 𝐻 )