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 43727

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 7283	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
3	2	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
4	3	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) = ((𝐹‘(𝑋 + 𝑡)) − 𝐶))
5		oveq1 7282	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑠 / 2) = (𝑡 / 2))
6	5	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (sin‘(𝑠 / 2)) = (sin‘(𝑡 / 2)))
7	6	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (2 · (sin‘(𝑠 / 2))) = (2 · (sin‘(𝑡 / 2))))
8	4, 7	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) = (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
9	8	cbvmptv 5187	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
10	1, 9	eqtr2i 2767	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))) = 𝑂
11	10	oveq2i 7286	. . . . . . 7 ⊢ (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = (ℝ D 𝑂)
12	11	dmeqi 5813	. . . . . 6 ⊢ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = dom (ℝ D 𝑂)
13	12	ineq2i 4143	. . . . 5 ⊢ (ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))))) = (ran 𝑆 ∩ dom (ℝ D 𝑂))
14	13	sneqi 4572	. . . 4 ⊢ {(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} = {(ran 𝑆 ∩ dom (ℝ D 𝑂))}
15	14	uneq1i 4093	. . 3 ⊢ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
16		snfi 8834	. . . . 5 ⊢ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin
17		fzofi 13694	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
18		eqid 2738	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
19	18	rnmptfi 42707	. . . . . 6 ⊢ ((0..^𝑁) ∈ Fin → ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin)
20	17, 19	ax-mp 5	. . . . 5 ⊢ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin
21		unfi 8955	. . . . 5 ⊢ (({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin ∧ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin) → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
22	16, 20, 21	mp2an 689	. . . 4 ⊢ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin
23	22	a1i 11	. . 3 ⊢ (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
24	15, 23	eqeltrid 2843	. 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 4852	. . . 4 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
27	25, 26	eleqtrdi 2849	. . 3 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
28		simpl 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → 𝜑)
29		uniun 4864	. . . . . . . . 9 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
30	29	eleq2i 2830	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ 𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
31		elun 4083	. . . . . . . 8 ⊢ (𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
32	30, 31	sylbb 218	. . . . . . 7 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
33	32	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
34		fourierdlem80.sf	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
35		ovex 7308	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ∈ V
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑁) ∈ V)
37	34, 36	fexd 7103	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ V)
38		rnexg 7751	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ran 𝑆 ∈ V)
39	37, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑆 ∈ V)
40		inex1g 5243	. . . . . . . . . . 11 ⊢ (ran 𝑆 ∈ V → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
41	39, 40	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
42		unisng 4860	. . . . . . . . . 10 ⊢ ((ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V → ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
43	41, 42	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
44	43	eleq2d 2824	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
45	44	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
46	45	orbi1d 914	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))))
47	33, 46	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
48		dvf 25071	. . . . . . . . 9 ⊢ (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ
49	48	a1i 11	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
50		elinel2 4130	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → 𝑠 ∈ dom (ℝ D 𝑂))
51	49, 50	ffvelrnd 6962	. . . . . . 7 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
52	51	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
53		ovex 7308	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∈ V
54	53	dfiun3 5875	. . . . . . . . . . 11 ⊢ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
55	54	eleq2i 2830	. . . . . . . . . 10 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
56	55	biimpri 227	. . . . . . . . 9 ⊢ (𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
57	56	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
58		eliun 4928	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
59	57, 58	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
60		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
61		nfmpt1 5182	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
62	61	nfrn 5861	. . . . . . . . . . 11 ⊢ Ⅎ𝑗ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
63	62	nfuni 4846	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
64	63	nfcri 2894	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
65	60, 64	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
66		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑗((ℝ D 𝑂)‘𝑠) ∈ ℂ
67	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
68		fourierdlem80.y	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
69	1	reseq1i 5887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
70		ioossicc 13165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
71		fourierdlem80.sjss	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
72	70, 71	sstrid 3932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
73	72	resmptd 5948	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
74	69, 73	eqtrid 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
75	68, 74	eqtr4id 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
76	75	oveq2d 7291	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
77		ax-resscn 10928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ℝ ⊆ ℂ)
79		fourierdlem80.f	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
80	79	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
81		fourierdlem80.xre	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ ℝ)
82	81	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
83		fourierdlem80.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ ℝ)
84		fourierdlem80.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ℝ)
85	83, 84	iccssred 13166	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
86	85	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
87	82, 86	readdcld 11004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
88	80, 87	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
89	88	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
90		fourierdlem80.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ∈ ℝ)
91	90	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℂ)
92	91	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)
93	89, 92	subcld 11332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
94		2cnd 12051	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
95	85, 78	sstrd 3931	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
96	95	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℂ)
97	96	halfcld 12218	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑠 / 2) ∈ ℂ)
98	97	sincld 15839	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
99	94, 98	mulcld 10995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
100		2ne0 12077	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ≠ 0
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
102		fourierdlem80.ab	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
103	102	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (-π[,]π))
104		eqcom 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
105	104	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 0 → 0 = 𝑠)
106	105	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
107		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴[,]𝐵))
108	106, 107	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
109	108	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
110		fourierdlem80.n0	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
111	110	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
112	109, 111	pm2.65da 814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ¬ 𝑠 = 0)
113	112	neqned 2950	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
114		fourierdlem44 43692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
115	103, 113, 114	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
116	94, 98, 101, 115	mulne0d 11627	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
117	93, 99, 116	divcld 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
118	117, 1	fmptd 6988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑂:(𝐴[,]𝐵)⟶ℂ)
119		ioossre 13140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
120	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
121		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
122	121	tgioo2 23966	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
123	121, 122	dvres 25075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℝ ⊆ ℂ ∧ 𝑂:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
124	78, 118, 85, 120, 123	syl22anc 836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
125		ioontr 43049	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))
126	125	reseq2i 5888	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
127	124, 126	eqtrdi 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
128	127	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
129	76, 128	eqtr2d 2779	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (ℝ D 𝑌))
130	129	dmeqd 5814	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = dom (ℝ D 𝑌))
131	79	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℝ)
132	81	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑋 ∈ ℝ)
133	85	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
134	34	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
135		elfzofz 13403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
136	135	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
137	134, 136	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
138	133, 137	sseldd 3922	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
139		fzofzp1 13484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
140	139	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
141	134, 140	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
142	133, 141	sseldd 3922	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
143		fdv	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ)
144		fourierdlem80.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
145	144	feq2i 6592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ ↔ (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
146	143, 145	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
147	144	reseq2i 5888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ↾ 𝐼) = (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
148	147	oveq2i 7286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ D (𝐹 ↾ 𝐼)) = (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))
149	148	feq1i 6591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ ↔ (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
150	146, 149	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
151	102	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ (-π[,]π))
152	72, 151	sstrd 3931	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
153	110	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ (𝐴[,]𝐵))
154	72, 153	ssneldd 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
155	90	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
156	131, 132, 138, 142, 150, 152, 154, 155, 68	fourierdlem57 43704	. . . . . . . . . . . . . . . . . 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))))
157	156	simpli 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
158	157	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ)
159		fdm 6609	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
160	158, 159	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
161	130, 160	eqtr2d 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
162		resss 5916	. . . . . . . . . . . . . . 15 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂)
163		dmss 5811	. . . . . . . . . . . . . . 15 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
164	162, 163	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
165	161, 164	eqsstrd 3959	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
166	165	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
167		simp3 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
168	166, 167	sseldd 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ dom (ℝ D 𝑂))
169	67, 168	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
170	169	3exp 1118	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
171	170	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
172	65, 66, 171	rexlimd 3250	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ))
173	59, 172	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
174	52, 173	jaodan 955	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
175	28, 47, 174	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
176	175	abscld 15148	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
177	27, 176	sylan2 593	. 2 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
178		id 22	. . . 4 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
179	178, 15	eleqtrdi 2849	. . 3 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
180		elsni 4578	. . . . . 6 ⊢ (𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
181		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
182		fzfid 13693	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
183		rnffi 42711	. . . . . . . . . . 11 ⊢ ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ Fin) → ran 𝑆 ∈ Fin)
184	34, 182, 183	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑆 ∈ Fin)
185		infi 9043	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ Fin → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
186	184, 185	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
187	186	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
188	181, 187	eqeltrd 2839	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 ∈ Fin)
189		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑠𝜑
190		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎ𝑠ran 𝑆
191		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠ℝ
192		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠 D
193		nfmpt1 5182	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
194	1, 193	nfcxfr 2905	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠𝑂
195	191, 192, 194	nfov 7305	. . . . . . . . . . . 12 ⊢ Ⅎ𝑠(ℝ D 𝑂)
196	195	nfdm 5860	. . . . . . . . . . 11 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
197	190, 196	nfin 4150	. . . . . . . . . 10 ⊢ Ⅎ𝑠(ran 𝑆 ∩ dom (ℝ D 𝑂))
198	197	nfeq2 2924	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))
199	189, 198	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑠(𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
200		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ 𝑟)
201		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
202	200, 201	eleqtrd 2841	. . . . . . . . . . . 12 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
203	202, 50	syl 17	. . . . . . . . . . 11 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
204	203	adantll 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
205	48	ffvelrni 6960	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
206	205	abscld 15148	. . . . . . . . . 10 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
207	204, 206	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
208	207	ex 413	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (𝑠 ∈ 𝑟 → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ))
209	199, 208	ralrimi 3141	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
210		fimaxre3 11921	. . . . . . 7 ⊢ ((𝑟 ∈ Fin ∧ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
211	188, 209, 210	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
212	180, 211	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
213	212	adantlr 712	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
214		simpll 764	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝜑)
215		elunnel1 4084	. . . . . 6 ⊢ ((𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
216	215	adantll 711	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
217		vex 3436	. . . . . . . . 9 ⊢ 𝑟 ∈ V
218	18	elrnmpt 5865	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
219	217, 218	ax-mp 5	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
220	219	biimpi 215	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
221	220	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
222	62	nfcri 2894	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
223	60, 222	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
224		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑗∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦
225		fourierdlem80.fbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
226		fourierdlem80.fdvbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
227		reeanv 3294	. . . . . . . . . . . . 13 ⊢ (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) ↔ (∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
228	225, 226, 227	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
229		simp1 1135	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
230		simp2l 1198	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑤 ∈ ℝ)
231		simp2r 1199	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑧 ∈ ℝ)
232	229, 230, 231	jca31 515	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ))
233		simp3l 1200	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
234		simp3r 1201	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
235	232, 233, 234	jca31 515	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
236		fourierdlem80.ch	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
237	235, 236	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝜒)
238	236	biimpi 215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
239		simp-5l 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝜑)
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝜑)
241	240, 79	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
242	240, 81	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑋 ∈ ℝ)
243		simp-4l 780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
244	238, 243	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
245	244, 138	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
246	244, 142	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
247		fourierdlem80.slt	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
248	244, 247	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
249	71, 151	sstrd 3931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
250	244, 249	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
251	71, 153	ssneldd 3924	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
252	244, 251	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
253	244, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
254		simp-4r 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑤 ∈ ℝ)
255	238, 254	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑤 ∈ ℝ)
256	238	simplrd 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
257		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
258	257, 144	eleqtrrdi 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ 𝐼)
259		rspa 3132	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ 𝑡 ∈ 𝐼) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
260	256, 258, 259	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
261		simpllr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑧 ∈ ℝ)
262	238, 261	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ)
263	148	fveq1i 6775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D (𝐹 ↾ 𝐼))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)
264	263	fveq2i 6777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡))
265	238	simprd 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
266	265	r19.21bi 3134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
267	264, 266	eqbrtrrid 5110	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
268	258, 267	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
269	240, 90	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐶 ∈ ℝ)
270	241, 242, 245, 246, 248, 250, 252, 253, 255, 260, 262, 268, 269, 68	fourierdlem68 43715	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
271	270	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
272	270	simpld 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
273	272	raleqdv 3348	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
274	273	rexbidv 3226	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
275	271, 274	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
276	125	eqcomi 2747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
277	276	reseq2i 5888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
278	277	fveq1i 6775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠)
279		fvres 6793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
280	279	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
281	244, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
282	281	resmptd 5948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
283	69, 282	eqtrid 2790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
284	68, 283	eqtr4id 2797	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
285	284	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
286	285	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D 𝑌)‘𝑠) = ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
287	124	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
288	240, 287	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
289	286, 288	eqtr2d 2779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
290	289	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
291	278, 280, 290	3eqtr3a 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) = ((ℝ D 𝑌)‘𝑠))
292	291	fveq2d 6778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D 𝑌)‘𝑠)))
293	292	breq1d 5084	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ (abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
294	293	ralbidva 3111	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
295	294	rexbidv 3226	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
296	275, 295	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
297	237, 296	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
298	297	3exp 1118	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
299	298	rexlimdvv 3222	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
300	228, 299	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
301	300	3adant3 1131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
302		raleq 3342	. . . . . . . . . . . 12 ⊢ (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
303	302	3ad2ant3 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
304	303	rexbidv 3226	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
305	301, 304	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
306	305	3exp 1118	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
307	306	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
308	223, 224, 307	rexlimd 3250	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
309	221, 308	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
310	214, 216, 309	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
311	213, 310	pm2.61dan 810	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
312	179, 311	sylan2 593	. 2 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
313		pm3.22 460	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
314		elin 3903	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ↔ (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
315	313, 314	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
316	315	adantll 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
317	43	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
318	317	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
319	316, 318	eleqtrd 2841	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
320	319	orcd 870	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
321		simpll 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝜑)
322	77	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → ℝ ⊆ ℂ)
323	118	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑂:(𝐴[,]𝐵)⟶ℂ)
324	83	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐴 ∈ ℝ)
325	84	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐵 ∈ ℝ)
326	324, 325	iccssred 13166	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝐴[,]𝐵) ⊆ ℝ)
327	322, 323, 326	dvbss 25065	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → dom (ℝ D 𝑂) ⊆ (𝐴[,]𝐵))
328		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ dom (ℝ D 𝑂))
329	327, 328	sseldd 3922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (𝐴[,]𝐵))
330	329	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (𝐴[,]𝐵))
331		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ¬ 𝑟 ∈ ran 𝑆)
332		fourierdlem80.relioo	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
333		fveq2 6774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘𝑗) = (𝑆‘𝑘))
334		oveq1 7282	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
335	334	fveq2d 6778	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝑘 + 1)))
336	333, 335	oveq12d 7293	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
337		ovex 7308	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))) ∈ V
338	336, 18, 337	fvmpt 6875	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
339	338	eleq2d 2824	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ 𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1)))))
340	339	rexbiia 3180	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
341	332, 340	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
342	53, 18	dmmpti 6577	. . . . . . . . . . . . 13 ⊢ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (0..^𝑁)
343	342	rexeqi 3347	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
344	341, 343	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
345	321, 330, 331, 344	syl21anc 835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
346		funmpt 6472	. . . . . . . . . . 11 ⊢ Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
347		elunirn 7124	. . . . . . . . . . 11 ⊢ (Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
348	346, 347	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
349	345, 348	mpbird 256	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
350	349	olcd 871	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
351	320, 350	pm2.61dan 810	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
352		elun 4083	. . . . . . 7 ⊢ (𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
353	351, 352	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
354	353, 29	eleqtrrdi 2850	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
355	354	ralrimiva 3103	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
356		dfss3 3909	. . . 4 ⊢ (dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
357	355, 356	sylibr 233	. . 3 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
358	357, 26	sseqtrrdi 3972	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
359	24, 177, 312, 358	ssfiunibd 42848	1 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 {csn 4561 ∪ cuni 4839 ∪ ciun 4924 class class class wbr 5074 ↦ cmpt 5157 dom cdm 5589 ran crn 5590 ↾ cres 5591 Fun wfun 6427 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 Fincfn 8733 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 < clt 11009 ≤ cle 11010 − cmin 11205 -cneg 11206 / cdiv 11632 2c2 12028 (,)cioo 13079 [,]cicc 13082 ...cfz 13239 ..^cfzo 13382 ↑cexp 13782 abscabs 14945 sincsin 15773 cosccos 15774 πcpi 15776 TopOpenctopn 17132 topGenctg 17148 ℂ_fldccnfld 20597 intcnt 22168 D cdv 25027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950 ax-mulf 10951

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-pm 8618 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ioc 13084 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-mod 13590 df-seq 13722 df-exp 13783 df-fac 13988 df-bc 14017 df-hash 14045 df-shft 14778 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-limsup 15180 df-clim 15197 df-rlim 15198 df-sum 15398 df-ef 15777 df-sin 15779 df-cos 15780 df-pi 15782 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-starv 16977 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-hom 16986 df-cco 16987 df-rest 17133 df-topn 17134 df-0g 17152 df-gsum 17153 df-topgen 17154 df-pt 17155 df-prds 17158 df-xrs 17213 df-qtop 17218 df-imas 17219 df-xps 17221 df-mre 17295 df-mrc 17296 df-acs 17298 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-submnd 18431 df-mulg 18701 df-cntz 18923 df-cmn 19388 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-fbas 20594 df-fg 20595 df-cnfld 20598 df-top 22043 df-topon 22060 df-topsp 22082 df-bases 22096 df-cld 22170 df-ntr 22171 df-cls 22172 df-nei 22249 df-lp 22287 df-perf 22288 df-cn 22378 df-cnp 22379 df-t1 22465 df-haus 22466 df-cmp 22538 df-tx 22713 df-hmeo 22906 df-fil 22997 df-fm 23089 df-flim 23090 df-flf 23091 df-xms 23473 df-ms 23474 df-tms 23475 df-cncf 24041 df-limc 25030 df-dv 25031

This theorem is referenced by: fourierdlem103 43750 fourierdlem104 43751

W3C validator