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 46163

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 2729	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3		eqid 2729	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4		eqid 2729	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5		simplll 774	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
6	1, 5	sylbi 217	. . . . . . . . . 10 ⊢ (𝜒 → 𝜑)
7	6	adantr 480	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8		ioossicc 13336	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9		fourierdlem76.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
10	9	rexrd 11165	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
11	6, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
12	11	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ^*)
13		fourierdlem76.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	13	rexrd 11165	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
15	6, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ^*)
17		elioore 13278	. . . . . . . . . . . 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 9213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝐴, 𝐵} ∈ Fin
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin)
24		fzfid 13880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
25		fourierdlem76.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
26	25	rnmptfi 45149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27		infi 9159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
28	24, 26, 27	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29		unfi 9085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
30	23, 28, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
31	21, 30	eqeltrid 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ Fin)
32		prssg 4770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
33	9, 13, 32	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
34	9, 13, 33	mpbi2and 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35		inss2 4189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossre 13310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴(,)𝐵) ⊆ ℝ
37	35, 36	sstri 3945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
39	34, 38	unssd 4143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
40	21, 39	eqsstrid 3974	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
41		fourierdlem76.s	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42		fourierdlem76.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘𝑇) − 1)
43	31, 40, 41, 42	fourierdlem36 46124	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44	6, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
45		isof1o 7260	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
46		f1of 6764	. . . . . . . . . . . . . . . 16 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
47	44, 45, 46	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶𝑇)
48	6, 40	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑇 ⊆ ℝ)
49	47, 48	fssd 6669	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
52	1, 51	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (0..^𝑁))
53		elfzofz 13578	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
54	52, 53	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑗 ∈ (0...𝑁))
55	54	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
56	50, 55	ffvelcdmd 7019	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ)
57	43, 45, 46	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
58		frn 6659	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆 ⊆ 𝑇)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝑆 ⊆ 𝑇)
60	9	leidd 11686	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
61		fourierdlem76.altb	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 < 𝐵)
62	9, 13, 61	ltled 11264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63	9, 13, 9, 60, 62	eliccd 45485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
64	13	leidd 11686	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
65	9, 13, 13, 62, 64	eliccd 45485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
66		prssg 4770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
67	9, 13, 66	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
68	63, 65, 67	mpbi2and 712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
69	35, 8	sstri 3945	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
71	68, 70	unssd 4143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
72	21, 71	eqsstrid 3974	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
73	59, 72	sstrd 3946	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
74	6, 73	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75		ffun 6655	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
76	49, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → Fun 𝑆)
77		fdm 6661	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
78	49, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom 𝑆 = (0...𝑁))
79	78	eqcomd 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (0...𝑁) = dom 𝑆)
80	54, 79	eleqtrd 2830	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ dom 𝑆)
81		fvelrn 7010	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆) → (𝑆‘𝑗) ∈ ran 𝑆)
82	76, 80, 81	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ran 𝑆)
83	74, 82	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
84		iccgelb 13305	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝑗))
85	11, 15, 83, 84	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ≤ (𝑆‘𝑗))
86	85	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆‘𝑗))
87	56	rexrd 11165	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ^*)
88		fzofzp1 13667	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
89	52, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
90	49, 89	ffvelcdmd 7019	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
91	90	rexrd 11165	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
92	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
93		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
94		ioogtlb 45476	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
95	87, 92, 93, 94	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
96	20, 56, 18, 86, 95	lelttrd 11274	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
97	90	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
98	6, 13	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐵 ∈ ℝ)
99	98	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100		iooltub 45491	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
101	87, 92, 93, 100	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
102	89, 79	eleqtrd 2830	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103		fvelrn 7010	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
104	76, 102, 103	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
105	74, 104	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106		iccleub 13304	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
107	11, 15, 105, 106	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108	107	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
109	18, 97, 99, 101, 108	ltletrd 11276	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
110	12, 16, 18, 96, 109	eliood 45479	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
111	8, 110	sselid 3933	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112		fourierdlem76.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
113	112	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114		fourierdlem76.xre	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ)
115	114	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
116	9, 13	iccssred 13337	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117	116	sselda 3935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118	115, 117	readdcld 11144	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119	113, 118	ffvelcdmd 7019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
120	7, 111, 119	syl2anc 584	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121	120	recnd 11143	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122		fourierdlem76.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
123	122	recnd 11143	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
124	6, 123	syl 17	. . . . . . . 8 ⊢ (𝜒 → 𝐶 ∈ ℂ)
125	124	adantr 480	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126	121, 125	subcld 11475	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127		ioossre 13310	. . . . . . . . 9 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129	128	sselda 3935	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130	129	recnd 11143	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131		nne 2929	. . . . . . . . . . . 12 ⊢ (¬ 𝑠 ≠ 0 ↔ 𝑠 = 0)
132	131	biimpi 216	. . . . . . . . . . 11 ⊢ (¬ 𝑠 ≠ 0 → 𝑠 = 0)
133	132	eqcomd 2735	. . . . . . . . . 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 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140	137, 139	condan 817	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
141	7, 111, 140	syl2anc 584	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142	126, 130, 141	divcld 11900	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143		2cnd 12206	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144	130	halfcld 12369	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145	144	sincld 16039	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146	143, 145	mulcld 11135	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
147	17	recnd 11143	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148	147	adantl 481	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149	148	halfcld 12369	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150	149	sincld 16039	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151		2ne0 12232	. . . . . . . 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 3936	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157		fourierdlem44 46132	. . . . . . . 8 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158	156, 141, 157	syl2anc 584	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159	143, 150, 152, 158	mulne0d 11772	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160	130, 146, 159	divcld 11900	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161		eqid 2729	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162		eqid 2729	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163	141	neneqd 2930	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164		velsn 4593	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
165	163, 164	sylnibr 329	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166	130, 165	eldifd 3914	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167		eqid 2729	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168		eqid 2729	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169		elfzofz 13578	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170	169	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171		pire 26364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ∈ ℝ
172	171	renegcli 11425	. . . . . . . . . . . . . . . . . . . 20 ⊢ -π ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -π ∈ ℝ)
174	173, 114	readdcld 11144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
175	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → π ∈ ℝ)
176	175, 114	readdcld 11144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
177	174, 176	iccssred 13337	. . . . . . . . . . . . . . . . 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 46103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183	182	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184	183, 170	ffvelcdmd 7019	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185	178, 184	sseldd 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
186	114	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187	185, 186	resubcld 11548	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
188	25	fvmpt2 6941	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
189	170, 187, 188	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
190	189, 187	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
191	190	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
192	191	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
193	1, 192	sylbi 217	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ)
194		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
195	194	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
196	195	cbvmptv 5196	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
197	25, 196	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
198	197	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
199		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
200	199	oveq1d 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201	200	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202		fzofzp1 13667	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203	202	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204	183, 203	ffvelcdmd 7019	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205	178, 204	sseldd 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206	205, 186	resubcld 11548	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207	198, 201, 203, 206	fvmptd 6937	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208	207, 206	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209	208	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
211	1, 210	sylbi 217	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212	179	fourierdlem2 46090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
213	180, 212	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
214	181, 213	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
215	214	simprrd 773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
216	215	r19.21bi 3221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
217	185, 205, 186, 216	ltsub1dd 11732	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218	217, 189, 207	3brtr4d 5124	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
219	218	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
220	219	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
221	1, 220	sylbi 217	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
222	1	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
223	222	simplrd 769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑖 ∈ (0..^𝑀))
224	6, 223, 185	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ)
225	224	rexrd 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ^*)
226	225	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
227	6, 223, 205	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228	227	rexrd 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
229	228	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
230	6, 114	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑋 ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13278	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233	232	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234	231, 233	readdcld 11144	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
235	6, 223, 189	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
236	235	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) = (𝑋 + ((𝑉‘𝑖) − 𝑋)))
237	230	recnd 11143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑋 ∈ ℂ)
238	224	recnd 11143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℂ)
239	237, 238	pncan3d 11478	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘𝑖) − 𝑋)) = (𝑉‘𝑖))
240	236, 239	eqtr2d 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
241	240	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
242	193	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
243	193	rexrd 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ^*)
244	243	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
245	211	rexrd 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
247		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
248		ioogtlb 45476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
249	244, 246, 247, 248	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
250	242, 233, 231, 249	ltadd2dd 11275	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
251	241, 250	eqbrtrd 5114	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
252	211	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253		iooltub 45491	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254	244, 246, 247, 253	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255	233, 252, 231, 254	ltadd2dd 11275	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
256	6, 223, 207	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257	256	oveq2d 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258	227	recnd 11143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259	237, 258	pncan3d 11478	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260	257, 259	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261	260	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262	255, 261	breqtrd 5118	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263	226, 229, 234, 251, 262	eliood 45479	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
264		fvres 6841	. . . . . . . . . . . . 13 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265	263, 264	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266	265	eqcomd 2735	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267	266	mpteq2dva 5185	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268		ioosscn 13311	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270		fourierdlem76.fcn	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
271	6, 223, 270	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272		ioosscn 13311	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273	272	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274	269, 271, 273, 237, 263	fourierdlem23 46111	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275	267, 274	eqeltrd 2828	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
276	6, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
277		ioossre 13310	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278	277	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279		eqid 2729	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280		ioossre 13310	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281	280	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282	233, 254	ltned 11252	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283		fourierdlem76.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
284	6, 223, 283	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
285	260	eqcomd 2735	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286	285	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
287	284, 286	eleqtrd 2830	. . . . . . . . . 10 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
288	211	recnd 11143	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289	276, 230, 278, 279, 263, 281, 282, 287, 288	fourierdlem53 46140	. . . . . . . . 9 ⊢ (𝜒 → 𝐿 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
290	49, 54	ffvelcdmd 7019	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
291		elfzoelz 13562	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292		zre 12475	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
293	52, 291, 292	3syl 18	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑗 ∈ ℝ)
294	293	ltp1d 12055	. . . . . . . . . 10 ⊢ (𝜒 → 𝑗 < (𝑗 + 1))
295		isorel 7263	. . . . . . . . . . 11 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
296	44, 54, 89, 295	syl12anc 836	. . . . . . . . . 10 ⊢ (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
297	294, 296	mpbid 232	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
298	1	simprbi 496	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
299		eqid 2729	. . . . . . . . 9 ⊢ if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300		eqid 2729	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301	193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300	fourierdlem33 46121	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
302		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304	303	oveq2d 7365	. . . . . . . . . . 11 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305	304	fveq2d 6826	. . . . . . . . . 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 46098	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑄‘𝑖) ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310	309	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
311	193, 290, 90, 310, 297	lelttrd 11274	. . . . . . . . . . . 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 2933	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317	316	necomd 2980	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318	317	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319	308, 313, 315, 318	leneltd 11270	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320	306, 307, 308, 312, 319	eliood 45479	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
321	230, 90	readdcld 11144	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322	276, 321	ffvelcdmd 7019	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323	322	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324	302, 305, 320, 323	fvmptd 6937	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325	324	ifeq2da 4509	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326	298	resmptd 5991	. . . . . . . . 9 ⊢ (𝜒 → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327	326	oveq1d 7364	. . . . . . . 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 11066	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
330	128, 329	sstrdi 3948	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
331	90	recnd 11143	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332	168, 330, 124, 331	constlimc 45605	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘(𝑗 + 1))))
333	167, 168, 161, 121, 125, 328, 332	sublimc 45633	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘(𝑗 + 1))))
334	330, 162, 331	idlimc 45607	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘(𝑗 + 1))))
335	6, 105	jca 511	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336		eleq1 2816	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337	336	anbi2d 630	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338		neeq1 2987	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339	337, 338	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340	339, 140	vtoclg 3509	. . . . . . 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 45637	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘(𝑗 + 1))))
343		eqid 2729	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344	143, 150	mulcld 11135	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345	159	neneqd 2930	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346		2re 12202	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
347	346	a1i 11	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
348	17	rehalfcld 12371	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349	348	resincld 16052	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350	349	adantl 481	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351	347, 350	remulcld 11145	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352		elsng 4591	. . . . . . . . 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 3914	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356		eqid 2729	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357		eqid 2729	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358		2cnd 12206	. . . . . . . 8 ⊢ (𝜒 → 2 ∈ ℂ)
359	356, 330, 358, 331	constlimc 45605	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘(𝑗 + 1))))
360	348	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361		recn 11099	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362	361	sincld 16039	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363	362	adantl 481	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364		eqid 2729	. . . . . . . . 9 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365		2cn 12203	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
366		eldifsn 4737	. . . . . . . . . . 11 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367	365, 151, 366	mpbir2an 711	. . . . . . . . . 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 45637	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘(𝑗 + 1))))
371		sinf 16033	. . . . . . . . . . . . . 14 ⊢ sin:ℂ⟶ℂ
372	371	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → sin:ℂ⟶ℂ)
373	329	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℝ ⊆ ℂ)
374	372, 373	feqresmpt 6892	. . . . . . . . . . . 12 ⊢ (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375	374	mptru 1547	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376		resincncf 45856	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377	375, 376	eqeltrri 2825	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378	377	a1i 11	. . . . . . . . 9 ⊢ (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
379	90	rehalfcld 12371	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381	378, 379, 380	cnmptlimc 25789	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘(𝑗 + 1)) / 2)))
382		fveq2 6822	. . . . . . . 8 ⊢ (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383		fveq2 6822	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384	383	ad2antll 729	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385	360, 363, 370, 381, 382, 384	limcco 25792	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘(𝑗 + 1))))
386	356, 357, 343, 143, 150, 359, 385	mullimc 45597	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘(𝑗 + 1))))
387	331	halfcld 12369	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388	387	sincld 16039	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389	154, 105	sseldd 3936	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390		fourierdlem44 46132	. . . . . . . 8 ⊢ (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391	389, 341, 390	syl2anc 584	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392	358, 388, 369, 391	mulne0d 11772	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393	162, 343, 3, 148, 355, 334, 386, 392, 159	divlimc 45637	. . . . 5 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘(𝑗 + 1))))
394	2, 3, 4, 142, 160, 342, 393	mullimc 45597	. . . 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 5926	. . . . . 6 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
399		ioossicc 13336	. . . . . . . 8 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
400		iccss 13317	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
401	19, 98, 85, 107, 400	syl22anc 838	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402	399, 401	sstrid 3947	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403	402	resmptd 5991	. . . . . 6 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404	398, 403	eqtrid 2776	. . . . 5 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405	404	oveq1d 7364	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘(𝑗 + 1))))
406	394, 396, 405	3eltr4d 2843	. . 3 ⊢ (𝜒 → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
407	1, 406	sylbir 235	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
408	242, 249	gtned 11251	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
409		fourierdlem76.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
410	6, 223, 409	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
411	240	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
412	410, 411	eleqtrd 2830	. . . . . . . . . 10 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
413	193	recnd 11143	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℂ)
414	276, 230, 278, 279, 263, 281, 408, 412, 413	fourierdlem53 46140	. . . . . . . . 9 ⊢ (𝜒 → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
415		eqid 2729	. . . . . . . . 9 ⊢ if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)))
416		eqid 2729	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
417	193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416	fourierdlem32 46120	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
418		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419		oveq2 7357	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘𝑗)))
420	419	fveq2d 6826	. . . . . . . . . . 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 2933	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘𝑗) = (𝑄‘𝑖) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
428	427	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
429	425, 424, 426, 428	leneltd 11270	. . . . . . . . . . 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 11276	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑄‘(𝑖 + 1)))
435	422, 423, 424, 429, 434	eliood 45479	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
436	230, 290	readdcld 11144	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘𝑗)) ∈ ℝ)
437	276, 436	ffvelcdmd 7019	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
438	437	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
439	418, 421, 435, 438	fvmptd 6937	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
440	439	ifeq2da 4509	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))))
441	326	oveq1d 7364	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
442	417, 440, 441	3eltr3d 2842	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
443	290	recnd 11143	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
444	168, 330, 124, 443	constlimc 45605	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘𝑗)))
445	167, 168, 161, 121, 125, 442, 444	sublimc 45633	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘𝑗)))
446	330, 162, 443	idlimc 45607	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘𝑗)))
447	6, 83	jca 511	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
448		eleq1 2816	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
449	448	anbi2d 630	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵))))
450		neeq1 2987	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ≠ 0 ↔ (𝑆‘𝑗) ≠ 0))
451	449, 450	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0)))
452	451, 140	vtoclg 3509	. . . . . . 7 ⊢ ((𝑆‘𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0))
453	83, 447, 452	sylc 65	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ≠ 0)
454	161, 162, 2, 126, 166, 445, 446, 453, 141	divlimc 45637	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘𝑗)))
455	356, 330, 358, 443	constlimc 45605	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘𝑗)))
456	348	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457	162, 356, 364, 148, 368, 446, 455, 369, 152	divlimc 45637	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘𝑗)))
458	290	rehalfcld 12371	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℝ)
459		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆‘𝑗) / 2)))
460	378, 458, 459	cnmptlimc 25789	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘𝑗) / 2)))
461		fveq2 6822	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
462	461	ad2antll 729	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
463	456, 363, 457, 460, 382, 462	limcco 25792	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘𝑗)))
464	356, 357, 343, 143, 150, 455, 463	mullimc 45597	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘𝑗)))
465	443	halfcld 12369	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℂ)
466	465	sincld 16039	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ℂ)
467	154, 83	sseldd 3936	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (-π[,]π))
468		fourierdlem44 46132	. . . . . . . 8 ⊢ (((𝑆‘𝑗) ∈ (-π[,]π) ∧ (𝑆‘𝑗) ≠ 0) → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
469	467, 453, 468	syl2anc 584	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
470	358, 466, 369, 469	mulne0d 11772	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ≠ 0)
471	162, 343, 3, 148, 355, 446, 464, 470, 159	divlimc 45637	. . . . 5 ⊢ (𝜒 → ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘𝑗)))
472	2, 3, 4, 142, 160, 454, 471	mullimc 45597	. . . 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 7364	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘𝑗)))
476	472, 474, 475	3eltr4d 2843	. . 3 ⊢ (𝜒 → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
477	1, 476	sylbir 235	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
478	298	sselda 3935	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
479	478, 266	syldan 591	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480	479	mpteq2dva 5185	. . . . . . . 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 11144	. . . . . . . . . 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 1373	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) < 𝑠)
490	486, 18, 483, 489	ltadd2dd 11275	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
491	485, 490	eqbrtrd 5114	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
492	211	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493	487, 488, 478, 253	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
494	18, 492, 483, 493	ltadd2dd 11275	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495	260	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496	494, 495	breqtrd 5118	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497	481, 482, 484, 491, 496	eliood 45479	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
498	269, 271, 330, 237, 497	fourierdlem23 46111	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499	480, 498	eqeltrd 2828	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500		ssid 3958	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
501	500	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ℂ ⊆ ℂ)
502	330, 124, 501	constcncfg 45853	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503	499, 502	subcncf 25343	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504	166	ralrimiva 3121	. . . . . . . 8 ⊢ (𝜒 → ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505		dfss3 3924	. . . . . . . 8 ⊢ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506	504, 505	sylibr 234	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507		difssd 4088	. . . . . . 7 ⊢ (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508	506, 507	idcncfg 45854	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509	503, 508	divcncf 25346	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510	330, 501	idcncfg 45854	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511	355, 343	fmptd 7048	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512	330, 358, 501	constcncfg 45853	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513		sincn 26352	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
514	513	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → sin ∈ (ℂ–cn→ℂ))
515	367	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜒 → 2 ∈ (ℂ ∖ {0}))
516	330, 515, 507	constcncfg 45853	. . . . . . . . . . 11 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517	510, 516	divcncf 25346	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518	514, 517	cncfmpt1f 24805	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519	512, 518	mulcncf 25344	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520		cncfcdm 24789	. . . . . . . 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 584	. . . . . . 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 25346	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524	509, 523	mulcncf 25344	. . . 4 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525	404, 524	eqeltrd 2828	. . 3 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
526	1, 525	sylbir 235	. 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 206 ∧ wa 395 = wceq 1540 ⊤wtru 1541 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 {crab 3394 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ifcif 4476 {csn 4577 {cpr 4579 class class class wbr 5092 ↦ cmpt 5173 dom cdm 5619 ran crn 5620 ↾ cres 5621 ℩cio 6436 Fun wfun 6476 ⟶wf 6478 –1-1-onto→wf1o 6481 ‘cfv 6482 Isom wiso 6483 (class class class)co 7349 ↑_m cmap 8753 Fincfn 8872 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 ℝ^*cxr 11148 < clt 11149 ≤ cle 11150 − cmin 11347 -cneg 11348 / cdiv 11777 ℕcn 12128 2c2 12183 ℤcz 12471 (,)cioo 13248 [,)cico 13250 [,]cicc 13251 ...cfz 13410 ..^cfzo 13557 ♯chash 14237 sincsin 15970 πcpi 15973 ↾_t crest 17324 TopOpenctopn 17325 ℂ_fldccnfld 21261 –cn→ccncf 24767 lim_ℂ climc 25761

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-ioo 13252 df-ioc 13253 df-ico 13254 df-icc 13255 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-shft 14974 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-sum 15594 df-ef 15974 df-sin 15976 df-cos 15977 df-pi 15979 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-submnd 18658 df-mulg 18947 df-cntz 19196 df-cmn 19661 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-fbas 21258 df-fg 21259 df-cnfld 21262 df-top 22779 df-topon 22796 df-topsp 22818 df-bases 22831 df-cld 22904 df-ntr 22905 df-cls 22906 df-nei 22983 df-lp 23021 df-perf 23022 df-cn 23112 df-cnp 23113 df-haus 23200 df-tx 23447 df-hmeo 23640 df-fil 23731 df-fm 23823 df-flim 23824 df-flf 23825 df-xms 24206 df-ms 24207 df-tms 24208 df-cncf 24769 df-limc 25765 df-dv 25766

This theorem is referenced by: fourierdlem86 46173

W3C validator