fourierdlem80 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem80 46224

Description: The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem80.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem80.xre	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem80.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem80.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem80.ab	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem80.n0	⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem80.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem80.o	⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
fourierdlem80.i	⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
fourierdlem80.fbdioo	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
fourierdlem80.fdvbdioo	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
fourierdlem80.sf	⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
fourierdlem80.slt	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
fourierdlem80.sjss	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
fourierdlem80.relioo	⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
fdv	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ)
fourierdlem80.y	⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
fourierdlem80.ch	⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))

**Assertion**
Ref	Expression
fourierdlem80	⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)

Distinct variable groups: 𝐴,𝑏,𝑟,𝑠,𝑡 𝐵,𝑏,𝑟,𝑠,𝑡 𝐶,𝑏,𝑟,𝑠,𝑡 𝐹,𝑏,𝑟,𝑠,𝑡 𝑤,𝐹,𝑧,𝑠,𝑡 𝑤,𝐼,𝑧 𝑁,𝑏,𝑗,𝑟,𝑠 𝑘,𝑁,𝑗,𝑟 𝑤,𝑁,𝑧,𝑗 𝑂,𝑏,𝑗,𝑟 𝑤,𝑂,𝑧 𝑆,𝑏,𝑗,𝑟,𝑠,𝑡 𝑆,𝑘 𝑤,𝑆,𝑧 𝑋,𝑏,𝑟,𝑠,𝑡 𝑌,𝑠 𝜑,𝑏,𝑗,𝑟,𝑠 𝜒,𝑠,𝑡 𝜑,𝑤,𝑧 Allowed substitution hints: 𝜑(𝑡,𝑘) 𝜒(𝑧,𝑤,𝑗,𝑘,𝑟,𝑏) 𝐴(𝑧,𝑤,𝑗,𝑘) 𝐵(𝑧,𝑤,𝑗,𝑘) 𝐶(𝑧,𝑤,𝑗,𝑘) 𝐹(𝑗,𝑘) 𝐼(𝑡,𝑗,𝑘,𝑠,𝑟,𝑏) 𝑁(𝑡) 𝑂(𝑡,𝑘,𝑠) 𝑋(𝑧,𝑤,𝑗,𝑘) 𝑌(𝑧,𝑤,𝑡,𝑗,𝑘,𝑟,𝑏)

