fourierdlem76 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem76		Structured version Visualization version GIF version

Theorem fourierdlem76 45493

Description: Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem76.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem76.xre	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem76.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem76.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem76.v	⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
fourierdlem76.fcn	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
fourierdlem76.r	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
fourierdlem76.l	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
fourierdlem76.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem76.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem76.altb	⊢ (𝜑 → 𝐴 < 𝐵)
fourierdlem76.ab	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem76.n0	⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem76.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem76.o	⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
fourierdlem76.q	⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
fourierdlem76.t	⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
fourierdlem76.n	⊢ 𝑁 = ((♯‘𝑇) − 1)
fourierdlem76.s	⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
fourierdlem76.d	⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
fourierdlem76.e	⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))
fourierdlem76.ch	⊢ (𝜒 ↔ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))

**Assertion**
Ref	Expression
fourierdlem76	⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))

Distinct variable groups: 𝐴,𝑠 𝐵,𝑠 𝐶,𝑠 𝐹,𝑠 𝐿,𝑠 𝑖,𝑀,𝑗 𝑚,𝑀,𝑝,𝑖 𝑓,𝑁 𝑄,𝑠 𝑅,𝑠 𝑆,𝑓 𝑆,𝑠 𝑇,𝑓 𝑖,𝑉,𝑗,𝑠 𝑉,𝑝 𝑖,𝑋,𝑗,𝑠 𝑚,𝑋,𝑝 𝜒,𝑠 𝜑,𝑓 𝜑,𝑖,𝑗,𝑠 Allowed substitution hints: 𝜑(𝑚,𝑝) 𝜒(𝑓,𝑖,𝑗,𝑚,𝑝) 𝐴(𝑓,𝑖,𝑗,𝑚,𝑝) 𝐵(𝑓,𝑖,𝑗,𝑚,𝑝) 𝐶(𝑓,𝑖,𝑗,𝑚,𝑝) 𝐷(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝) 𝑃(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝) 𝑄(𝑓,𝑖,𝑗,𝑚,𝑝) 𝑅(𝑓,𝑖,𝑗,𝑚,𝑝) 𝑆(𝑖,𝑗,𝑚,𝑝) 𝑇(𝑖,𝑗,𝑚,𝑠,𝑝) 𝐸(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝) 𝐹(𝑓,𝑖,𝑗,𝑚,𝑝) 𝐿(𝑓,𝑖,𝑗,𝑚,𝑝) 𝑀(𝑓,𝑠) 𝑁(𝑖,𝑗,𝑚,𝑠,𝑝) 𝑂(𝑓,𝑖,𝑗,𝑚,𝑠,𝑝) 𝑉(𝑓,𝑚) 𝑋(𝑓)

