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 47161

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 2761	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3		eqid 2761	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4		eqid 2761	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5		simplll 787	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
6	1, 5	sylbi 220	. . . . . . . . . 10 ⊢ (𝜒 → 𝜑)
7	6	adantr 486	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8		ioossicc 13557	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9		fourierdlem76.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
10	9	rexrd 11352	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
11	6, 10	syl 18	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
12	11	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ^*)
13		fourierdlem76.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	13	rexrd 11352	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
15	6, 14	syl 18	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
16	15	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ^*)
17		elioore 13499	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℝ)
18	17	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
19	6, 9	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ∈ ℝ)
20	19	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ)
21		fourierdlem76.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
22		prfi 9308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝐴, 𝐵} ∈ Fin
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin)
24		fzfid 14109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
25		fourierdlem76.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
26	25	rnmptfi 46155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27		infi 9254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
28	24, 26, 27	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29		unfi 9179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
30	23, 28, 29	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
31	21, 30	eqeltrid 2865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ Fin)
32		prssg 4780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
33	9, 13, 32	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
34	9, 13, 33	mpbi2and 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35		inss2 4183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossre 13531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴(,)𝐵) ⊆ ℝ
37	35, 36	sstri 3940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
39	34, 38	unssd 4138	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
40	21, 39	eqsstrid 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
41		fourierdlem76.s	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42		fourierdlem76.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘𝑇) − 1)
43	31, 40, 41, 42	fourierdlem36 47122	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44	6, 43	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
45		isof1o 7329	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
46		f1of 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
47	44, 45, 46	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶𝑇)
48	6, 40	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑇 ⊆ ℝ)
49	47, 48	fssd 6725	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
52	1, 51	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (0..^𝑁))
53		elfzofz 13803	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
54	52, 53	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑗 ∈ (0...𝑁))
55	54	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
56	50, 55	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ)
57	43, 45, 46	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
58		frn 6715	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆 ⊆ 𝑇)
59	57, 58	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝑆 ⊆ 𝑇)
60	9	leidd 11875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
61		fourierdlem76.altb	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 < 𝐵)
62	9, 13, 61	ltled 11451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63	9, 13, 9, 60, 62	eliccd 46485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
64	13	leidd 11875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
65	9, 13, 13, 62, 64	eliccd 46485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
66		prssg 4780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
67	9, 13, 66	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
68	63, 65, 67	mpbi2and 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
69	35, 8	sstri 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
71	68, 70	unssd 4138	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
72	21, 71	eqsstrid 3969	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
73	59, 72	sstrd 3941	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
74	6, 73	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75		ffun 6710	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
76	49, 75	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → Fun 𝑆)
77		fdm 6717	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
78	49, 77	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom 𝑆 = (0...𝑁))
79	78	eqcomd 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (0...𝑁) = dom 𝑆)
80	54, 79	eleqtrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ dom 𝑆)
81		fvelrn 7074	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆) → (𝑆‘𝑗) ∈ ran 𝑆)
82	76, 80, 81	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ran 𝑆)
83	74, 82	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
84		iccgelb 13526	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝑗))
85	11, 15, 83, 84	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ≤ (𝑆‘𝑗))
86	85	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆‘𝑗))
87	56	rexrd 11352	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ^*)
88		fzofzp1 13892	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
89	52, 88	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
90	49, 89	ffvelcdmd 7083	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
91	90	rexrd 11352	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
92	91	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
93		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
94		ioogtlb 46476	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
95	87, 92, 93, 94	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
96	20, 56, 18, 86, 95	lelttrd 11461	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
97	90	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
98	6, 13	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐵 ∈ ℝ)
99	98	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100		iooltub 46491	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
101	87, 92, 93, 100	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
102	89, 79	eleqtrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103		fvelrn 7074	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
104	76, 102, 103	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
105	74, 104	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106		iccleub 13525	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
107	11, 15, 105, 106	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108	107	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
109	18, 97, 99, 101, 108	ltletrd 11463	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
110	12, 16, 18, 96, 109	eliood 46479	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
111	8, 110	sselid 3929	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112		fourierdlem76.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
113	112	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114		fourierdlem76.xre	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ)
115	114	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
116	9, 13	iccssred 13558	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117	116	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118	115, 117	readdcld 11331	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119	113, 118	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
120	7, 111, 119	syl2anc 596	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121	120	recnd 11330	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122		fourierdlem76.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
123	122	recnd 11330	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
124	6, 123	syl 18	. . . . . . . 8 ⊢ (𝜒 → 𝐶 ∈ ℂ)
125	124	adantr 486	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126	121, 125	subcld 11662	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127		ioossre 13531	. . . . . . . . 9 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129	128	sselda 3931	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130	129	recnd 11330	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131		nne 2960	. . . . . . . . . . . 12 ⊢ (¬ 𝑠 ≠ 0 ↔ 𝑠 = 0)
132	131	biimpi 219	. . . . . . . . . . 11 ⊢ (¬ 𝑠 ≠ 0 → 𝑠 = 0)
133	132	eqcomd 2767	. . . . . . . . . 10 ⊢ (¬ 𝑠 ≠ 0 → 0 = 𝑠)
134	133	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136	135	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137	134, 136	eqeltrd 2861	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138		fourierdlem76.n0	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139	138	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140	137, 139	condan 830	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
141	7, 111, 140	syl2anc 596	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142	126, 130, 141	divcld 12086	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143		2cnd 12414	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144	130	halfcld 12584	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145	144	sincld 16291	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146	143, 145	mulcld 11322	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
147	17	recnd 11330	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148	147	adantl 487	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149	148	halfcld 12584	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150	149	sincld 16291	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151		2ne0 12442	. . . . . . . 8 ⊢ 2 ≠ 0
152	151	a1i 11	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ≠ 0)
153		fourierdlem76.ab	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
154	6, 153	syl 18	. . . . . . . . . 10 ⊢ (𝜒 → (𝐴[,]𝐵) ⊆ (-π[,]π))
155	154	adantr 486	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐴[,]𝐵) ⊆ (-π[,]π))
156	155, 111	sseldd 3932	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157		fourierdlem44 47130	. . . . . . . 8 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158	156, 141, 157	syl2anc 596	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159	143, 150, 152, 158	mulne0d 11961	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160	130, 146, 159	divcld 12086	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161		eqid 2761	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162		eqid 2761	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163	141	neneqd 2961	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164		velsn 4600	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
165	163, 164	sylnibr 332	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166	130, 165	eldifd 3910	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167		eqid 2761	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168		eqid 2761	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169		elfzofz 13803	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170	169	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171		pire 26776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ∈ ℝ
172	171	renegcli 11612	. . . . . . . . . . . . . . . . . . . 20 ⊢ -π ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -π ∈ ℝ)
174	173, 114	readdcld 11331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
175	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → π ∈ ℝ)
176	175, 114	readdcld 11331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
177	174, 176	iccssred 13558	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
178	177	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
179		fourierdlem76.p	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
180		fourierdlem76.m	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℕ)
181		fourierdlem76.v	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
182	179, 180, 181	fourierdlem15 47101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183	182	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184	183, 170	ffvelcdmd 7083	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185	178, 184	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
186	114	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187	185, 186	resubcld 11737	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
188	25	fvmpt2 7003	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
189	170, 187, 188	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
190	189, 187	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
191	190	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
192	191	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
193	1, 192	sylbi 220	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ)
194		fveq2 6883	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
195	194	oveq1d 7433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
196	195	cbvmptv 5209	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
197	25, 196	eqtri 2784	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
198	197	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
199		fveq2 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
200	199	oveq1d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201	200	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202		fzofzp1 13892	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203	202	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204	183, 203	ffvelcdmd 7083	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205	178, 204	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206	205, 186	resubcld 11737	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207	198, 201, 203, 206	fvmptd 6999	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208	207, 206	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209	208	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210	209	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
211	1, 210	sylbi 220	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212	179	fourierdlem2 47088	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
213	180, 212	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
214	181, 213	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
215	214	simprrd 786	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
216	215	r19.21bi 3255	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
217	185, 205, 186, 216	ltsub1dd 11921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218	217, 189, 207	3brtr4d 5137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
219	218	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
220	219	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
221	1, 220	sylbi 220	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
222	1	biimpi 219	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
223	222	simplrd 782	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑖 ∈ (0..^𝑀))
224	6, 223, 185	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ)
225	224	rexrd 11352	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ^*)
226	225	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
227	6, 223, 205	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228	227	rexrd 11352	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
229	228	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
230	6, 114	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑋 ∈ ℝ)
231	230	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13499	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233	232	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234	231, 233	readdcld 11331	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
235	6, 223, 189	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
236	235	oveq2d 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) = (𝑋 + ((𝑉‘𝑖) − 𝑋)))
237	230	recnd 11330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑋 ∈ ℂ)
238	224	recnd 11330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℂ)
239	237, 238	pncan3d 11665	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘𝑖) − 𝑋)) = (𝑉‘𝑖))
240	236, 239	eqtr2d 2797	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
241	240	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
242	193	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
243	193	rexrd 11352	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ^*)
244	243	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
245	211	rexrd 11352	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
247		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
248		ioogtlb 46476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
249	244, 246, 247, 248	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
250	242, 233, 231, 249	ltadd2dd 11462	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
251	241, 250	eqbrtrd 5127	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
252	211	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253		iooltub 46491	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254	244, 246, 247, 253	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255	233, 252, 231, 254	ltadd2dd 11462	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
256	6, 223, 207	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257	256	oveq2d 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258	227	recnd 11330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259	237, 258	pncan3d 11665	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260	257, 259	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261	260	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262	255, 261	breqtrd 5131	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263	226, 229, 234, 251, 262	eliood 46479	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
264		fvres 6902	. . . . . . . . . . . . 13 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265	263, 264	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266	265	eqcomd 2767	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267	266	mpteq2dva 5198	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268		ioosscn 13532	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270		fourierdlem76.fcn	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
271	6, 223, 270	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272		ioosscn 13532	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273	272	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274	269, 271, 273, 237, 263	fourierdlem23 47109	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275	267, 274	eqeltrd 2861	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
276	6, 112	syl 18	. . . . . . . . . 10 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
277		ioossre 13531	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278	277	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279		eqid 2761	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280		ioossre 13531	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281	280	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282	233, 254	ltned 11439	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283		fourierdlem76.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
284	6, 223, 283	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
285	260	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286	285	oveq2d 7434	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
287	284, 286	eleqtrd 2863	. . . . . . . . . 10 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
288	211	recnd 11330	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289	276, 230, 278, 279, 263, 281, 282, 287, 288	fourierdlem53 47138	. . . . . . . . 9 ⊢ (𝜒 → 𝐿 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
290	49, 54	ffvelcdmd 7083	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
291		elfzoelz 13786	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292		zre 12690	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
293	52, 291, 292	3syl 19	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑗 ∈ ℝ)
294	293	ltp1d 12240	. . . . . . . . . 10 ⊢ (𝜒 → 𝑗 < (𝑗 + 1))
295		isorel 7332	. . . . . . . . . . 11 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
296	44, 54, 89, 295	syl12anc 850	. . . . . . . . . 10 ⊢ (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
297	294, 296	mpbid 235	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
298	1	simprbi 503	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
299		eqid 2761	. . . . . . . . 9 ⊢ if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300		eqid 2761	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301	193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300	fourierdlem33 47119	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
302		eqidd 2762	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304	303	oveq2d 7434	. . . . . . . . . . 11 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305	304	fveq2d 6887	. . . . . . . . . 10 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
306	243	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) ∈ ℝ^*)
307	245	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
308	90	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
309	193, 211, 290, 90, 297, 298	fourierdlem10 47096	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑄‘𝑖) ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310	309	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
311	193, 290, 90, 310, 297	lelttrd 11461	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑆‘(𝑗 + 1)))
312	311	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < (𝑆‘(𝑗 + 1)))
313	211	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
314	309	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
315	314	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
316		neqne 2964	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317	316	necomd 3011	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318	317	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319	308, 313, 315, 318	leneltd 11457	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320	306, 307, 308, 312, 319	eliood 46479	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
321	230, 90	readdcld 11331	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322	276, 321	ffvelcdmd 7083	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323	322	adantr 486	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324	302, 305, 320, 323	fvmptd 6999	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325	324	ifeq2da 4515	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326	298	resmptd 6032	. . . . . . . . 9 ⊢ (𝜒 → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327	326	oveq1d 7433	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
328	301, 325, 327	3eltr3d 2875	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
329		ax-resscn 11250	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
330	128, 329	sstrdi 3943	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
331	90	recnd 11330	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332	168, 330, 124, 331	constlimc 46605	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘(𝑗 + 1))))
333	167, 168, 161, 121, 125, 328, 332	sublimc 46631	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘(𝑗 + 1))))
334	330, 162, 331	idlimc 46607	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘(𝑗 + 1))))
335	6, 105	jca 521	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337	336	anbi2d 642	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338		neeq1 3018	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339	337, 338	imbi12d 347	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340	339, 140	vtoclg 3518	. . . . . . 7 ⊢ ((𝑆‘(𝑗 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0))
341	90, 335, 340	sylc 66	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≠ 0)
342	161, 162, 2, 126, 166, 333, 334, 341, 141	divlimc 46635	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘(𝑗 + 1))))
343		eqid 2761	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344	143, 150	mulcld 11322	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345	159	neneqd 2961	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346		2re 12410	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
347	346	a1i 11	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
348	17	rehalfcld 12586	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349	348	resincld 16304	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350	349	adantl 487	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351	347, 350	remulcld 11332	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352		elsng 4598	. . . . . . . . 9 ⊢ ((2 · (sin‘(𝑠 / 2))) ∈ ℝ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
353	351, 352	syl 18	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
354	345, 353	mtbird 328	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355	344, 354	eldifd 3910	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356		eqid 2761	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357		eqid 2761	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358		2cnd 12414	. . . . . . . 8 ⊢ (𝜒 → 2 ∈ ℂ)
359	356, 330, 358, 331	constlimc 46605	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘(𝑗 + 1))))
360	348	ad2antrl 741	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361		recn 11283	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362	361	sincld 16291	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363	362	adantl 487	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364		eqid 2761	. . . . . . . . 9 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365		2cn 12411	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
366		eldifsn 4748	. . . . . . . . . . 11 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367	365, 151, 366	mpbir2an 724	. . . . . . . . . 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 46635	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘(𝑗 + 1))))
371		sinf 16285	. . . . . . . . . . . . . 14 ⊢ sin:ℂ⟶ℂ
372	371	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → sin:ℂ⟶ℂ)
373	329	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℝ ⊆ ℂ)
374	372, 373	feqresmpt 6952	. . . . . . . . . . . 12 ⊢ (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375	374	mptru 1577	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376		resincncf 46854	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377	375, 376	eqeltrri 2858	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378	377	a1i 11	. . . . . . . . 9 ⊢ (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
379	90	rehalfcld 12586	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380		fveq2 6883	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381	378, 379, 380	cnmptlimc 26203	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘(𝑗 + 1)) / 2)))
382		fveq2 6883	. . . . . . . 8 ⊢ (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383		fveq2 6883	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384	383	ad2antll 742	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385	360, 363, 370, 381, 382, 384	limcco 26206	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘(𝑗 + 1))))
386	356, 357, 343, 143, 150, 359, 385	mullimc 46597	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘(𝑗 + 1))))
387	331	halfcld 12584	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388	387	sincld 16291	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389	154, 105	sseldd 3932	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390		fourierdlem44 47130	. . . . . . . 8 ⊢ (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391	389, 341, 390	syl2anc 596	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392	358, 388, 369, 391	mulne0d 11961	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393	162, 343, 3, 148, 355, 334, 386, 392, 159	divlimc 46635	. . . . 5 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘(𝑗 + 1))))
394	2, 3, 4, 142, 160, 342, 393	mullimc 46597	. . . 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 5966	. . . . . 6 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
399		ioossicc 13557	. . . . . . . 8 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
400		iccss 13538	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
401	19, 98, 85, 107, 400	syl22anc 852	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402	399, 401	sstrid 3942	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403	402	resmptd 6032	. . . . . 6 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404	398, 403	eqtrid 2808	. . . . 5 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405	404	oveq1d 7433	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘(𝑗 + 1))))
406	394, 396, 405	3eltr4d 2876	. . 3 ⊢ (𝜒 → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
407	1, 406	sylbir 238	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
408	242, 249	gtned 11438	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
409		fourierdlem76.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
410	6, 223, 409	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
411	240	oveq2d 7434	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
412	410, 411	eleqtrd 2863	. . . . . . . . . 10 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
413	193	recnd 11330	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℂ)
414	276, 230, 278, 279, 263, 281, 408, 412, 413	fourierdlem53 47138	. . . . . . . . 9 ⊢ (𝜒 → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
415		eqid 2761	. . . . . . . . 9 ⊢ if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)))
416		eqid 2761	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
417	193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416	fourierdlem32 47118	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
418		eqidd 2762	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419		oveq2 7426	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘𝑗)))
420	419	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑆‘𝑗) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
421	420	adantl 487	. . . . . . . . . 10 ⊢ (((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) ∧ 𝑠 = (𝑆‘𝑗)) → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
422	243	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ^*)
423	245	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
424	290	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ℝ)
425	193	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ)
426	310	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
427		neqne 2964	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘𝑗) = (𝑄‘𝑖) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
428	427	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
429	425, 424, 426, 428	leneltd 11457	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘𝑖) < (𝑆‘𝑗))
430	90	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
431	211	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
432	297	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
433	314	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1)))
434	424, 430, 431, 432, 433	ltletrd 11463	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑄‘(𝑖 + 1)))
435	422, 423, 424, 429, 434	eliood 46479	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
436	230, 290	readdcld 11331	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘𝑗)) ∈ ℝ)
437	276, 436	ffvelcdmd 7083	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
438	437	adantr 486	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
439	418, 421, 435, 438	fvmptd 6999	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
440	439	ifeq2da 4515	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))))
441	326	oveq1d 7433	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
442	417, 440, 441	3eltr3d 2875	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
443	290	recnd 11330	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
444	168, 330, 124, 443	constlimc 46605	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘𝑗)))
445	167, 168, 161, 121, 125, 442, 444	sublimc 46631	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘𝑗)))
446	330, 162, 443	idlimc 46607	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘𝑗)))
447	6, 83	jca 521	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
448		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
449	448	anbi2d 642	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵))))
450		neeq1 3018	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ≠ 0 ↔ (𝑆‘𝑗) ≠ 0))
451	449, 450	imbi12d 347	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0)))
452	451, 140	vtoclg 3518	. . . . . . 7 ⊢ ((𝑆‘𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0))
453	83, 447, 452	sylc 66	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ≠ 0)
454	161, 162, 2, 126, 166, 445, 446, 453, 141	divlimc 46635	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘𝑗)))
455	356, 330, 358, 443	constlimc 46605	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘𝑗)))
456	348	ad2antrl 741	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457	162, 356, 364, 148, 368, 446, 455, 369, 152	divlimc 46635	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘𝑗)))
458	290	rehalfcld 12586	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℝ)
459		fveq2 6883	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆‘𝑗) / 2)))
460	378, 458, 459	cnmptlimc 26203	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘𝑗) / 2)))
461		fveq2 6883	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
462	461	ad2antll 742	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
463	456, 363, 457, 460, 382, 462	limcco 26206	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘𝑗)))
464	356, 357, 343, 143, 150, 455, 463	mullimc 46597	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘𝑗)))
465	443	halfcld 12584	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℂ)
466	465	sincld 16291	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ℂ)
467	154, 83	sseldd 3932	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (-π[,]π))
468		fourierdlem44 47130	. . . . . . . 8 ⊢ (((𝑆‘𝑗) ∈ (-π[,]π) ∧ (𝑆‘𝑗) ≠ 0) → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
469	467, 453, 468	syl2anc 596	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
470	358, 466, 369, 469	mulne0d 11961	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ≠ 0)
471	162, 343, 3, 148, 355, 446, 464, 470, 159	divlimc 46635	. . . . 5 ⊢ (𝜒 → ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘𝑗)))
472	2, 3, 4, 142, 160, 454, 471	mullimc 46597	. . . 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 7433	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘𝑗)))
476	472, 474, 475	3eltr4d 2876	. . 3 ⊢ (𝜒 → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
477	1, 476	sylbir 238	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
478	298	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
479	478, 266	syldan 603	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480	479	mpteq2dva 5198	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
481	225	adantr 486	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
482	228	adantr 486	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
483	230	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑋 ∈ ℝ)
484	483, 129	readdcld 11331	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485	240	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
486	193	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
487	243	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
488	245	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
489	487, 488, 478, 248	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) < 𝑠)
490	486, 18, 483, 489	ltadd2dd 11462	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
491	485, 490	eqbrtrd 5127	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
492	211	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493	487, 488, 478, 253	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
494	18, 492, 483, 493	ltadd2dd 11462	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495	260	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496	494, 495	breqtrd 5131	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497	481, 482, 484, 491, 496	eliood 46479	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
498	269, 271, 330, 237, 497	fourierdlem23 47109	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499	480, 498	eqeltrd 2861	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500		ssid 3953	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
501	500	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ℂ ⊆ ℂ)
502	330, 124, 501	constcncfg 46851	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503	499, 502	subcncf 25759	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504	166	ralrimiva 3155	. . . . . . . 8 ⊢ (𝜒 → ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505		dfss3 3920	. . . . . . . 8 ⊢ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506	504, 505	sylibr 237	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507		difssd 4084	. . . . . . 7 ⊢ (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508	506, 507	idcncfg 46852	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509	503, 508	divcncf 25761	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510	330, 501	idcncfg 46852	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511	355, 343	fmptd 7112	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512	330, 358, 501	constcncfg 46851	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513		sincn 26764	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
514	513	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → sin ∈ (ℂ–cn→ℂ))
515	367	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜒 → 2 ∈ (ℂ ∖ {0}))
516	330, 515, 507	constcncfg 46851	. . . . . . . . . . 11 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517	510, 516	divcncf 25761	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518	514, 517	cncfmpt1f 25228	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519	512, 518	mulcncf 25760	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520		cncfcdm 25212	. . . . . . . 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 596	. . . . . . 7 ⊢ (𝜒 → ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522	511, 521	mpbird 260	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523	510, 522	divcncf 25761	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524	509, 523	mulcncf 25760	. . . 4 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525	404, 524	eqeltrd 2861	. . 3 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
526	1, 525	sylbir 238	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527	407, 477, 526	jca31 524	1 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 {crab 3413 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ifcif 4482 {csn 4584 {cpr 4586 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ran crn 5652 ↾ cres 5653 ℩cio 6491 Fun wfun 6531 ⟶wf 6533 –1-1-onto→wf1o 6536 ‘cfv 6537 Isom wiso 6538 (class class class)co 7418 ↑_m cmap 8840 Fincfn 8966 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 · cmul 11198 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 − cmin 11534 -cneg 11535 / cdiv 11966 ℕcn 12328 2c2 12390 ℤcz 12686 (,)cioo 13469 [,)cico 13471 [,]cicc 13472 ...cfz 13632 ..^cfzo 13781 ♯chash 14467 sincsin 16222 πcpi 16225 ↾_t crest 17584 TopOpenctopn 17585 ℂ_fldccnfld 21671 –cn→ccncf 25190 lim_ℂ climc 26175

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ioc 13474 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-mod 14003 df-seq 14138 df-exp 14198 df-fac 14411 df-bc 14440 df-hash 14468 df-shft 15213 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-limsup 15631 df-clim 15648 df-rlim 15649 df-sum 15847 df-ef 16226 df-sin 16228 df-cos 16229 df-pi 16231 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-submnd 18972 df-mulg 19271 df-cntz 19524 df-cmn 19989 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-xms 24632 df-ms 24633 df-tms 24634 df-cncf 25192 df-limc 26179 df-dv 26180

This theorem is used by: fourierdlem86 47171

W3C validator