Proof of Theorem fourierdlem80 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem80.o	. . . . . . . . 9 ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
2		oveq2 7349	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
3	2	fveq2d 6821	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
4	3	oveq1d 7356	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) = ((𝐹‘(𝑋 + 𝑡)) − 𝐶))
5		oveq1 7348	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑠 / 2) = (𝑡 / 2))
6	5	fveq2d 6821	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (sin‘(𝑠 / 2)) = (sin‘(𝑡 / 2)))
7	6	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (2 · (sin‘(𝑠 / 2))) = (2 · (sin‘(𝑡 / 2))))
8	4, 7	oveq12d 7359	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) = (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
9	8	cbvmptv 5190	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
10	1, 9	eqtr2i 2755	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))) = 𝑂
11	10	oveq2i 7352	. . . . . . 7 ⊢ (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = (ℝ D 𝑂)
12	11	dmeqi 5839	. . . . . 6 ⊢ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = dom (ℝ D 𝑂)
13	12	ineq2i 4162	. . . . 5 ⊢ (ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))))) = (ran 𝑆 ∩ dom (ℝ D 𝑂))
14	13	sneqi 4582	. . . 4 ⊢ {(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} = {(ran 𝑆 ∩ dom (ℝ D 𝑂))}
15	14	uneq1i 4109	. . 3 ⊢ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
16		snfi 8960	. . . . 5 ⊢ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin
17		fzofi 13876	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
18		eqid 2731	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
19	18	rnmptfi 45208	. . . . . 6 ⊢ ((0..^𝑁) ∈ Fin → ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin)
20	17, 19	ax-mp 5	. . . . 5 ⊢ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin
21		unfi 9075	. . . . 5 ⊢ (({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin ∧ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin) → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
22	16, 20, 21	mp2an 692	. . . 4 ⊢ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin
23	22	a1i 11	. . 3 ⊢ (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
24	15, 23	eqeltrid 2835	. 2 ⊢ (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
25		id 22	. . . 4 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
26	15	unieqi 4866	. . . 4 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
27	25, 26	eleqtrdi 2841	. . 3 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
28		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → 𝜑)
29		uniun 4877	. . . . . . . . 9 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
30	29	eleq2i 2823	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ 𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
31		elun 4098	. . . . . . . 8 ⊢ (𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
32	30, 31	sylbb 219	. . . . . . 7 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
33	32	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
34		fourierdlem80.sf	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
35		ovex 7374	. . . . . . . . . . . 12 ⊢ (0...𝑁) ∈ V
36	35	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ V)
37	34, 36	fexd 7156	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
38		rnexg 7827	. . . . . . . . . 10 ⊢ (𝑆 ∈ V → ran 𝑆 ∈ V)
39		inex1g 5252	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ V → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
40		unisng 4872	. . . . . . . . . 10 ⊢ ((ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V → ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
41	37, 38, 39, 40	4syl 19	. . . . . . . . 9 ⊢ (𝜑 → ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
42	41	eleq2d 2817	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
43	42	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
44	43	orbi1d 916	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))))
45	33, 44	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
46		dvf 25830	. . . . . . . . 9 ⊢ (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ
47	46	a1i 11	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
48		elinel2 4147	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → 𝑠 ∈ dom (ℝ D 𝑂))
49	47, 48	ffvelcdmd 7013	. . . . . . 7 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
50	49	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
51		ovex 7374	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∈ V
52	51	dfiun3 5904	. . . . . . . . . . 11 ⊢ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
53	52	eleq2i 2823	. . . . . . . . . 10 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
54	53	biimpri 228	. . . . . . . . 9 ⊢ (𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
55	54	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
56		eliun 4940	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
57	55, 56	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
58		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
59		nfmpt1 5185	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
60	59	nfrn 5887	. . . . . . . . . . 11 ⊢ Ⅎ𝑗ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
61	60	nfuni 4861	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
62	61	nfcri 2886	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
63	58, 62	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
64		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑗((ℝ D 𝑂)‘𝑠) ∈ ℂ
65	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
66		fourierdlem80.y	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
67	1	reseq1i 5919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
68		ioossicc 13328	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
69		fourierdlem80.sjss	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
70	68, 69	sstrid 3941	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
71	70	resmptd 5984	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
72	67, 71	eqtrid 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
73	66, 72	eqtr4id 2785	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
74	73	oveq2d 7357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
75		ax-resscn 11058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ℝ ⊆ ℂ)
77		fourierdlem80.f	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
78	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
79		fourierdlem80.xre	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ ℝ)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
81		fourierdlem80.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ ℝ)
82		fourierdlem80.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ℝ)
83	81, 82	iccssred 13329	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
84	83	sselda 3929	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
85	80, 84	readdcld 11136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
86	78, 85	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
87	86	recnd 11135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
88		fourierdlem80.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ∈ ℝ)
89	88	recnd 11135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℂ)
90	89	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)
91	87, 90	subcld 11467	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
92		2cnd 12198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
93	83, 76	sstrd 3940	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
94	93	sselda 3929	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℂ)
95	94	halfcld 12361	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑠 / 2) ∈ ℂ)
96	95	sincld 16034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
97	92, 96	mulcld 11127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
98		2ne0 12224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ≠ 0
99	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
100		fourierdlem80.ab	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
101	100	sselda 3929	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (-π[,]π))
102		eqcom 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
103	102	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 0 → 0 = 𝑠)
104	103	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
105		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴[,]𝐵))
106	104, 105	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
107	106	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
108		fourierdlem80.n0	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
109	108	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
110	107, 109	pm2.65da 816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ¬ 𝑠 = 0)
111	110	neqned 2935	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
112		fourierdlem44 46189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
113	101, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
114	92, 96, 99, 113	mulne0d 11764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
115	91, 97, 114	divcld 11892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
116	115, 1	fmptd 7042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑂:(𝐴[,]𝐵)⟶ℂ)
117		ioossre 13302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
119		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
120		tgioo4 24715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
121	119, 120	dvres 25834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℝ ⊆ ℂ ∧ 𝑂:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
122	76, 116, 83, 118, 121	syl22anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
123		ioontr 45551	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))
124	123	reseq2i 5920	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
125	122, 124	eqtrdi 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
126	125	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
127	74, 126	eqtr2d 2767	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (ℝ D 𝑌))
128	127	dmeqd 5840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = dom (ℝ D 𝑌))
129	77	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℝ)
130	79	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑋 ∈ ℝ)
131	83	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
132	34	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
133		elfzofz 13570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
134	133	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
135	132, 134	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
136	131, 135	sseldd 3930	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
137		fzofzp1 13659	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
138	137	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
139	132, 138	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
140	131, 139	sseldd 3930	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
141		fdv	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ)
142		fourierdlem80.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
143	142	feq2i 6638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ ↔ (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
144	141, 143	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
145	142	reseq2i 5920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ↾ 𝐼) = (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
146	145	oveq2i 7352	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ D (𝐹 ↾ 𝐼)) = (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))
147	146	feq1i 6637	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ ↔ (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
148	144, 147	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
149	100	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ (-π[,]π))
150	70, 149	sstrd 3940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
151	108	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ (𝐴[,]𝐵))
152	70, 151	ssneldd 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
153	88	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
154	129, 130, 136, 140, 148, 150, 152, 153, 66	fourierdlem57 46201	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (cos‘(𝑠 / 2))))
155	154	simpli 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
156	155	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ)
157		fdm 6655	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
158	156, 157	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
159	128, 158	eqtr2d 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
160		resss 5945	. . . . . . . . . . . . . . 15 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂)
161		dmss 5837	. . . . . . . . . . . . . . 15 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
162	160, 161	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
163	159, 162	eqsstrd 3964	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
164	163	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
165		simp3 1138	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
166	164, 165	sseldd 3930	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ dom (ℝ D 𝑂))
167	65, 166	ffvelcdmd 7013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
168	167	3exp 1119	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
169	168	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
170	63, 64, 169	rexlimd 3239	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ))
171	57, 170	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
172	50, 171	jaodan 959	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
173	28, 45, 172	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
174	173	abscld 15341	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
175	27, 174	sylan2 593	. 2 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
176		id 22	. . . 4 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
177	176, 15	eleqtrdi 2841	. . 3 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
178		elsni 4588	. . . . . 6 ⊢ (𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
179		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
180		fzfid 13875	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
181		rnffi 45212	. . . . . . . . . . 11 ⊢ ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ Fin) → ran 𝑆 ∈ Fin)
182	34, 180, 181	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑆 ∈ Fin)
183		infi 9149	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ Fin → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
184	182, 183	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
185	184	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
186	179, 185	eqeltrd 2831	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 ∈ Fin)
187		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑠𝜑
188		nfcv 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑠ran 𝑆
189		nfcv 2894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠ℝ
190		nfcv 2894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠 D
191		nfmpt1 5185	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
192	1, 191	nfcxfr 2892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠𝑂
193	189, 190, 192	nfov 7371	. . . . . . . . . . . 12 ⊢ Ⅎ𝑠(ℝ D 𝑂)
194	193	nfdm 5886	. . . . . . . . . . 11 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
195	188, 194	nfin 4169	. . . . . . . . . 10 ⊢ Ⅎ𝑠(ran 𝑆 ∩ dom (ℝ D 𝑂))
196	195	nfeq2 2912	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))
197	187, 196	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑠(𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
198		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ 𝑟)
199		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
200	198, 199	eleqtrd 2833	. . . . . . . . . . . 12 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
201	200, 48	syl 17	. . . . . . . . . . 11 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
202	201	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
203	46	ffvelcdmi 7011	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
204	203	abscld 15341	. . . . . . . . . 10 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
205	202, 204	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
206	205	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (𝑠 ∈ 𝑟 → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ))
207	197, 206	ralrimi 3230	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
208		fimaxre3 12063	. . . . . . 7 ⊢ ((𝑟 ∈ Fin ∧ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
209	186, 207, 208	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
210	178, 209	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
211	210	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
212		simpll 766	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝜑)
213		elunnel1 4099	. . . . . 6 ⊢ ((𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
214	213	adantll 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
215		vex 3440	. . . . . . . . 9 ⊢ 𝑟 ∈ V
216	18	elrnmpt 5893	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
217	215, 216	ax-mp 5	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
218	217	biimpi 216	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
219	218	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
220	60	nfcri 2886	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
221	58, 220	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
222		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑗∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦
223		fourierdlem80.fbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
224		fourierdlem80.fdvbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
225		reeanv 3204	. . . . . . . . . . . . 13 ⊢ (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) ↔ (∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
226	223, 224, 225	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
227		simp1 1136	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
228		simp2l 1200	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑤 ∈ ℝ)
229		simp2r 1201	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑧 ∈ ℝ)
230	227, 228, 229	jca31 514	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ))
231		simp3l 1202	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
232		simp3r 1203	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
233	230, 231, 232	jca31 514	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
234		fourierdlem80.ch	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
235	233, 234	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝜒)
236	234	biimpi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
237		simp-5l 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝜑)
238	236, 237	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝜑)
239	238, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
240	238, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑋 ∈ ℝ)
241		simp-4l 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
242	236, 241	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
243	242, 136	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
244	242, 140	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
245		fourierdlem80.slt	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
246	242, 245	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
247	69, 149	sstrd 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
248	242, 247	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
249	69, 151	ssneldd 3932	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
250	242, 249	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
251	242, 148	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
252		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑤 ∈ ℝ)
253	236, 252	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑤 ∈ ℝ)
254	236	simplrd 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
255		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
256	255, 142	eleqtrrdi 2842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ 𝐼)
257		rspa 3221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ 𝑡 ∈ 𝐼) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
258	254, 256, 257	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
259		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑧 ∈ ℝ)
260	236, 259	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ)
261	146	fveq1i 6818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D (𝐹 ↾ 𝐼))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)
262	261	fveq2i 6820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡))
263	236	simprd 495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
264	263	r19.21bi 3224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
265	262, 264	eqbrtrrid 5122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
266	256, 265	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
267	238, 88	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐶 ∈ ℝ)
268	239, 240, 243, 244, 246, 248, 250, 251, 253, 258, 260, 266, 267, 66	fourierdlem68 46212	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
269	268	simprd 495	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
270	268	simpld 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
271	270	raleqdv 3292	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
272	271	rexbidv 3156	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
273	269, 272	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
274	123	eqcomi 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
275	274	reseq2i 5920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
276	275	fveq1i 6818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠)
277		fvres 6836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
278	277	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
279	242, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
280	279	resmptd 5984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
281	67, 280	eqtrid 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
282	66, 281	eqtr4id 2785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
283	282	oveq2d 7357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
284	283	fveq1d 6819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D 𝑌)‘𝑠) = ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
285	122	fveq1d 6819	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
286	238, 285	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
287	284, 286	eqtr2d 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
288	287	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
289	276, 278, 288	3eqtr3a 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) = ((ℝ D 𝑌)‘𝑠))
290	289	fveq2d 6821	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D 𝑌)‘𝑠)))
291	290	breq1d 5096	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ (abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
292	291	ralbidva 3153	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
293	292	rexbidv 3156	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
294	273, 293	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
295	235, 294	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
296	295	3exp 1119	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
297	296	rexlimdvv 3188	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
298	226, 297	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
299	298	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
300		raleq 3289	. . . . . . . . . . . 12 ⊢ (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
301	300	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
302	301	rexbidv 3156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
303	299, 302	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
304	303	3exp 1119	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
305	304	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
306	221, 222, 305	rexlimd 3239	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
307	219, 306	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
308	212, 214, 307	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
309	211, 308	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
310	177, 309	sylan2 593	. 2 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
311		pm3.22 459	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
312		elin 3913	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ↔ (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
313	311, 312	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
314	313	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
315	41	eqcomd 2737	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
316	315	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
317	314, 316	eleqtrd 2833	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
318	317	orcd 873	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
319		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝜑)
320	75	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → ℝ ⊆ ℂ)
321	116	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑂:(𝐴[,]𝐵)⟶ℂ)
322	81	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐴 ∈ ℝ)
323	82	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐵 ∈ ℝ)
324	322, 323	iccssred 13329	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝐴[,]𝐵) ⊆ ℝ)
325	320, 321, 324	dvbss 25824	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → dom (ℝ D 𝑂) ⊆ (𝐴[,]𝐵))
326		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ dom (ℝ D 𝑂))
327	325, 326	sseldd 3930	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (𝐴[,]𝐵))
328	327	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (𝐴[,]𝐵))
329		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ¬ 𝑟 ∈ ran 𝑆)
330		fourierdlem80.relioo	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
331		fveq2 6817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘𝑗) = (𝑆‘𝑘))
332		oveq1 7348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
333	332	fveq2d 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝑘 + 1)))
334	331, 333	oveq12d 7359	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
335		ovex 7374	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))) ∈ V
336	334, 18, 335	fvmpt 6924	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
337	336	eleq2d 2817	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ 𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1)))))
338	337	rexbiia 3077	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
339	330, 338	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
340	51, 18	dmmpti 6620	. . . . . . . . . . . . 13 ⊢ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (0..^𝑁)
341	340	rexeqi 3291	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
342	339, 341	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
343	319, 328, 329, 342	syl21anc 837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
344		funmpt 6514	. . . . . . . . . . 11 ⊢ Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
345		elunirn 7180	. . . . . . . . . . 11 ⊢ (Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
346	344, 345	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
347	343, 346	mpbird 257	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
348	347	olcd 874	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
349	318, 348	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
350		elun 4098	. . . . . . 7 ⊢ (𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
351	349, 350	sylibr 234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
352	351, 29	eleqtrrdi 2842	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
353	352	ralrimiva 3124	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
354		dfss3 3918	. . . 4 ⊢ (dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
355	353, 354	sylibr 234	. . 3 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
356	355, 26	sseqtrrdi 3971	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
357	24, 175, 310, 356	ssfiunibd 45350	1 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 Vcvv 3436 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 {csn 4571 ∪ cuni 4854 ∪ ciun 4936 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5611 ran crn 5612 ↾ cres 5613 Fun wfun 6470 ⟶wf 6472 ‘cfv 6476 (class class class)co 7341 Fincfn 8864 ℂcc 10999 ℝcr 11000 0cc0 11001 1c1 11002 + caddc 11004 · cmul 11006 < clt 11141 ≤ cle 11142 − cmin 11339 -cneg 11340 / cdiv 11769 2c2 12175 (,)cioo 13240 [,]cicc 13243 ...cfz 13402 ..^cfzo 13549 ↑cexp 13963 abscabs 15136 sincsin 15965 cosccos 15966 πcpi 15968 TopOpenctopn 17320 topGenctg 17336 ℂ_fldccnfld 21286 intcnt 22927 D cdv 25786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079 ax-addf 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-er 8617 df-map 8747 df-pm 8748 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-fi 9290 df-sup 9321 df-inf 9322 df-oi 9391 df-card 9827 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-z 12464 df-dec 12584 df-uz 12728 df-q 12842 df-rp 12886 df-xneg 13006 df-xadd 13007 df-xmul 13008 df-ioo 13244 df-ioc 13245 df-ico 13246 df-icc 13247 df-fz 13403 df-fzo 13550 df-fl 13691 df-mod 13769 df-seq 13904 df-exp 13964 df-fac 14176 df-bc 14205 df-hash 14233 df-shft 14969 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-limsup 15373 df-clim 15390 df-rlim 15391 df-sum 15589 df-ef 15969 df-sin 15971 df-cos 15972 df-pi 15974 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-mulr 17170 df-starv 17171 df-sca 17172 df-vsca 17173 df-ip 17174 df-tset 17175 df-ple 17176 df-ds 17178 df-unif 17179 df-hom 17180 df-cco 17181 df-rest 17321 df-topn 17322 df-0g 17340 df-gsum 17341 df-topgen 17342 df-pt 17343 df-prds 17346 df-xrs 17401 df-qtop 17406 df-imas 17407 df-xps 17409 df-mre 17483 df-mrc 17484 df-acs 17486 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19224 df-cmn 19689 df-psmet 21278 df-xmet 21279 df-met 21280 df-bl 21281 df-mopn 21282 df-fbas 21283 df-fg 21284 df-cnfld 21287 df-top 22804 df-topon 22821 df-topsp 22843 df-bases 22856 df-cld 22929 df-ntr 22930 df-cls 22931 df-nei 23008 df-lp 23046 df-perf 23047 df-cn 23137 df-cnp 23138 df-t1 23224 df-haus 23225 df-cmp 23297 df-tx 23472 df-hmeo 23665 df-fil 23756 df-fm 23848 df-flim 23849 df-flf 23850 df-xms 24230 df-ms 24231 df-tms 24232 df-cncf 24793 df-limc 25789 df-dv 25790

This theorem is referenced by: fourierdlem103 46247 fourierdlem104 46248

W3C validator