Proof of Theorem fourierdlem76 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem76.ch	. . 3 ⊢ (𝜒 ↔ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
2		eqid 2727	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3		eqid 2727	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4		eqid 2727	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5		simplll 774	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
6	1, 5	sylbi 216	. . . . . . . . . 10 ⊢ (𝜒 → 𝜑)
7	6	adantr 480	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8		ioossicc 13434	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9		fourierdlem76.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
10	9	rexrd 11286	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
11	6, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
12	11	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ^*)
13		fourierdlem76.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	13	rexrd 11286	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
15	6, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ^*)
17		elioore 13378	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
18	17	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
19	6, 9	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ∈ ℝ)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21		fourierdlem76.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22		prfi 9338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝐴, 𝐵} ∈ Fin
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin)
24		fzfid 13962	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
25		fourierdlem76.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
26	25	rnmptfi 44467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27		infi 9284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
28	24, 26, 27	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29		unfi 9188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
30	23, 28, 29	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
31	21, 30	eqeltrid 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ Fin)
32		prssg 4818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
33	9, 13, 32	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
34	9, 13, 33	mpbi2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35		inss2 4225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossre 13409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴(,)𝐵) ⊆ ℝ
37	35, 36	sstri 3987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
39	34, 38	unssd 4182	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
40	21, 39	eqsstrid 4026	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
41		fourierdlem76.s	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42		fourierdlem76.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘𝑇) − 1)
43	31, 40, 41, 42	fourierdlem36 45454	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44	6, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
45		isof1o 7325	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
46		f1of 6833	. . . . . . . . . . . . . . . 16 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
47	44, 45, 46	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶𝑇)
48	6, 40	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑇 ⊆ ℝ)
49	47, 48	fssd 6734	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
52	1, 51	sylbi 216	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (0..^𝑁))
53		elfzofz 13672	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
54	52, 53	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑗 ∈ (0...𝑁))
55	54	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
56	50, 55	ffvelcdmd 7089	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ)
57	43, 45, 46	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
58		frn 6723	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆 ⊆ 𝑇)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝑆 ⊆ 𝑇)
60	9	leidd 11802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
61		fourierdlem76.altb	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 < 𝐵)
62	9, 13, 61	ltled 11384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63	9, 13, 9, 60, 62	eliccd 44812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
64	13	leidd 11802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
65	9, 13, 13, 62, 64	eliccd 44812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
66		prssg 4818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
67	9, 13, 66	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
68	63, 65, 67	mpbi2and 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
69	35, 8	sstri 3987	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
71	68, 70	unssd 4182	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
72	21, 71	eqsstrid 4026	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
73	59, 72	sstrd 3988	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
74	6, 73	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75		ffun 6719	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
76	49, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → Fun 𝑆)
77		fdm 6725	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
78	49, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom 𝑆 = (0...𝑁))
79	78	eqcomd 2733	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (0...𝑁) = dom 𝑆)
80	54, 79	eleqtrd 2830	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ dom 𝑆)
81		fvelrn 7080	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆) → (𝑆‘𝑗) ∈ ran 𝑆)
82	76, 80, 81	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ran 𝑆)
83	74, 82	sseldd 3979	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
84		iccgelb 13404	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝑗))
85	11, 15, 83, 84	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ≤ (𝑆‘𝑗))
86	85	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆‘𝑗))
87	56	rexrd 11286	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ^*)
88		fzofzp1 13753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
89	52, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
90	49, 89	ffvelcdmd 7089	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
91	90	rexrd 11286	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
92	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
93		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
94		ioogtlb 44803	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
95	87, 92, 93, 94	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
96	20, 56, 18, 86, 95	lelttrd 11394	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
97	90	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
98	6, 13	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐵 ∈ ℝ)
99	98	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100		iooltub 44818	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
101	87, 92, 93, 100	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
102	89, 79	eleqtrd 2830	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103		fvelrn 7080	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
104	76, 102, 103	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
105	74, 104	sseldd 3979	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106		iccleub 13403	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
107	11, 15, 105, 106	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108	107	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
109	18, 97, 99, 101, 108	ltletrd 11396	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
110	12, 16, 18, 96, 109	eliood 44806	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
111	8, 110	sselid 3976	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112		fourierdlem76.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
113	112	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114		fourierdlem76.xre	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ)
115	114	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
116	9, 13	iccssred 13435	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117	116	sselda 3978	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118	115, 117	readdcld 11265	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119	113, 118	ffvelcdmd 7089	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
120	7, 111, 119	syl2anc 583	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121	120	recnd 11264	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122		fourierdlem76.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
123	122	recnd 11264	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
124	6, 123	syl 17	. . . . . . . 8 ⊢ (𝜒 → 𝐶 ∈ ℂ)
125	124	adantr 480	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126	121, 125	subcld 11593	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127		ioossre 13409	. . . . . . . . 9 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129	128	sselda 3978	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130	129	recnd 11264	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131		nne 2939	. . . . . . . . . . . 12 ⊢ (¬ 𝑠 ≠ 0 ↔ 𝑠 = 0)
132	131	biimpi 215	. . . . . . . . . . 11 ⊢ (¬ 𝑠 ≠ 0 → 𝑠 = 0)
133	132	eqcomd 2733	. . . . . . . . . 10 ⊢ (¬ 𝑠 ≠ 0 → 0 = 𝑠)
134	133	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136	135	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137	134, 136	eqeltrd 2828	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138		fourierdlem76.n0	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139	138	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140	137, 139	condan 817	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
141	7, 111, 140	syl2anc 583	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142	126, 130, 141	divcld 12012	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143		2cnd 12312	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144	130	halfcld 12479	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145	144	sincld 16098	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146	143, 145	mulcld 11256	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
147	17	recnd 11264	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148	147	adantl 481	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149	148	halfcld 12479	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150	149	sincld 16098	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151		2ne0 12338	. . . . . . . 8 ⊢ 2 ≠ 0
152	151	a1i 11	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153		fourierdlem76.ab	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
154	6, 153	syl 17	. . . . . . . . . 10 ⊢ (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155	154	adantr 480	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156	155, 111	sseldd 3979	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157		fourierdlem44 45462	. . . . . . . 8 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158	156, 141, 157	syl2anc 583	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159	143, 150, 152, 158	mulne0d 11888	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160	130, 146, 159	divcld 12012	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161		eqid 2727	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162		eqid 2727	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163	141	neneqd 2940	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164		velsn 4640	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
165	163, 164	sylnibr 329	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166	130, 165	eldifd 3955	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167		eqid 2727	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168		eqid 2727	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169		elfzofz 13672	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170	169	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171		pire 26380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ∈ ℝ
172	171	renegcli 11543	. . . . . . . . . . . . . . . . . . . 20 ⊢ -π ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -π ∈ ℝ)
174	173, 114	readdcld 11265	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
175	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → π ∈ ℝ)
176	175, 114	readdcld 11265	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
177	174, 176	iccssred 13435	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178	177	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179		fourierdlem76.p	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
180		fourierdlem76.m	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℕ)
181		fourierdlem76.v	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
182	179, 180, 181	fourierdlem15 45433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183	182	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184	183, 170	ffvelcdmd 7089	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185	178, 184	sseldd 3979	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
186	114	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187	185, 186	resubcld 11664	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
188	25	fvmpt2 7010	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
189	170, 187, 188	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
190	189, 187	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
191	190	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
192	191	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
193	1, 192	sylbi 216	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ)
194		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
195	194	oveq1d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
196	195	cbvmptv 5255	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
197	25, 196	eqtri 2755	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
198	197	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
199		fveq2 6891	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
200	199	oveq1d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201	200	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202		fzofzp1 13753	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203	202	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204	183, 203	ffvelcdmd 7089	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205	178, 204	sseldd 3979	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206	205, 186	resubcld 11664	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207	198, 201, 203, 206	fvmptd 7006	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208	207, 206	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209	208	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
211	1, 210	sylbi 216	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212	179	fourierdlem2 45420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
213	180, 212	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
214	181, 213	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
215	214	simprrd 773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
216	215	r19.21bi 3243	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
217	185, 205, 186, 216	ltsub1dd 11848	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218	217, 189, 207	3brtr4d 5174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
219	218	adantlr 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
220	219	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
221	1, 220	sylbi 216	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
222	1	biimpi 215	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
223	222	simplrd 769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑖 ∈ (0..^𝑀))
224	6, 223, 185	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ)
225	224	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ^*)
226	225	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
227	6, 223, 205	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228	227	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
229	228	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
230	6, 114	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑋 ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13378	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233	232	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234	231, 233	readdcld 11265	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
235	6, 223, 189	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
236	235	oveq2d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) = (𝑋 + ((𝑉‘𝑖) − 𝑋)))
237	230	recnd 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑋 ∈ ℂ)
238	224	recnd 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℂ)
239	237, 238	pncan3d 11596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘𝑖) − 𝑋)) = (𝑉‘𝑖))
240	236, 239	eqtr2d 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
241	240	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
242	193	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
243	193	rexrd 11286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ^*)
244	243	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
245	211	rexrd 11286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
247		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
248		ioogtlb 44803	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
249	244, 246, 247, 248	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
250	242, 233, 231, 249	ltadd2dd 11395	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
251	241, 250	eqbrtrd 5164	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
252	211	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253		iooltub 44818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254	244, 246, 247, 253	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255	233, 252, 231, 254	ltadd2dd 11395	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
256	6, 223, 207	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257	256	oveq2d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258	227	recnd 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259	237, 258	pncan3d 11596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260	257, 259	eqtrd 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261	260	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262	255, 261	breqtrd 5168	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263	226, 229, 234, 251, 262	eliood 44806	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
264		fvres 6910	. . . . . . . . . . . . 13 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265	263, 264	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266	265	eqcomd 2733	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267	266	mpteq2dva 5242	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268		ioosscn 13410	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270		fourierdlem76.fcn	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
271	6, 223, 270	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272		ioosscn 13410	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273	272	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274	269, 271, 273, 237, 263	fourierdlem23 45441	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275	267, 274	eqeltrd 2828	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
276	6, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
277		ioossre 13409	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278	277	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279		eqid 2727	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280		ioossre 13409	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281	280	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282	233, 254	ltned 11372	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283		fourierdlem76.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
284	6, 223, 283	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
285	260	eqcomd 2733	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286	285	oveq2d 7430	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
287	284, 286	eleqtrd 2830	. . . . . . . . . 10 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
288	211	recnd 11264	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289	276, 230, 278, 279, 263, 281, 282, 287, 288	fourierdlem53 45470	. . . . . . . . 9 ⊢ (𝜒 → 𝐿 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
290	49, 54	ffvelcdmd 7089	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
291		elfzoelz 13656	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292		zre 12584	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
293	52, 291, 292	3syl 18	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑗 ∈ ℝ)
294	293	ltp1d 12166	. . . . . . . . . 10 ⊢ (𝜒 → 𝑗 < (𝑗 + 1))
295		isorel 7328	. . . . . . . . . . 11 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
296	44, 54, 89, 295	syl12anc 836	. . . . . . . . . 10 ⊢ (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
297	294, 296	mpbid 231	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
298	1	simprbi 496	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
299		eqid 2727	. . . . . . . . 9 ⊢ if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300		eqid 2727	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301	193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300	fourierdlem33 45451	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
302		eqidd 2728	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304	303	oveq2d 7430	. . . . . . . . . . 11 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305	304	fveq2d 6895	. . . . . . . . . 10 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306	243	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) ∈ ℝ^*)
307	245	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
308	90	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309	193, 211, 290, 90, 297, 298	fourierdlem10 45428	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑄‘𝑖) ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310	309	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
311	193, 290, 90, 310, 297	lelttrd 11394	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑆‘(𝑗 + 1)))
312	311	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < (𝑆‘(𝑗 + 1)))
313	211	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314	309	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315	314	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316		neqne 2943	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317	316	necomd 2991	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318	317	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319	308, 313, 315, 318	leneltd 11390	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320	306, 307, 308, 312, 319	eliood 44806	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
321	230, 90	readdcld 11265	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322	276, 321	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323	322	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324	302, 305, 320, 323	fvmptd 7006	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325	324	ifeq2da 4556	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326	298	resmptd 6038	. . . . . . . . 9 ⊢ (𝜒 → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327	326	oveq1d 7429	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
328	301, 325, 327	3eltr3d 2842	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
329		ax-resscn 11187	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
330	128, 329	sstrdi 3990	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
331	90	recnd 11264	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332	168, 330, 124, 331	constlimc 44935	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘(𝑗 + 1))))
333	167, 168, 161, 121, 125, 328, 332	sublimc 44963	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘(𝑗 + 1))))
334	330, 162, 331	idlimc 44937	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘(𝑗 + 1))))
335	6, 105	jca 511	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336		eleq1 2816	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337	336	anbi2d 628	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338		neeq1 2998	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339	337, 338	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340	339, 140	vtoclg 3538	. . . . . . 7 ⊢ ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
341	90, 335, 340	sylc 65	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342	161, 162, 2, 126, 166, 333, 334, 341, 141	divlimc 44967	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘(𝑗 + 1))))
343		eqid 2727	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344	143, 150	mulcld 11256	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345	159	neneqd 2940	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346		2re 12308	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
347	346	a1i 11	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
348	17	rehalfcld 12481	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349	348	resincld 16111	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350	349	adantl 481	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351	347, 350	remulcld 11266	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352		elsng 4638	. . . . . . . . 9 ⊢ ((2 · (sin‘(𝑠 / 2))) ∈ ℝ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
353	351, 352	syl 17	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
354	345, 353	mtbird 325	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355	344, 354	eldifd 3955	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356		eqid 2727	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357		eqid 2727	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358		2cnd 12312	. . . . . . . 8 ⊢ (𝜒 → 2 ∈ ℂ)
359	356, 330, 358, 331	constlimc 44935	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘(𝑗 + 1))))
360	348	ad2antrl 727	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361		recn 11220	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362	361	sincld 16098	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363	362	adantl 481	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364		eqid 2727	. . . . . . . . 9 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365		2cn 12309	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
366		eldifsn 4786	. . . . . . . . . . 11 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367	365, 151, 366	mpbir2an 710	. . . . . . . . . 10 ⊢ 2 ∈ (ℂ ∖ {0})
368	367	a1i 11	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ (ℂ ∖ {0}))
369	151	a1i 11	. . . . . . . . 9 ⊢ (𝜒 → 2 ≠ 0)
370	162, 356, 364, 148, 368, 334, 359, 369, 152	divlimc 44967	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘(𝑗 + 1))))
371		sinf 16092	. . . . . . . . . . . . . 14 ⊢ sin:ℂ⟶ℂ
372	371	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → sin:ℂ⟶ℂ)
373	329	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℝ ⊆ ℂ)
374	372, 373	feqresmpt 6962	. . . . . . . . . . . 12 ⊢ (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375	374	mptru 1541	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376		resincncf 45186	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377	375, 376	eqeltrri 2825	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378	377	a1i 11	. . . . . . . . 9 ⊢ (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
379	90	rehalfcld 12481	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380		fveq2 6891	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381	378, 379, 380	cnmptlimc 25806	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘(𝑗 + 1)) / 2)))
382		fveq2 6891	. . . . . . . 8 ⊢ (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383		fveq2 6891	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384	383	ad2antll 728	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385	360, 363, 370, 381, 382, 384	limcco 25809	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘(𝑗 + 1))))
386	356, 357, 343, 143, 150, 359, 385	mullimc 44927	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘(𝑗 + 1))))
387	331	halfcld 12479	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388	387	sincld 16098	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389	154, 105	sseldd 3979	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390		fourierdlem44 45462	. . . . . . . 8 ⊢ (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391	389, 341, 390	syl2anc 583	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392	358, 388, 369, 391	mulne0d 11888	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393	162, 343, 3, 148, 355, 334, 386, 392, 159	divlimc 44967	. . . . 5 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘(𝑗 + 1))))
394	2, 3, 4, 142, 160, 342, 393	mullimc 44927	. . . 4 ⊢ (𝜒 → (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘(𝑗 + 1))))
395		fourierdlem76.d	. . . . 5 ⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
396	395	a1i 11	. . . 4 ⊢ (𝜒 → 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))))
397		fourierdlem76.o	. . . . . . 7 ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
398	397	reseq1i 5975	. . . . . 6 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
399		ioossicc 13434	. . . . . . . 8 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
400		iccss 13416	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
401	19, 98, 85, 107, 400	syl22anc 838	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402	399, 401	sstrid 3989	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403	402	resmptd 6038	. . . . . 6 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404	398, 403	eqtrid 2779	. . . . 5 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405	404	oveq1d 7429	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘(𝑗 + 1))))
406	394, 396, 405	3eltr4d 2843	. . 3 ⊢ (𝜒 → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
407	1, 406	sylbir 234	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
408	242, 249	gtned 11371	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
409		fourierdlem76.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
410	6, 223, 409	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
411	240	oveq2d 7430	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
412	410, 411	eleqtrd 2830	. . . . . . . . . 10 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
413	193	recnd 11264	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℂ)
414	276, 230, 278, 279, 263, 281, 408, 412, 413	fourierdlem53 45470	. . . . . . . . 9 ⊢ (𝜒 → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
415		eqid 2727	. . . . . . . . 9 ⊢ if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)))
416		eqid 2727	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
417	193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416	fourierdlem32 45450	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
418		eqidd 2728	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419		oveq2 7422	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘𝑗)))
420	419	fveq2d 6895	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑆‘𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
421	420	adantl 481	. . . . . . . . . 10 ⊢ (((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) ∧ 𝑠 = (𝑆‘𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
422	243	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ^*)
423	245	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
424	290	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ℝ)
425	193	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ)
426	310	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
427		neqne 2943	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘𝑗) = (𝑄‘𝑖) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
428	427	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
429	425, 424, 426, 428	leneltd 11390	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) < (𝑆‘𝑗))
430	90	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431	211	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432	297	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
433	314	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434	424, 430, 431, 432, 433	ltletrd 11396	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑄‘(𝑖 + 1)))
435	422, 423, 424, 429, 434	eliood 44806	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
436	230, 290	readdcld 11265	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘𝑗)) ∈ ℝ)
437	276, 436	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
438	437	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
439	418, 421, 435, 438	fvmptd 7006	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
440	439	ifeq2da 4556	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))))
441	326	oveq1d 7429	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
442	417, 440, 441	3eltr3d 2842	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
443	290	recnd 11264	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
444	168, 330, 124, 443	constlimc 44935	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘𝑗)))
445	167, 168, 161, 121, 125, 442, 444	sublimc 44963	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘𝑗)))
446	330, 162, 443	idlimc 44937	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘𝑗)))
447	6, 83	jca 511	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
448		eleq1 2816	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
449	448	anbi2d 628	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵))))
450		neeq1 2998	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ≠ 0 ↔ (𝑆‘𝑗) ≠ 0))
451	449, 450	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0)))
452	451, 140	vtoclg 3538	. . . . . . 7 ⊢ ((𝑆‘𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0))
453	83, 447, 452	sylc 65	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ≠ 0)
454	161, 162, 2, 126, 166, 445, 446, 453, 141	divlimc 44967	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘𝑗)))
455	356, 330, 358, 443	constlimc 44935	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘𝑗)))
456	348	ad2antrl 727	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457	162, 356, 364, 148, 368, 446, 455, 369, 152	divlimc 44967	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘𝑗)))
458	290	rehalfcld 12481	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℝ)
459		fveq2 6891	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆‘𝑗) / 2)))
460	378, 458, 459	cnmptlimc 25806	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘𝑗) / 2)))
461		fveq2 6891	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
462	461	ad2antll 728	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
463	456, 363, 457, 460, 382, 462	limcco 25809	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘𝑗)))
464	356, 357, 343, 143, 150, 455, 463	mullimc 44927	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘𝑗)))
465	443	halfcld 12479	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℂ)
466	465	sincld 16098	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ℂ)
467	154, 83	sseldd 3979	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (-π[,]π))
468		fourierdlem44 45462	. . . . . . . 8 ⊢ (((𝑆‘𝑗) ∈ (-π[,]π) ∧ (𝑆‘𝑗) ≠ 0) → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
469	467, 453, 468	syl2anc 583	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
470	358, 466, 369, 469	mulne0d 11888	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ≠ 0)
471	162, 343, 3, 148, 355, 446, 464, 470, 159	divlimc 44967	. . . . 5 ⊢ (𝜒 → ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘𝑗)))
472	2, 3, 4, 142, 160, 454, 471	mullimc 44927	. . . 4 ⊢ (𝜒 → (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘𝑗)))
473		fourierdlem76.e	. . . . 5 ⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))
474	473	a1i 11	. . . 4 ⊢ (𝜒 → 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))))
475	404	oveq1d 7429	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘𝑗)))
476	472, 474, 475	3eltr4d 2843	. . 3 ⊢ (𝜒 → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
477	1, 476	sylbir 234	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
478	298	sselda 3978	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
479	478, 266	syldan 590	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480	479	mpteq2dva 5242	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481	225	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
482	228	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
483	230	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484	483, 129	readdcld 11265	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485	240	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
486	193	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
487	243	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
488	245	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
489	487, 488, 478, 248	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) < 𝑠)
490	486, 18, 483, 489	ltadd2dd 11395	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
491	485, 490	eqbrtrd 5164	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
492	211	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493	487, 488, 478, 253	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
494	18, 492, 483, 493	ltadd2dd 11395	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495	260	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496	494, 495	breqtrd 5168	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497	481, 482, 484, 491, 496	eliood 44806	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
498	269, 271, 330, 237, 497	fourierdlem23 45441	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499	480, 498	eqeltrd 2828	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500		ssid 4000	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
501	500	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ℂ ⊆ ℂ)
502	330, 124, 501	constcncfg 45183	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503	499, 502	subcncf 25360	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504	166	ralrimiva 3141	. . . . . . . 8 ⊢ (𝜒 → ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505		dfss3 3966	. . . . . . . 8 ⊢ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506	504, 505	sylibr 233	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507		difssd 4128	. . . . . . 7 ⊢ (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508	506, 507	idcncfg 45184	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509	503, 508	divcncf 25363	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510	330, 501	idcncfg 45184	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511	355, 343	fmptd 7118	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512	330, 358, 501	constcncfg 45183	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513		sincn 26368	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
514	513	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → sin ∈ (ℂ–cn→ℂ))
515	367	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜒 → 2 ∈ (ℂ ∖ {0}))
516	330, 515, 507	constcncfg 45183	. . . . . . . . . . 11 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517	510, 516	divcncf 25363	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518	514, 517	cncfmpt1f 24821	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519	512, 518	mulcncf 25361	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520		cncfcdm 24805	. . . . . . . 8 ⊢ (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) → ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
521	507, 519, 520	syl2anc 583	. . . . . . 7 ⊢ (𝜒 → ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522	511, 521	mpbird 257	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523	510, 522	divcncf 25363	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524	509, 523	mulcncf 25361	. . . 4 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525	404, 524	eqeltrd 2828	. . 3 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
526	1, 525	sylbir 234	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527	407, 477, 526	jca31 514	1 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1534 ⊤wtru 1535 ∈ wcel 2099 ≠ wne 2935 ∀wral 3056 {crab 3427 ∖ cdif 3941 ∪ cun 3942 ∩ cin 3943 ⊆ wss 3944 ifcif 4524 {csn 4624 {cpr 4626 class class class wbr 5142 ↦ cmpt 5225 dom cdm 5672 ran crn 5673 ↾ cres 5674 ℩cio 6492 Fun wfun 6536 ⟶wf 6538 –1-1-onto→wf1o 6541 ‘cfv 6542 Isom wiso 6543 (class class class)co 7414 ↑_m cmap 8836 Fincfn 8955 ℂcc 11128 ℝcr 11129 0cc0 11130 1c1 11131 + caddc 11133 · cmul 11135 ℝ^*cxr 11269 < clt 11270 ≤ cle 11271 − cmin 11466 -cneg 11467 / cdiv 11893 ℕcn 12234 2c2 12289 ℤcz 12580 (,)cioo 13348 [,)cico 13350 [,]cicc 13351 ...cfz 13508 ..^cfzo 13651 ♯chash 14313 sincsin 16031 πcpi 16034 ↾_t crest 17393 TopOpenctopn 17394 ℂ_fldccnfld 21266 –cn→ccncf 24783 lim_ℂ climc 25778

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-inf2 9656 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207 ax-pre-sup 11208 ax-addf 11209

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-iin 4994 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7865 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-er 8718 df-map 8838 df-pm 8839 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9378 df-fi 9426 df-sup 9457 df-inf 9458 df-oi 9525 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-div 11894 df-nn 12235 df-2 12297 df-3 12298 df-4 12299 df-5 12300 df-6 12301 df-7 12302 df-8 12303 df-9 12304 df-n0 12495 df-z 12581 df-dec 12700 df-uz 12845 df-q 12955 df-rp 12999 df-xneg 13116 df-xadd 13117 df-xmul 13118 df-ioo 13352 df-ioc 13353 df-ico 13354 df-icc 13355 df-fz 13509 df-fzo 13652 df-fl 13781 df-mod 13859 df-seq 13991 df-exp 14051 df-fac 14257 df-bc 14286 df-hash 14314 df-shft 15038 df-cj 15070 df-re 15071 df-im 15072 df-sqrt 15206 df-abs 15207 df-limsup 15439 df-clim 15456 df-rlim 15457 df-sum 15657 df-ef 16035 df-sin 16037 df-cos 16038 df-pi 16040 df-struct 17107 df-sets 17124 df-slot 17142 df-ndx 17154 df-base 17172 df-ress 17201 df-plusg 17237 df-mulr 17238 df-starv 17239 df-sca 17240 df-vsca 17241 df-ip 17242 df-tset 17243 df-ple 17244 df-ds 17246 df-unif 17247 df-hom 17248 df-cco 17249 df-rest 17395 df-topn 17396 df-0g 17414 df-gsum 17415 df-topgen 17416 df-pt 17417 df-prds 17420 df-xrs 17475 df-qtop 17480 df-imas 17481 df-xps 17483 df-mre 17557 df-mrc 17558 df-acs 17560 df-mgm 18591 df-sgrp 18670 df-mnd 18686 df-submnd 18732 df-mulg 19015 df-cntz 19259 df-cmn 19728 df-psmet 21258 df-xmet 21259 df-met 21260 df-bl 21261 df-mopn 21262 df-fbas 21263 df-fg 21264 df-cnfld 21267 df-top 22783 df-topon 22800 df-topsp 22822 df-bases 22836 df-cld 22910 df-ntr 22911 df-cls 22912 df-nei 22989 df-lp 23027 df-perf 23028 df-cn 23118 df-cnp 23119 df-haus 23206 df-tx 23453 df-hmeo 23646 df-fil 23737 df-fm 23829 df-flim 23830 df-flf 23831 df-xms 24213 df-ms 24214 df-tms 24215 df-cncf 24785 df-limc 25782 df-dv 25783

This theorem is referenced by: fourierdlem86 45503

W3C validator