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 42474

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 2823	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3		eqid 2823	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4		eqid 2823	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5		simplll 773	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
6	1, 5	sylbi 219	. . . . . . . . . 10 ⊢ (𝜒 → 𝜑)
7	6	adantr 483	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8		ioossicc 12825	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9		fourierdlem76.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
10	9	rexrd 10693	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
11	6, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
12	11	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ^*)
13		fourierdlem76.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	13	rexrd 10693	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
15	6, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
16	15	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ^*)
17		elioore 12771	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
18	17	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
19	6, 9	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ∈ ℝ)
20	19	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21		fourierdlem76.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22		prfi 8795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝐴, 𝐵} ∈ Fin
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin)
24		fzfid 13344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
25		fourierdlem76.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
26	25	rnmptfi 41434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27		infi 8744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
28	24, 26, 27	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29		unfi 8787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
30	23, 28, 29	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
31	21, 30	eqeltrid 2919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ Fin)
32		prssg 4754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
33	9, 13, 32	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
34	9, 13, 33	mpbi2and 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35		inss2 4208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossre 12801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴(,)𝐵) ⊆ ℝ
37	35, 36	sstri 3978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
39	34, 38	unssd 4164	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
40	21, 39	eqsstrid 4017	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
41		fourierdlem76.s	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42		fourierdlem76.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘𝑇) − 1)
43	31, 40, 41, 42	fourierdlem36 42435	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44	6, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
45		isof1o 7078	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
46		f1of 6617	. . . . . . . . . . . . . . . 16 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
47	44, 45, 46	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶𝑇)
48	6, 40	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑇 ⊆ ℝ)
49	47, 48	fssd 6530	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51		simpllr 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
52	1, 51	sylbi 219	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (0..^𝑁))
53		elfzofz 13056	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
54	52, 53	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑗 ∈ (0...𝑁))
55	54	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
56	50, 55	ffvelrnd 6854	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ)
57	43, 45, 46	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
58		frn 6522	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆 ⊆ 𝑇)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝑆 ⊆ 𝑇)
60	9	leidd 11208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
61		fourierdlem76.altb	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 < 𝐵)
62	9, 13, 61	ltled 10790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63	9, 13, 9, 60, 62	eliccd 41786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
64	13	leidd 11208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
65	9, 13, 13, 62, 64	eliccd 41786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
66		prssg 4754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
67	9, 13, 66	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
68	63, 65, 67	mpbi2and 710	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
69	35, 8	sstri 3978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
71	68, 70	unssd 4164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
72	21, 71	eqsstrid 4017	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
73	59, 72	sstrd 3979	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
74	6, 73	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75		ffun 6519	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
76	49, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → Fun 𝑆)
77		fdm 6524	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
78	49, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom 𝑆 = (0...𝑁))
79	78	eqcomd 2829	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (0...𝑁) = dom 𝑆)
80	54, 79	eleqtrd 2917	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ dom 𝑆)
81		fvelrn 6846	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆) → (𝑆‘𝑗) ∈ ran 𝑆)
82	76, 80, 81	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ran 𝑆)
83	74, 82	sseldd 3970	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
84		iccgelb 12796	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝑗))
85	11, 15, 83, 84	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ≤ (𝑆‘𝑗))
86	85	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆‘𝑗))
87	56	rexrd 10693	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ^*)
88		fzofzp1 13137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
89	52, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
90	49, 89	ffvelrnd 6854	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
91	90	rexrd 10693	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
92	91	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
93		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
94		ioogtlb 41777	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
95	87, 92, 93, 94	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
96	20, 56, 18, 86, 95	lelttrd 10800	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
97	90	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
98	6, 13	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐵 ∈ ℝ)
99	98	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100		iooltub 41793	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
101	87, 92, 93, 100	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
102	89, 79	eleqtrd 2917	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103		fvelrn 6846	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
104	76, 102, 103	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
105	74, 104	sseldd 3970	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106		iccleub 12795	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
107	11, 15, 105, 106	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108	107	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
109	18, 97, 99, 101, 108	ltletrd 10802	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
110	12, 16, 18, 96, 109	eliood 41780	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
111	8, 110	sseldi 3967	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112		fourierdlem76.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
113	112	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114		fourierdlem76.xre	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ)
115	114	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
116	9, 13	iccssred 41787	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117	116	sselda 3969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118	115, 117	readdcld 10672	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119	113, 118	ffvelrnd 6854	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
120	7, 111, 119	syl2anc 586	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121	120	recnd 10671	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122		fourierdlem76.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
123	122	recnd 10671	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
124	6, 123	syl 17	. . . . . . . 8 ⊢ (𝜒 → 𝐶 ∈ ℂ)
125	124	adantr 483	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126	121, 125	subcld 10999	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127		ioossre 12801	. . . . . . . . 9 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129	128	sselda 3969	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130	129	recnd 10671	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131		nne 3022	. . . . . . . . . . . 12 ⊢ (¬ 𝑠 ≠ 0 ↔ 𝑠 = 0)
132	131	biimpi 218	. . . . . . . . . . 11 ⊢ (¬ 𝑠 ≠ 0 → 𝑠 = 0)
133	132	eqcomd 2829	. . . . . . . . . 10 ⊢ (¬ 𝑠 ≠ 0 → 0 = 𝑠)
134	133	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136	135	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137	134, 136	eqeltrd 2915	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138		fourierdlem76.n0	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139	138	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140	137, 139	condan 816	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
141	7, 111, 140	syl2anc 586	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142	126, 130, 141	divcld 11418	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143		2cnd 11718	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144	130	halfcld 11885	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145	144	sincld 15485	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146	143, 145	mulcld 10663	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
147	17	recnd 10671	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148	147	adantl 484	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149	148	halfcld 11885	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150	149	sincld 15485	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151		2ne0 11744	. . . . . . . 8 ⊢ 2 ≠ 0
152	151	a1i 11	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153		fourierdlem76.ab	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
154	6, 153	syl 17	. . . . . . . . . 10 ⊢ (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155	154	adantr 483	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156	155, 111	sseldd 3970	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157		fourierdlem44 42443	. . . . . . . 8 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158	156, 141, 157	syl2anc 586	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159	143, 150, 152, 158	mulne0d 11294	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160	130, 146, 159	divcld 11418	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161		eqid 2823	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162		eqid 2823	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163	141	neneqd 3023	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164		velsn 4585	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
165	163, 164	sylnibr 331	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166	130, 165	eldifd 3949	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167		eqid 2823	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168		eqid 2823	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169		elfzofz 13056	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170	169	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171		pire 25046	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ∈ ℝ
172	171	renegcli 10949	. . . . . . . . . . . . . . . . . . . 20 ⊢ -π ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -π ∈ ℝ)
174	173, 114	readdcld 10672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
175	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → π ∈ ℝ)
176	175, 114	readdcld 10672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
177	174, 176	iccssred 41787	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178	177	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179		fourierdlem76.p	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
180		fourierdlem76.m	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℕ)
181		fourierdlem76.v	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
182	179, 180, 181	fourierdlem15 42414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183	182	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184	183, 170	ffvelrnd 6854	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185	178, 184	sseldd 3970	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
186	114	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187	185, 186	resubcld 11070	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
188	25	fvmpt2 6781	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
189	170, 187, 188	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
190	189, 187	eqeltrd 2915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
191	190	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
192	191	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
193	1, 192	sylbi 219	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ)
194		fveq2 6672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
195	194	oveq1d 7173	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
196	195	cbvmptv 5171	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
197	25, 196	eqtri 2846	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
198	197	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
199		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
200	199	oveq1d 7173	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201	200	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202		fzofzp1 13137	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203	202	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204	183, 203	ffvelrnd 6854	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205	178, 204	sseldd 3970	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206	205, 186	resubcld 11070	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207	198, 201, 203, 206	fvmptd 6777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208	207, 206	eqeltrd 2915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209	208	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210	209	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
211	1, 210	sylbi 219	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212	179	fourierdlem2 42401	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
213	180, 212	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
214	181, 213	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
215	214	simprrd 772	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
216	215	r19.21bi 3210	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
217	185, 205, 186, 216	ltsub1dd 11254	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218	217, 189, 207	3brtr4d 5100	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
219	218	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
220	219	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
221	1, 220	sylbi 219	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
222	1	biimpi 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
223	222	simplrd 768	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑖 ∈ (0..^𝑀))
224	6, 223, 185	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ)
225	224	rexrd 10693	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ^*)
226	225	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
227	6, 223, 205	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228	227	rexrd 10693	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
229	228	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
230	6, 114	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑋 ∈ ℝ)
231	230	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 12771	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233	232	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234	231, 233	readdcld 10672	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
235	6, 223, 189	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
236	235	oveq2d 7174	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) = (𝑋 + ((𝑉‘𝑖) − 𝑋)))
237	230	recnd 10671	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑋 ∈ ℂ)
238	224	recnd 10671	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℂ)
239	237, 238	pncan3d 11002	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘𝑖) − 𝑋)) = (𝑉‘𝑖))
240	236, 239	eqtr2d 2859	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
241	240	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
242	193	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
243	193	rexrd 10693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ^*)
244	243	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
245	211	rexrd 10693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
247		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
248		ioogtlb 41777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
249	244, 246, 247, 248	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
250	242, 233, 231, 249	ltadd2dd 10801	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
251	241, 250	eqbrtrd 5090	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
252	211	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253		iooltub 41793	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254	244, 246, 247, 253	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255	233, 252, 231, 254	ltadd2dd 10801	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
256	6, 223, 207	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257	256	oveq2d 7174	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258	227	recnd 10671	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259	237, 258	pncan3d 11002	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260	257, 259	eqtrd 2858	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261	260	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262	255, 261	breqtrd 5094	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263	226, 229, 234, 251, 262	eliood 41780	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
264		fvres 6691	. . . . . . . . . . . . 13 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265	263, 264	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266	265	eqcomd 2829	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267	266	mpteq2dva 5163	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268		ioosscn 41776	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270		fourierdlem76.fcn	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
271	6, 223, 270	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272		ioosscn 41776	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273	272	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274	269, 271, 273, 237, 263	fourierdlem23 42422	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275	267, 274	eqeltrd 2915	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
276	6, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
277		ioossre 12801	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278	277	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279		eqid 2823	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280		ioossre 12801	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281	280	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282	233, 254	ltned 10778	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283		fourierdlem76.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
284	6, 223, 283	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
285	260	eqcomd 2829	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286	285	oveq2d 7174	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
287	284, 286	eleqtrd 2917	. . . . . . . . . 10 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
288	211	recnd 10671	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289	276, 230, 278, 279, 263, 281, 282, 287, 288	fourierdlem53 42451	. . . . . . . . 9 ⊢ (𝜒 → 𝐿 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
290	49, 54	ffvelrnd 6854	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
291		elfzoelz 13041	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292		zre 11988	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
293	52, 291, 292	3syl 18	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑗 ∈ ℝ)
294	293	ltp1d 11572	. . . . . . . . . 10 ⊢ (𝜒 → 𝑗 < (𝑗 + 1))
295		isorel 7081	. . . . . . . . . . 11 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
296	44, 54, 89, 295	syl12anc 834	. . . . . . . . . 10 ⊢ (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
297	294, 296	mpbid 234	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
298	1	simprbi 499	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
299		eqid 2823	. . . . . . . . 9 ⊢ if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300		eqid 2823	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301	193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300	fourierdlem33 42432	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
302		eqidd 2824	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304	303	oveq2d 7174	. . . . . . . . . . 11 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305	304	fveq2d 6676	. . . . . . . . . 10 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306	243	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) ∈ ℝ^*)
307	245	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
308	90	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309	193, 211, 290, 90, 297, 298	fourierdlem10 42409	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑄‘𝑖) ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310	309	simpld 497	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
311	193, 290, 90, 310, 297	lelttrd 10800	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑆‘(𝑗 + 1)))
312	311	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < (𝑆‘(𝑗 + 1)))
313	211	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314	309	simprd 498	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315	314	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316		neqne 3026	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317	316	necomd 3073	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318	317	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319	308, 313, 315, 318	leneltd 10796	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320	306, 307, 308, 312, 319	eliood 41780	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
321	230, 90	readdcld 10672	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322	276, 321	ffvelrnd 6854	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323	322	adantr 483	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324	302, 305, 320, 323	fvmptd 6777	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325	324	ifeq2da 4500	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326	298	resmptd 5910	. . . . . . . . 9 ⊢ (𝜒 → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327	326	oveq1d 7173	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
328	301, 325, 327	3eltr3d 2929	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
329		ax-resscn 10596	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
330	128, 329	sstrdi 3981	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
331	90	recnd 10671	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332	168, 330, 124, 331	constlimc 41912	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘(𝑗 + 1))))
333	167, 168, 161, 121, 125, 328, 332	sublimc 41940	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘(𝑗 + 1))))
334	330, 162, 331	idlimc 41914	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘(𝑗 + 1))))
335	6, 105	jca 514	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336		eleq1 2902	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337	336	anbi2d 630	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338		neeq1 3080	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339	337, 338	imbi12d 347	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340	339, 140	vtoclg 3569	. . . . . . 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 41944	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘(𝑗 + 1))))
343		eqid 2823	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344	143, 150	mulcld 10663	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345	159	neneqd 3023	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346		2re 11714	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
347	346	a1i 11	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
348	17	rehalfcld 11887	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349	348	resincld 15498	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350	349	adantl 484	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351	347, 350	remulcld 10673	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352		elsng 4583	. . . . . . . . 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 327	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355	344, 354	eldifd 3949	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356		eqid 2823	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357		eqid 2823	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358		2cnd 11718	. . . . . . . 8 ⊢ (𝜒 → 2 ∈ ℂ)
359	356, 330, 358, 331	constlimc 41912	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘(𝑗 + 1))))
360	348	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361		recn 10629	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362	361	sincld 15485	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363	362	adantl 484	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364		eqid 2823	. . . . . . . . 9 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365		2cn 11715	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
366		eldifsn 4721	. . . . . . . . . . 11 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367	365, 151, 366	mpbir2an 709	. . . . . . . . . 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 41944	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘(𝑗 + 1))))
371		sinf 15479	. . . . . . . . . . . . . 14 ⊢ sin:ℂ⟶ℂ
372	371	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → sin:ℂ⟶ℂ)
373	329	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℝ ⊆ ℂ)
374	372, 373	feqresmpt 6736	. . . . . . . . . . . 12 ⊢ (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375	374	mptru 1544	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376		resincncf 42165	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377	375, 376	eqeltrri 2912	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378	377	a1i 11	. . . . . . . . 9 ⊢ (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
379	90	rehalfcld 11887	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380		fveq2 6672	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381	378, 379, 380	cnmptlimc 24490	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘(𝑗 + 1)) / 2)))
382		fveq2 6672	. . . . . . . 8 ⊢ (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383		fveq2 6672	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384	383	ad2antll 727	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385	360, 363, 370, 381, 382, 384	limcco 24493	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘(𝑗 + 1))))
386	356, 357, 343, 143, 150, 359, 385	mullimc 41904	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘(𝑗 + 1))))
387	331	halfcld 11885	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388	387	sincld 15485	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389	154, 105	sseldd 3970	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390		fourierdlem44 42443	. . . . . . . 8 ⊢ (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391	389, 341, 390	syl2anc 586	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392	358, 388, 369, 391	mulne0d 11294	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393	162, 343, 3, 148, 355, 334, 386, 392, 159	divlimc 41944	. . . . 5 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘(𝑗 + 1))))
394	2, 3, 4, 142, 160, 342, 393	mullimc 41904	. . . 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 5851	. . . . . 6 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
399		ioossicc 12825	. . . . . . . 8 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
400		iccss 12807	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
401	19, 98, 85, 107, 400	syl22anc 836	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402	399, 401	sstrid 3980	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403	402	resmptd 5910	. . . . . 6 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404	398, 403	syl5eq 2870	. . . . 5 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405	404	oveq1d 7173	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘(𝑗 + 1))))
406	394, 396, 405	3eltr4d 2930	. . 3 ⊢ (𝜒 → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
407	1, 406	sylbir 237	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
408	242, 249	gtned 10777	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
409		fourierdlem76.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
410	6, 223, 409	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
411	240	oveq2d 7174	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
412	410, 411	eleqtrd 2917	. . . . . . . . . 10 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
413	193	recnd 10671	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℂ)
414	276, 230, 278, 279, 263, 281, 408, 412, 413	fourierdlem53 42451	. . . . . . . . 9 ⊢ (𝜒 → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
415		eqid 2823	. . . . . . . . 9 ⊢ if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)))
416		eqid 2823	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
417	193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416	fourierdlem32 42431	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
418		eqidd 2824	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419		oveq2 7166	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘𝑗)))
420	419	fveq2d 6676	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑆‘𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
421	420	adantl 484	. . . . . . . . . 10 ⊢ (((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) ∧ 𝑠 = (𝑆‘𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
422	243	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ^*)
423	245	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
424	290	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ℝ)
425	193	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ)
426	310	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
427		neqne 3026	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘𝑗) = (𝑄‘𝑖) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
428	427	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
429	425, 424, 426, 428	leneltd 10796	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) < (𝑆‘𝑗))
430	90	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431	211	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432	297	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
433	314	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434	424, 430, 431, 432, 433	ltletrd 10802	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑄‘(𝑖 + 1)))
435	422, 423, 424, 429, 434	eliood 41780	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
436	230, 290	readdcld 10672	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘𝑗)) ∈ ℝ)
437	276, 436	ffvelrnd 6854	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
438	437	adantr 483	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
439	418, 421, 435, 438	fvmptd 6777	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
440	439	ifeq2da 4500	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))))
441	326	oveq1d 7173	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
442	417, 440, 441	3eltr3d 2929	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
443	290	recnd 10671	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
444	168, 330, 124, 443	constlimc 41912	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘𝑗)))
445	167, 168, 161, 121, 125, 442, 444	sublimc 41940	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘𝑗)))
446	330, 162, 443	idlimc 41914	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘𝑗)))
447	6, 83	jca 514	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
448		eleq1 2902	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
449	448	anbi2d 630	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵))))
450		neeq1 3080	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ≠ 0 ↔ (𝑆‘𝑗) ≠ 0))
451	449, 450	imbi12d 347	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0)))
452	451, 140	vtoclg 3569	. . . . . . 7 ⊢ ((𝑆‘𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0))
453	83, 447, 452	sylc 65	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ≠ 0)
454	161, 162, 2, 126, 166, 445, 446, 453, 141	divlimc 41944	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘𝑗)))
455	356, 330, 358, 443	constlimc 41912	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘𝑗)))
456	348	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457	162, 356, 364, 148, 368, 446, 455, 369, 152	divlimc 41944	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘𝑗)))
458	290	rehalfcld 11887	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℝ)
459		fveq2 6672	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆‘𝑗) / 2)))
460	378, 458, 459	cnmptlimc 24490	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘𝑗) / 2)))
461		fveq2 6672	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
462	461	ad2antll 727	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
463	456, 363, 457, 460, 382, 462	limcco 24493	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘𝑗)))
464	356, 357, 343, 143, 150, 455, 463	mullimc 41904	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘𝑗)))
465	443	halfcld 11885	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℂ)
466	465	sincld 15485	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ℂ)
467	154, 83	sseldd 3970	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (-π[,]π))
468		fourierdlem44 42443	. . . . . . . 8 ⊢ (((𝑆‘𝑗) ∈ (-π[,]π) ∧ (𝑆‘𝑗) ≠ 0) → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
469	467, 453, 468	syl2anc 586	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
470	358, 466, 369, 469	mulne0d 11294	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ≠ 0)
471	162, 343, 3, 148, 355, 446, 464, 470, 159	divlimc 41944	. . . . 5 ⊢ (𝜒 → ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘𝑗)))
472	2, 3, 4, 142, 160, 454, 471	mullimc 41904	. . . 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 7173	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘𝑗)))
476	472, 474, 475	3eltr4d 2930	. . 3 ⊢ (𝜒 → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
477	1, 476	sylbir 237	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
478	298	sselda 3969	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
479	478, 266	syldan 593	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480	479	mpteq2dva 5163	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481	225	adantr 483	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
482	228	adantr 483	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
483	230	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484	483, 129	readdcld 10672	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485	240	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
486	193	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
487	243	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
488	245	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
489	487, 488, 478, 248	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) < 𝑠)
490	486, 18, 483, 489	ltadd2dd 10801	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
491	485, 490	eqbrtrd 5090	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
492	211	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493	487, 488, 478, 253	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
494	18, 492, 483, 493	ltadd2dd 10801	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495	260	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496	494, 495	breqtrd 5094	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497	481, 482, 484, 491, 496	eliood 41780	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
498	269, 271, 330, 237, 497	fourierdlem23 42422	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499	480, 498	eqeltrd 2915	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500		ssid 3991	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
501	500	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ℂ ⊆ ℂ)
502	330, 124, 501	constcncfg 42161	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503	499, 502	subcncf 42159	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504	166	ralrimiva 3184	. . . . . . . 8 ⊢ (𝜒 → ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505		dfss3 3958	. . . . . . . 8 ⊢ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506	504, 505	sylibr 236	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507		difssd 4111	. . . . . . 7 ⊢ (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508	506, 507	idcncfg 42162	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509	503, 508	divcncf 24050	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510	330, 501	idcncfg 42162	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511	355, 343	fmptd 6880	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512	330, 358, 501	constcncfg 42161	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513		sincn 25034	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
514	513	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → sin ∈ (ℂ–cn→ℂ))
515	367	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜒 → 2 ∈ (ℂ ∖ {0}))
516	330, 515, 507	constcncfg 42161	. . . . . . . . . . 11 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517	510, 516	divcncf 24050	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518	514, 517	cncfmpt1f 23523	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519	512, 518	mulcncf 24049	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520		cncffvrn 23508	. . . . . . . 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 586	. . . . . . 7 ⊢ (𝜒 → ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522	511, 521	mpbird 259	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523	510, 522	divcncf 24050	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524	509, 523	mulcncf 24049	. . . 4 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525	404, 524	eqeltrd 2915	. . 3 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
526	1, 525	sylbir 237	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527	407, 477, 526	jca31 517	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 208 ∧ wa 398 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 {crab 3144 ∖ cdif 3935 ∪ cun 3936 ∩ cin 3937 ⊆ wss 3938 ifcif 4469 {csn 4569 {cpr 4571 class class class wbr 5068 ↦ cmpt 5148 dom cdm 5557 ran crn 5558 ↾ cres 5559 ℩cio 6314 Fun wfun 6351 ⟶wf 6353 –1-1-onto→wf1o 6356 ‘cfv 6357 Isom wiso 6358 (class class class)co 7158 ↑_m cmap 8408 Fincfn 8511 ℂcc 10537 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 · cmul 10544 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 − cmin 10872 -cneg 10873 / cdiv 11299 ℕcn 11640 2c2 11695 ℤcz 11984 (,)cioo 12741 [,)cico 12743 [,]cicc 12744 ...cfz 12895 ..^cfzo 13036 ♯chash 13693 sincsin 15419 πcpi 15422 ↾_t crest 16696 TopOpenctopn 16697 ℂ_fldccnfld 20547 –cn→ccncf 23486 lim_ℂ climc 24462

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-inf2 9106 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617 ax-addf 10618 ax-mulf 10619

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-iin 4924 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-se 5517 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-of 7411 df-om 7583 df-1st 7691 df-2nd 7692 df-supp 7833 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-pm 8411 df-ixp 8464 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fsupp 8836 df-fi 8877 df-sup 8908 df-inf 8909 df-oi 8976 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ioc 12746 df-ico 12747 df-icc 12748 df-fz 12896 df-fzo 13037 df-fl 13165 df-mod 13241 df-seq 13373 df-exp 13433 df-fac 13637 df-bc 13666 df-hash 13694 df-shft 14428 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-limsup 14830 df-clim 14847 df-rlim 14848 df-sum 15045 df-ef 15423 df-sin 15425 df-cos 15426 df-pi 15428 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-sets 16492 df-ress 16493 df-plusg 16580 df-mulr 16581 df-starv 16582 df-sca 16583 df-vsca 16584 df-ip 16585 df-tset 16586 df-ple 16587 df-ds 16589 df-unif 16590 df-hom 16591 df-cco 16592 df-rest 16698 df-topn 16699 df-0g 16717 df-gsum 16718 df-topgen 16719 df-pt 16720 df-prds 16723 df-xrs 16777 df-qtop 16782 df-imas 16783 df-xps 16785 df-mre 16859 df-mrc 16860 df-acs 16862 df-mgm 17854 df-sgrp 17903 df-mnd 17914 df-submnd 17959 df-mulg 18227 df-cntz 18449 df-cmn 18910 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-fbas 20544 df-fg 20545 df-cnfld 20548 df-top 21504 df-topon 21521 df-topsp 21543 df-bases 21556 df-cld 21629 df-ntr 21630 df-cls 21631 df-nei 21708 df-lp 21746 df-perf 21747 df-cn 21837 df-cnp 21838 df-haus 21925 df-tx 22172 df-hmeo 22365 df-fil 22456 df-fm 22548 df-flim 22549 df-flf 22550 df-xms 22932 df-ms 22933 df-tms 22934 df-cncf 23488 df-limc 24466 df-dv 24467

This theorem is referenced by: fourierdlem86 42484

W3C validator