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 43613

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 2738	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))
3		eqid 2738	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
4		eqid 2738	. . . . 5 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
5		simplll 771	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
6	1, 5	sylbi 216	. . . . . . . . . 10 ⊢ (𝜒 → 𝜑)
7	6	adantr 480	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝜑)
8		ioossicc 13094	. . . . . . . . . 10 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
9		fourierdlem76.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
10	9	rexrd 10956	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
11	6, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐴 ∈ ℝ^*)
12	11	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ∈ ℝ^*)
13		fourierdlem76.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	13	rexrd 10956	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
15	6, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝜒 → 𝐵 ∈ ℝ^*)
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ^*)
17		elioore 13038	. . . . . . . . . . . 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 9019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝐴, 𝐵} ∈ Fin
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin)
24		fzfid 13621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
25		fourierdlem76.q	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
26	25	rnmptfi 42596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
27		infi 8972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
28	24, 26, 27	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
29		unfi 8917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
30	23, 28, 29	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
31	21, 30	eqeltrid 2843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ Fin)
32		prssg 4749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
33	9, 13, 32	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
34	9, 13, 33	mpbi2and 708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
35		inss2 4160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossre 13069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴(,)𝐵) ⊆ ℝ
37	35, 36	sstri 3926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
39	34, 38	unssd 4116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
40	21, 39	eqsstrid 3965	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
41		fourierdlem76.s	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
42		fourierdlem76.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘𝑇) − 1)
43	31, 40, 41, 42	fourierdlem36 43574	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44	6, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
45		isof1o 7174	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
46		f1of 6700	. . . . . . . . . . . . . . . 16 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
47	44, 45, 46	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶𝑇)
48	6, 40	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑇 ⊆ ℝ)
49	47, 48	fssd 6602	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑆:(0...𝑁)⟶ℝ)
51		simpllr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑗 ∈ (0..^𝑁))
52	1, 51	sylbi 216	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑗 ∈ (0..^𝑁))
53		elfzofz 13331	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
54	52, 53	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝑗 ∈ (0...𝑁))
55	54	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑗 ∈ (0...𝑁))
56	50, 55	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ)
57	43, 45, 46	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
58		frn 6591	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆:(0...𝑁)⟶𝑇 → ran 𝑆 ⊆ 𝑇)
59	57, 58	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝑆 ⊆ 𝑇)
60	9	leidd 11471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
61		fourierdlem76.altb	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐴 < 𝐵)
62	9, 13, 61	ltled 11053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
63	9, 13, 9, 60, 62	eliccd 42932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
64	13	leidd 11471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
65	9, 13, 13, 62, 64	eliccd 42932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
66		prssg 4749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
67	9, 13, 66	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
68	63, 65, 67	mpbi2and 708	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
69	35, 8	sstri 3926	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
71	68, 70	unssd 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
72	21, 71	eqsstrid 3965	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
73	59, 72	sstrd 3927	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑆 ⊆ (𝐴[,]𝐵))
74	6, 73	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ran 𝑆 ⊆ (𝐴[,]𝐵))
75		ffun 6587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆:(0...𝑁)⟶ℝ → Fun 𝑆)
76	49, 75	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → Fun 𝑆)
77		fdm 6593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆:(0...𝑁)⟶ℝ → dom 𝑆 = (0...𝑁))
78	49, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → dom 𝑆 = (0...𝑁))
79	78	eqcomd 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (0...𝑁) = dom 𝑆)
80	54, 79	eleqtrd 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑗 ∈ dom 𝑆)
81		fvelrn 6936	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆) → (𝑆‘𝑗) ∈ ran 𝑆)
82	76, 80, 81	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ran 𝑆)
83	74, 82	sseldd 3918	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
84		iccgelb 13064	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝑗))
85	11, 15, 83, 84	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐴 ≤ (𝑆‘𝑗))
86	85	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 ≤ (𝑆‘𝑗))
87	56	rexrd 10956	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) ∈ ℝ^*)
88		fzofzp1 13412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
89	52, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ (0...𝑁))
90	49, 89	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
91	90	rexrd 10956	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
92	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ^*)
93		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
94		ioogtlb 42923	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
95	87, 92, 93, 94	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘𝑗) < 𝑠)
96	20, 56, 18, 86, 95	lelttrd 11063	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐴 < 𝑠)
97	90	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
98	6, 13	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜒 → 𝐵 ∈ ℝ)
99	98	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐵 ∈ ℝ)
100		iooltub 42938	. . . . . . . . . . . . 13 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
101	87, 92, 93, 100	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑆‘(𝑗 + 1)))
102	89, 79	eleqtrd 2841	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑗 + 1) ∈ dom 𝑆)
103		fvelrn 6936	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑆 ∧ (𝑗 + 1) ∈ dom 𝑆) → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
104	76, 102, 103	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ran 𝑆)
105	74, 104	sseldd 3918	. . . . . . . . . . . . . 14 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
106		iccleub 13063	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
107	11, 15, 105, 106	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
108	107	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑆‘(𝑗 + 1)) ≤ 𝐵)
109	18, 97, 99, 101, 108	ltletrd 11065	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < 𝐵)
110	12, 16, 18, 96, 109	eliood 42926	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴(,)𝐵))
111	8, 110	sselid 3915	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (𝐴[,]𝐵))
112		fourierdlem76.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
113	112	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
114		fourierdlem76.xre	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ)
115	114	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
116	9, 13	iccssred 13095	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
117	116	sselda 3917	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
118	115, 117	readdcld 10935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
119	113, 118	ffvelrnd 6944	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
120	7, 111, 119	syl2anc 583	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
121	120	recnd 10934	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
122		fourierdlem76.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
123	122	recnd 10934	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
124	6, 123	syl 17	. . . . . . . 8 ⊢ (𝜒 → 𝐶 ∈ ℂ)
125	124	adantr 480	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝐶 ∈ ℂ)
126	121, 125	subcld 11262	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
127		ioossre 13069	. . . . . . . . 9 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
128	127	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
129	128	sselda 3917	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℝ)
130	129	recnd 10934	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
131		nne 2946	. . . . . . . . . . . 12 ⊢ (¬ 𝑠 ≠ 0 ↔ 𝑠 = 0)
132	131	biimpi 215	. . . . . . . . . . 11 ⊢ (¬ 𝑠 ≠ 0 → 𝑠 = 0)
133	132	eqcomd 2744	. . . . . . . . . 10 ⊢ (¬ 𝑠 ≠ 0 → 0 = 𝑠)
134	133	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 = 𝑠)
135		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
136	135	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 𝑠 ∈ (𝐴[,]𝐵))
137	134, 136	eqeltrd 2839	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → 0 ∈ (𝐴[,]𝐵))
138		fourierdlem76.n0	. . . . . . . . 9 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
139	138	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑠 ≠ 0) → ¬ 0 ∈ (𝐴[,]𝐵))
140	137, 139	condan 814	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
141	7, 111, 140	syl2anc 583	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ≠ 0)
142	126, 130, 141	divcld 11681	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℂ)
143		2cnd 11981	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℂ)
144	130	halfcld 12148	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
145	144	sincld 15767	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
146	143, 145	mulcld 10926	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
147	17	recnd 10934	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → 𝑠 ∈ ℂ)
148	147	adantl 481	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ℂ)
149	148	halfcld 12148	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / 2) ∈ ℂ)
150	149	sincld 15767	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℂ)
151		2ne0 12007	. . . . . . . 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 3918	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (-π[,]π))
157		fourierdlem44 43582	. . . . . . . 8 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
158	156, 141, 157	syl2anc 583	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ≠ 0)
159	143, 150, 152, 158	mulne0d 11557	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
160	130, 146, 159	divcld 11681	. . . . 5 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
161		eqid 2738	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))
162		eqid 2738	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠)
163	141	neneqd 2947	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 = 0)
164		velsn 4574	. . . . . . . 8 ⊢ (𝑠 ∈ {0} ↔ 𝑠 = 0)
165	163, 164	sylnibr 328	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ 𝑠 ∈ {0})
166	130, 165	eldifd 3894	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
167		eqid 2738	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
168		eqid 2738	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶)
169		elfzofz 13331	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170	169	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
171		pire 25520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ∈ ℝ
172	171	renegcli 11212	. . . . . . . . . . . . . . . . . . . 20 ⊢ -π ∈ ℝ
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → -π ∈ ℝ)
174	173, 114	readdcld 10935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (-π + 𝑋) ∈ ℝ)
175	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → π ∈ ℝ)
176	175, 114	readdcld 10935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (π + 𝑋) ∈ ℝ)
177	174, 176	iccssred 13095	. . . . . . . . . . . . . . . . 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 43553	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
183	182	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
184	183, 170	ffvelrnd 6944	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
185	178, 184	sseldd 3918	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ)
186	114	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
187	185, 186	resubcld 11333	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ)
188	25	fvmpt2 6868	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
189	170, 187, 188	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
190	189, 187	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
191	190	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
192	191	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
193	1, 192	sylbi 216	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ)
194		fveq2 6756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑉‘𝑖) = (𝑉‘𝑗))
195	194	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑗) − 𝑋))
196	195	cbvmptv 5183	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
197	25, 196	eqtri 2766	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋))
198	197	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉‘𝑗) − 𝑋)))
199		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑖 + 1) → (𝑉‘𝑗) = (𝑉‘(𝑖 + 1)))
200	199	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑖 + 1) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
201	200	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉‘𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
202		fzofzp1 13412	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
203	202	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
204	183, 203	ffvelrnd 6944	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ((-π + 𝑋)[,](π + 𝑋)))
205	178, 204	sseldd 3918	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
206	205, 186	resubcld 11333	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
207	198, 201, 203, 206	fvmptd 6864	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
208	207, 206	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
209	208	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
211	1, 210	sylbi 216	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
212	179	fourierdlem2 43540	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
213	180, 212	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))))
214	181, 213	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))
215	214	simprrd 770	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
216	215	r19.21bi 3132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))
217	185, 205, 186, 216	ltsub1dd 11517	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑉‘𝑖) − 𝑋) < ((𝑉‘(𝑖 + 1)) − 𝑋))
218	217, 189, 207	3brtr4d 5102	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
219	218	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
220	219	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
221	1, 220	sylbi 216	. . . . . . . . 9 ⊢ (𝜒 → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
222	1	biimpi 215	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
223	222	simplrd 766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → 𝑖 ∈ (0..^𝑀))
224	6, 223, 185	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ)
225	224	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ^*)
226	225	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) ∈ ℝ^*)
227	6, 223, 205	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
228	227	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
229	228	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ^*)
230	6, 114	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → 𝑋 ∈ ℝ)
231	230	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
232		elioore 13038	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
233	232	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
234	231, 233	readdcld 10935	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
235	6, 223, 189	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋))
236	235	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) = (𝑋 + ((𝑉‘𝑖) − 𝑋)))
237	230	recnd 10934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → 𝑋 ∈ ℂ)
238	224	recnd 10934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘𝑖) ∈ ℂ)
239	237, 238	pncan3d 11265	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘𝑖) − 𝑋)) = (𝑉‘𝑖))
240	236, 239	eqtr2d 2779	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
241	240	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
242	193	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
243	193	rexrd 10956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ^*)
244	243	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
245	211	rexrd 10956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
246	245	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
247		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
248		ioogtlb 42923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
249	244, 246, 247, 248	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑠)
250	242, 233, 231, 249	ltadd2dd 11064	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
251	241, 250	eqbrtrd 5092	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
252	211	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
253		iooltub 42938	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑖) ∈ ℝ^* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ^* ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
254	244, 246, 247, 253	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
255	233, 252, 231, 254	ltadd2dd 11064	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
256	6, 223, 207	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
257	256	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
258	227	recnd 10934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
259	237, 258	pncan3d 11265	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
260	257, 259	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
261	260	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
262	255, 261	breqtrd 5096	. . . . . . . . . . . . . 14 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
263	226, 229, 234, 251, 262	eliood 42926	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
264		fvres 6775	. . . . . . . . . . . . 13 ⊢ ((𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
265	263, 264	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
266	265	eqcomd 2744	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
267	266	mpteq2dva 5170	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))))
268		ioosscn 13070	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℂ)
270		fourierdlem76.fcn	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
271	6, 223, 270	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
272		ioosscn 13070	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
273	272	a1i 11	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
274	269, 271, 273, 237, 263	fourierdlem23 43561	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
275	267, 274	eqeltrd 2839	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
276	6, 112	syl 17	. . . . . . . . . 10 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
277		ioossre 13069	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
278	277	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
279		eqid 2738	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
280		ioossre 13069	. . . . . . . . . . 11 ⊢ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
281	280	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
282	233, 254	ltned 11041	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
283		fourierdlem76.l	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
284	6, 223, 283	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
285	260	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
286	285	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
287	284, 286	eleqtrd 2841	. . . . . . . . . 10 ⊢ (𝜒 → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘(𝑖 + 1)))))
288	211	recnd 10934	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℂ)
289	276, 230, 278, 279, 263, 281, 282, 287, 288	fourierdlem53 43590	. . . . . . . . 9 ⊢ (𝜒 → 𝐿 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘(𝑖 + 1))))
290	49, 54	ffvelrnd 6944	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
291		elfzoelz 13316	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
292		zre 12253	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
293	52, 291, 292	3syl 18	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑗 ∈ ℝ)
294	293	ltp1d 11835	. . . . . . . . . 10 ⊢ (𝜒 → 𝑗 < (𝑗 + 1))
295		isorel 7177	. . . . . . . . . . 11 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
296	44, 54, 89, 295	syl12anc 833	. . . . . . . . . 10 ⊢ (𝜒 → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
297	294, 296	mpbid 231	. . . . . . . . 9 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
298	1	simprbi 496	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
299		eqid 2738	. . . . . . . . 9 ⊢ if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))))
300		eqid 2738	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∪ {(𝑄‘(𝑖 + 1))}))
301	193, 211, 221, 275, 289, 290, 90, 297, 298, 299, 300	fourierdlem33 43571	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
302		eqidd 2739	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
303		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → 𝑠 = (𝑆‘(𝑗 + 1)))
304	303	oveq2d 7271	. . . . . . . . . . 11 ⊢ (((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) ∧ 𝑠 = (𝑆‘(𝑗 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘(𝑗 + 1))))
305	304	fveq2d 6760	. . . . . . . . . 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 43548	. . . . . . . . . . . . . 14 ⊢ (𝜒 → ((𝑄‘𝑖) ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ (𝑄‘(𝑖 + 1))))
310	309	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜒 → (𝑄‘𝑖) ≤ (𝑆‘𝑗))
311	193, 290, 90, 310, 297	lelttrd 11063	. . . . . . . . . . . 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 2950	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑆‘(𝑗 + 1)) ≠ (𝑄‘(𝑖 + 1)))
317	316	necomd 2998	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
318	317	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑆‘(𝑗 + 1)))
319	308, 313, 315, 318	leneltd 11059	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) < (𝑄‘(𝑖 + 1)))
320	306, 307, 308, 312, 319	eliood 42926	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝑆‘(𝑗 + 1)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
321	230, 90	readdcld 10935	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘(𝑗 + 1))) ∈ ℝ)
322	276, 321	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
323	322	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))) ∈ ℝ)
324	302, 305, 320, 323	fvmptd 6864	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1))) = (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
325	324	ifeq2da 4488	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘(𝑗 + 1)))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
326	298	resmptd 5937	. . . . . . . . 9 ⊢ (𝜒 → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
327	326	oveq1d 7270	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
328	301, 325, 327	3eltr3d 2853	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘(𝑗 + 1))))
329		ax-resscn 10859	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
330	128, 329	sstrdi 3929	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℂ)
331	90	recnd 10934	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℂ)
332	168, 330, 124, 331	constlimc 43055	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘(𝑗 + 1))))
333	167, 168, 161, 121, 125, 328, 332	sublimc 43083	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘(𝑗 + 1))))
334	330, 162, 331	idlimc 43057	. . . . . 6 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘(𝑗 + 1))))
335	6, 105	jca 511	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
336		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)))
337	336	anbi2d 628	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))))
338		neeq1 3005	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (𝑠 ≠ 0 ↔ (𝑆‘(𝑗 + 1)) ≠ 0))
339	337, 338	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘(𝑗 + 1)) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝑗 + 1)) ≠ 0)))
340	339, 140	vtoclg 3495	. . . . . . 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 43087	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘(𝑗 + 1))))
343		eqid 2738	. . . . . 6 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))
344	143, 150	mulcld 10926	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
345	159	neneqd 2947	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
346		2re 11977	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
347	346	a1i 11	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 2 ∈ ℝ)
348	17	rehalfcld 12150	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (𝑠 / 2) ∈ ℝ)
349	348	resincld 15780	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (sin‘(𝑠 / 2)) ∈ ℝ)
350	349	adantl 481	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (sin‘(𝑠 / 2)) ∈ ℝ)
351	347, 350	remulcld 10936	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
352		elsng 4572	. . . . . . . . 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 324	. . . . . . 7 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
355	344, 354	eldifd 3894	. . . . . 6 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
356		eqid 2738	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2)
357		eqid 2738	. . . . . . 7 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2)))
358		2cnd 11981	. . . . . . . 8 ⊢ (𝜒 → 2 ∈ ℂ)
359	356, 330, 358, 331	constlimc 43055	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘(𝑗 + 1))))
360	348	ad2antrl 724	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘(𝑗 + 1)) / 2))) → (𝑠 / 2) ∈ ℝ)
361		recn 10892	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
362	361	sincld 15767	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (sin‘𝑥) ∈ ℂ)
363	362	adantl 481	. . . . . . . 8 ⊢ ((𝜒 ∧ 𝑥 ∈ ℝ) → (sin‘𝑥) ∈ ℂ)
364		eqid 2738	. . . . . . . . 9 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2))
365		2cn 11978	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
366		eldifsn 4717	. . . . . . . . . . 11 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
367	365, 151, 366	mpbir2an 707	. . . . . . . . . 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 43087	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘(𝑗 + 1))))
371		sinf 15761	. . . . . . . . . . . . . 14 ⊢ sin:ℂ⟶ℂ
372	371	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → sin:ℂ⟶ℂ)
373	329	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → ℝ ⊆ ℂ)
374	372, 373	feqresmpt 6820	. . . . . . . . . . . 12 ⊢ (⊤ → (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥)))
375	374	mptru 1546	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) = (𝑥 ∈ ℝ ↦ (sin‘𝑥))
376		resincncf 43306	. . . . . . . . . . 11 ⊢ (sin ↾ ℝ) ∈ (ℝ–cn→ℝ)
377	375, 376	eqeltrri 2836	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ)
378	377	a1i 11	. . . . . . . . 9 ⊢ (𝜒 → (𝑥 ∈ ℝ ↦ (sin‘𝑥)) ∈ (ℝ–cn→ℝ))
379	90	rehalfcld 12150	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℝ)
380		fveq2 6756	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘𝑥) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
381	378, 379, 380	cnmptlimc 24959	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘(𝑗 + 1)) / 2)))
382		fveq2 6756	. . . . . . . 8 ⊢ (𝑥 = (𝑠 / 2) → (sin‘𝑥) = (sin‘(𝑠 / 2)))
383		fveq2 6756	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
384	383	ad2antll 725	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘(𝑗 + 1)) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘(𝑗 + 1)) / 2)))
385	360, 363, 370, 381, 382, 384	limcco 24962	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘(𝑗 + 1))))
386	356, 357, 343, 143, 150, 359, 385	mullimc 43047	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘(𝑗 + 1))))
387	331	halfcld 12148	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / 2) ∈ ℂ)
388	387	sincld 15767	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ∈ ℂ)
389	154, 105	sseldd 3918	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ (-π[,]π))
390		fourierdlem44 43582	. . . . . . . 8 ⊢ (((𝑆‘(𝑗 + 1)) ∈ (-π[,]π) ∧ (𝑆‘(𝑗 + 1)) ≠ 0) → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
391	389, 341, 390	syl2anc 583	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘(𝑗 + 1)) / 2)) ≠ 0)
392	358, 388, 369, 391	mulne0d 11557	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))) ≠ 0)
393	162, 343, 3, 148, 355, 334, 386, 392, 159	divlimc 43087	. . . . 5 ⊢ (𝜒 → ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘(𝑗 + 1))))
394	2, 3, 4, 142, 160, 342, 393	mullimc 43047	. . . 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 5876	. . . . . 6 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
399		ioossicc 13094	. . . . . . . 8 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
400		iccss 13076	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝑆‘𝑗) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐵)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
401	19, 98, 85, 107, 400	syl22anc 835	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
402	399, 401	sstrid 3928	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
403	402	resmptd 5937	. . . . . 6 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
404	398, 403	syl5eq 2791	. . . . 5 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
405	404	oveq1d 7270	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘(𝑗 + 1))))
406	394, 396, 405	3eltr4d 2854	. . 3 ⊢ (𝜒 → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
407	1, 406	sylbir 234	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
408	242, 249	gtned 11040	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘𝑖))
409		fourierdlem76.r	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
410	6, 223, 409	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
411	240	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜒 → ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
412	410, 411	eleqtrd 2841	. . . . . . . . . 10 ⊢ (𝜒 → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑋 + (𝑄‘𝑖))))
413	193	recnd 10934	. . . . . . . . . 10 ⊢ (𝜒 → (𝑄‘𝑖) ∈ ℂ)
414	276, 230, 278, 279, 263, 281, 408, 412, 413	fourierdlem53 43590	. . . . . . . . 9 ⊢ (𝜒 → 𝑅 ∈ ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑄‘𝑖)))
415		eqid 2738	. . . . . . . . 9 ⊢ if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)))
416		eqid 2738	. . . . . . . . 9 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1))))
417	193, 211, 221, 275, 414, 290, 90, 297, 298, 415, 416	fourierdlem32 43570	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) ∈ (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
418		eqidd 2739	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))))
419		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑋 + 𝑠) = (𝑋 + (𝑆‘𝑗)))
420	419	fveq2d 6760	. . . . . . . . . . 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 2950	. . . . . . . . . . . . 13 ⊢ (¬ (𝑆‘𝑗) = (𝑄‘𝑖) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
428	427	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ≠ (𝑄‘𝑖))
429	425, 424, 426, 428	leneltd 11059	. . . . . . . . . . 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 11065	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) < (𝑄‘(𝑖 + 1)))
435	422, 423, 424, 429, 434	eliood 42926	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝑆‘𝑗) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
436	230, 290	readdcld 10935	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝑋 + (𝑆‘𝑗)) ∈ ℝ)
437	276, 436	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ (𝜒 → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
438	437	adantr 480	. . . . . . . . . 10 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → (𝐹‘(𝑋 + (𝑆‘𝑗))) ∈ ℝ)
439	418, 421, 435, 438	fvmptd 6864	. . . . . . . . 9 ⊢ ((𝜒 ∧ ¬ (𝑆‘𝑗) = (𝑄‘𝑖)) → ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗)) = (𝐹‘(𝑋 + (𝑆‘𝑗))))
440	439	ifeq2da 4488	. . . . . . . 8 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, ((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))‘(𝑆‘𝑗))) = if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))))
441	326	oveq1d 7270	. . . . . . . 8 ⊢ (𝜒 → (((𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
442	417, 440, 441	3eltr3d 2853	. . . . . . 7 ⊢ (𝜒 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim_ℂ (𝑆‘𝑗)))
443	290	recnd 10934	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℂ)
444	168, 330, 124, 443	constlimc 43055	. . . . . . 7 ⊢ (𝜒 → 𝐶 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) lim_ℂ (𝑆‘𝑗)))
445	167, 168, 161, 121, 125, 442, 444	sublimc 43083	. . . . . 6 ⊢ (𝜒 → (if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) lim_ℂ (𝑆‘𝑗)))
446	330, 162, 443	idlimc 43057	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) lim_ℂ (𝑆‘𝑗)))
447	6, 83	jca 511	. . . . . . 7 ⊢ (𝜒 → (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
448		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ∈ (𝐴[,]𝐵) ↔ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)))
449	448	anbi2d 628	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵))))
450		neeq1 3005	. . . . . . . . 9 ⊢ (𝑠 = (𝑆‘𝑗) → (𝑠 ≠ 0 ↔ (𝑆‘𝑗) ≠ 0))
451	449, 450	imbi12d 344	. . . . . . . 8 ⊢ (𝑠 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0)))
452	451, 140	vtoclg 3495	. . . . . . 7 ⊢ ((𝑆‘𝑗) ∈ (𝐴[,]𝐵) → ((𝜑 ∧ (𝑆‘𝑗) ∈ (𝐴[,]𝐵)) → (𝑆‘𝑗) ≠ 0))
453	83, 447, 452	sylc 65	. . . . . 6 ⊢ (𝜒 → (𝑆‘𝑗) ≠ 0)
454	161, 162, 2, 126, 166, 445, 446, 453, 141	divlimc 43087	. . . . 5 ⊢ (𝜒 → ((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) lim_ℂ (𝑆‘𝑗)))
455	356, 330, 358, 443	constlimc 43055	. . . . . . 7 ⊢ (𝜒 → 2 ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) lim_ℂ (𝑆‘𝑗)))
456	348	ad2antrl 724	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) ≠ ((𝑆‘𝑗) / 2))) → (𝑠 / 2) ∈ ℝ)
457	162, 356, 364, 148, 368, 446, 455, 369, 152	divlimc 43087	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) lim_ℂ (𝑆‘𝑗)))
458	290	rehalfcld 12150	. . . . . . . . 9 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℝ)
459		fveq2 6756	. . . . . . . . 9 ⊢ (𝑥 = ((𝑆‘𝑗) / 2) → (sin‘𝑥) = (sin‘((𝑆‘𝑗) / 2)))
460	378, 458, 459	cnmptlimc 24959	. . . . . . . 8 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑥 ∈ ℝ ↦ (sin‘𝑥)) lim_ℂ ((𝑆‘𝑗) / 2)))
461		fveq2 6756	. . . . . . . . 9 ⊢ ((𝑠 / 2) = ((𝑆‘𝑗) / 2) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
462	461	ad2antll 725	. . . . . . . 8 ⊢ ((𝜒 ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ (𝑠 / 2) = ((𝑆‘𝑗) / 2))) → (sin‘(𝑠 / 2)) = (sin‘((𝑆‘𝑗) / 2)))
463	456, 363, 457, 460, 382, 462	limcco 24962	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) lim_ℂ (𝑆‘𝑗)))
464	356, 357, 343, 143, 150, 455, 463	mullimc 43047	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) lim_ℂ (𝑆‘𝑗)))
465	443	halfcld 12148	. . . . . . . 8 ⊢ (𝜒 → ((𝑆‘𝑗) / 2) ∈ ℂ)
466	465	sincld 15767	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ∈ ℂ)
467	154, 83	sseldd 3918	. . . . . . . 8 ⊢ (𝜒 → (𝑆‘𝑗) ∈ (-π[,]π))
468		fourierdlem44 43582	. . . . . . . 8 ⊢ (((𝑆‘𝑗) ∈ (-π[,]π) ∧ (𝑆‘𝑗) ≠ 0) → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
469	467, 453, 468	syl2anc 583	. . . . . . 7 ⊢ (𝜒 → (sin‘((𝑆‘𝑗) / 2)) ≠ 0)
470	358, 466, 369, 469	mulne0d 11557	. . . . . 6 ⊢ (𝜒 → (2 · (sin‘((𝑆‘𝑗) / 2))) ≠ 0)
471	162, 343, 3, 148, 355, 446, 464, 470, 159	divlimc 43087	. . . . 5 ⊢ (𝜒 → ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))) ∈ ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim_ℂ (𝑆‘𝑗)))
472	2, 3, 4, 142, 160, 454, 471	mullimc 43047	. . . 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 7270	. . . 4 ⊢ (𝜒 → ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) = ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim_ℂ (𝑆‘𝑗)))
476	472, 474, 475	3eltr4d 2854	. . 3 ⊢ (𝜒 → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
477	1, 476	sylbir 234	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
478	298	sselda 3917	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
479	478, 266	syldan 590	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠)))
480	479	mpteq2dva 5170	. . . . . . . 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 10935	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
485	240	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖)))
486	193	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
487	243	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) ∈ ℝ^*)
488	245	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
489	487, 488, 478, 248	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘𝑖) < 𝑠)
490	486, 18, 483, 489	ltadd2dd 11064	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘𝑖)) < (𝑋 + 𝑠))
491	485, 490	eqbrtrd 5092	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑉‘𝑖) < (𝑋 + 𝑠))
492	211	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493	487, 488, 478, 253	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
494	18, 492, 483, 493	ltadd2dd 11064	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
495	260	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
496	494, 495	breqtrd 5096	. . . . . . . . . 10 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
497	481, 482, 484, 491, 496	eliood 42926	. . . . . . . . 9 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))
498	269, 271, 330, 237, 497	fourierdlem23 43561	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1))))‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
499	480, 498	eqeltrd 2839	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
500		ssid 3939	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
501	500	a1i 11	. . . . . . . 8 ⊢ (𝜒 → ℂ ⊆ ℂ)
502	330, 124, 501	constcncfg 43303	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝐶) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
503	499, 502	subcncf 24514	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
504	166	ralrimiva 3107	. . . . . . . 8 ⊢ (𝜒 → ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
505		dfss3 3905	. . . . . . . 8 ⊢ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}) ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))𝑠 ∈ (ℂ ∖ {0}))
506	504, 505	sylibr 233	. . . . . . 7 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (ℂ ∖ {0}))
507		difssd 4063	. . . . . . 7 ⊢ (𝜒 → (ℂ ∖ {0}) ⊆ ℂ)
508	506, 507	idcncfg 43304	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
509	503, 508	divcncf 24516	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
510	330, 501	idcncfg 43304	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 𝑠) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
511	355, 343	fmptd 6970	. . . . . . 7 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0}))
512	330, 358, 501	constcncfg 43303	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
513		sincn 25508	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
514	513	a1i 11	. . . . . . . . . 10 ⊢ (𝜒 → sin ∈ (ℂ–cn→ℂ))
515	367	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜒 → 2 ∈ (ℂ ∖ {0}))
516	330, 515, 507	constcncfg 43303	. . . . . . . . . . 11 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ 2) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
517	510, 516	divcncf 24516	. . . . . . . . . 10 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / 2)) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
518	514, 517	cncfmpt1f 23983	. . . . . . . . 9 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (sin‘(𝑠 / 2))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
519	512, 518	mulcncf 24515	. . . . . . . 8 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
520		cncffvrn 23967	. . . . . . . 8 ⊢ (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) → ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
521	507, 519, 520	syl2anc 583	. . . . . . 7 ⊢ (𝜒 → ((𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶(ℂ ∖ {0})))
522	511, 521	mpbird 256	. . . . . 6 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→(ℂ ∖ {0})))
523	510, 522	divcncf 24516	. . . . 5 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
524	509, 523	mulcncf 24515	. . . 4 ⊢ (𝜒 → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
525	404, 524	eqeltrd 2839	. . 3 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
526	1, 525	sylbir 234	. 2 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
527	407, 477, 526	jca31 514	1 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ⊤wtru 1540 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 {crab 3067 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ifcif 4456 {csn 4558 {cpr 4560 class class class wbr 5070 ↦ cmpt 5153 dom cdm 5580 ran crn 5581 ↾ cres 5582 ℩cio 6374 Fun wfun 6412 ⟶wf 6414 –1-1-onto→wf1o 6417 ‘cfv 6418 Isom wiso 6419 (class class class)co 7255 ↑_m cmap 8573 Fincfn 8691 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 ℤcz 12249 (,)cioo 13008 [,)cico 13010 [,]cicc 13011 ...cfz 13168 ..^cfzo 13311 ♯chash 13972 sincsin 15701 πcpi 15704 ↾_t crest 17048 TopOpenctopn 17049 ℂ_fldccnfld 20510 –cn→ccncf 23945 lim_ℂ climc 24931

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ioc 13013 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-fac 13916 df-bc 13945 df-hash 13973 df-shft 14706 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-limsup 15108 df-clim 15125 df-rlim 15126 df-sum 15326 df-ef 15705 df-sin 15707 df-cos 15708 df-pi 15710 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-hom 16912 df-cco 16913 df-rest 17050 df-topn 17051 df-0g 17069 df-gsum 17070 df-topgen 17071 df-pt 17072 df-prds 17075 df-xrs 17130 df-qtop 17135 df-imas 17136 df-xps 17138 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-submnd 18346 df-mulg 18616 df-cntz 18838 df-cmn 19303 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-fbas 20507 df-fg 20508 df-cnfld 20511 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-nei 22157 df-lp 22195 df-perf 22196 df-cn 22286 df-cnp 22287 df-haus 22374 df-tx 22621 df-hmeo 22814 df-fil 22905 df-fm 22997 df-flim 22998 df-flf 22999 df-xms 23381 df-ms 23382 df-tms 23383 df-cncf 23947 df-limc 24935 df-dv 24936

This theorem is referenced by: fourierdlem86 43623

W3C validator