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 46157

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 7377	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
3	2	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
4	3	oveq1d 7384	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) = ((𝐹‘(𝑋 + 𝑡)) − 𝐶))
5		oveq1 7376	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑠 / 2) = (𝑡 / 2))
6	5	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (sin‘(𝑠 / 2)) = (sin‘(𝑡 / 2)))
7	6	oveq2d 7385	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (2 · (sin‘(𝑠 / 2))) = (2 · (sin‘(𝑡 / 2))))
8	4, 7	oveq12d 7387	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) = (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
9	8	cbvmptv 5206	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
10	1, 9	eqtr2i 2753	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))) = 𝑂
11	10	oveq2i 7380	. . . . . . 7 ⊢ (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = (ℝ D 𝑂)
12	11	dmeqi 5858	. . . . . 6 ⊢ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = dom (ℝ D 𝑂)
13	12	ineq2i 4176	. . . . 5 ⊢ (ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))))) = (ran 𝑆 ∩ dom (ℝ D 𝑂))
14	13	sneqi 4596	. . . 4 ⊢ {(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} = {(ran 𝑆 ∩ dom (ℝ D 𝑂))}
15	14	uneq1i 4123	. . 3 ⊢ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
16		snfi 8991	. . . . 5 ⊢ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin
17		fzofi 13915	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
18		eqid 2729	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
19	18	rnmptfi 45138	. . . . . 6 ⊢ ((0..^𝑁) ∈ Fin → ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin)
20	17, 19	ax-mp 5	. . . . 5 ⊢ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin
21		unfi 9112	. . . . 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 2832	. 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 4879	. . . 4 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
27	25, 26	eleqtrdi 2838	. . 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 4890	. . . . . . . . 9 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
30	29	eleq2i 2820	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ 𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
31		elun 4112	. . . . . . . 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 7402	. . . . . . . . . . . 12 ⊢ (0...𝑁) ∈ V
36	35	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ V)
37	34, 36	fexd 7183	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
38		rnexg 7858	. . . . . . . . . 10 ⊢ (𝑆 ∈ V → ran 𝑆 ∈ V)
39		inex1g 5269	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ V → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
40		unisng 4885	. . . . . . . . . 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 2814	. . . . . . . 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 25784	. . . . . . . . 9 ⊢ (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ
47	46	a1i 11	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
48		elinel2 4161	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → 𝑠 ∈ dom (ℝ D 𝑂))
49	47, 48	ffvelcdmd 7039	. . . . . . 7 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
50	49	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
51		ovex 7402	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∈ V
52	51	dfiun3 5922	. . . . . . . . . . 11 ⊢ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
53	52	eleq2i 2820	. . . . . . . . . 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 4955	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
57	55, 56	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
58		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
59		nfmpt1 5201	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
60	59	nfrn 5905	. . . . . . . . . . 11 ⊢ Ⅎ𝑗ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
61	60	nfuni 4874	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
62	61	nfcri 2883	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
63	58, 62	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
64		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑗((ℝ D 𝑂)‘𝑠) ∈ ℂ
65	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
66		fourierdlem80.y	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
67	1	reseq1i 5935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
68		ioossicc 13370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
69		fourierdlem80.sjss	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
70	68, 69	sstrid 3955	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
71	70	resmptd 6000	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
72	67, 71	eqtrid 2776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
73	66, 72	eqtr4id 2783	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
74	73	oveq2d 7385	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
75		ax-resscn 11101	. . . . . . . . . . . . . . . . . . . . 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 13371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
84	83	sselda 3943	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
85	80, 84	readdcld 11179	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
86	78, 85	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
87	86	recnd 11178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
88		fourierdlem80.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ∈ ℝ)
89	88	recnd 11178	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℂ)
90	89	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)
91	87, 90	subcld 11509	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
92		2cnd 12240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
93	83, 76	sstrd 3954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
94	93	sselda 3943	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℂ)
95	94	halfcld 12403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑠 / 2) ∈ ℂ)
96	95	sincld 16074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
97	92, 96	mulcld 11170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
98		2ne0 12266	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ≠ 0
99	98	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
100		fourierdlem80.ab	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
101	100	sselda 3943	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (-π[,]π))
102		eqcom 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2828	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
112		fourierdlem44 46122	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
113	101, 111, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
114	92, 96, 99, 113	mulne0d 11806	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
115	91, 97, 114	divcld 11934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
116	115, 1	fmptd 7068	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑂:(𝐴[,]𝐵)⟶ℂ)
117		ioossre 13344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
119		eqid 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
120		tgioo4 24669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
121	119, 120	dvres 25788	. . . . . . . . . . . . . . . . . . . 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 45482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))
124	123	reseq2i 5936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
125	122, 124	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
126	125	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
127	74, 126	eqtr2d 2765	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (ℝ D 𝑌))
128	127	dmeqd 5859	. . . . . . . . . . . . . . 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 13612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
134	133	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
135	132, 134	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
136	131, 135	sseldd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
137		fzofzp1 13701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
138	137	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
139	132, 138	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
140	131, 139	sseldd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
141		fdv	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ)
142		fourierdlem80.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
143	142	feq2i 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ ↔ (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
144	141, 143	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
145	142	reseq2i 5936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ↾ 𝐼) = (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
146	145	oveq2i 7380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ D (𝐹 ↾ 𝐼)) = (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))
147	146	feq1i 6661	. . . . . . . . . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
151	108	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ (𝐴[,]𝐵))
152	70, 151	ssneldd 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
153	88	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
154	129, 130, 136, 140, 148, 150, 152, 153, 66	fourierdlem57 46134	. . . . . . . . . . . . . . . . . 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 6679	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
158	156, 157	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
159	128, 158	eqtr2d 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
160		resss 5961	. . . . . . . . . . . . . . 15 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂)
161		dmss 5856	. . . . . . . . . . . . . . 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 3978	. . . . . . . . . . . . 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 3944	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ dom (ℝ D 𝑂))
167	65, 166	ffvelcdmd 7039	. . . . . . . . . 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 3242	. . . . . . 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 15381	. . 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 2838	. . 3 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
178		elsni 4602	. . . . . 6 ⊢ (𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
179		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
180		fzfid 13914	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
181		rnffi 45142	. . . . . . . . . . 11 ⊢ ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ Fin) → ran 𝑆 ∈ Fin)
182	34, 180, 181	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑆 ∈ Fin)
183		infi 9189	. . . . . . . . . 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 2828	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 ∈ Fin)
187		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑠𝜑
188		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑠ran 𝑆
189		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠ℝ
190		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠 D
191		nfmpt1 5201	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
192	1, 191	nfcxfr 2889	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠𝑂
193	189, 190, 192	nfov 7399	. . . . . . . . . . . 12 ⊢ Ⅎ𝑠(ℝ D 𝑂)
194	193	nfdm 5904	. . . . . . . . . . 11 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
195	188, 194	nfin 4183	. . . . . . . . . 10 ⊢ Ⅎ𝑠(ran 𝑆 ∩ dom (ℝ D 𝑂))
196	195	nfeq2 2909	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))
197	187, 196	nfan 1899	. . . . . . . 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 2830	. . . . . . . . . . . 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 7037	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
204	203	abscld 15381	. . . . . . . . . 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 3233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
208		fimaxre3 12105	. . . . . . 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 4113	. . . . . 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 3448	. . . . . . . . 9 ⊢ 𝑟 ∈ V
216	18	elrnmpt 5911	. . . . . . . . 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 2883	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
221	58, 220	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
222		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑗∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦
223		fourierdlem80.fbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
224		fourierdlem80.fdvbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
225		reeanv 3207	. . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
248	242, 247	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
249	69, 151	ssneldd 3946	. . . . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ 𝐼)
257		rspa 3224	. . . . . . . . . . . . . . . . . . . 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 6841	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D (𝐹 ↾ 𝐼))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)
262	261	fveq2i 6843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡))
263	236	simprd 495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
264	263	r19.21bi 3227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
265	262, 264	eqbrtrrid 5138	. . . . . . . . . . . . . . . . . . . 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 46145	. . . . . . . . . . . . . . . . . 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 3296	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
272	271	rexbidv 3157	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
273	269, 272	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
274	123	eqcomi 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
275	274	reseq2i 5936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
276	275	fveq1i 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠)
277		fvres 6859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
278	277	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
279	242, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
280	279	resmptd 6000	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
281	67, 280	eqtrid 2776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
282	66, 281	eqtr4id 2783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
283	282	oveq2d 7385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
284	283	fveq1d 6842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D 𝑌)‘𝑠) = ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
285	122	fveq1d 6842	. . . . . . . . . . . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
288	287	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
289	276, 278, 288	3eqtr3a 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) = ((ℝ D 𝑌)‘𝑠))
290	289	fveq2d 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D 𝑌)‘𝑠)))
291	290	breq1d 5112	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ (abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
292	291	ralbidva 3154	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
293	292	rexbidv 3157	. . . . . . . . . . . . . . . 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 3191	. . . . . . . . . . . 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 3293	. . . . . . . . . . . 12 ⊢ (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
301	300	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
302	301	rexbidv 3157	. . . . . . . . . 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 3242	. . . . . 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 3927	. . . . . . . . . . . 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 2735	. . . . . . . . . . 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 2830	. . . . . . . . 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 13371	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝐴[,]𝐵) ⊆ ℝ)
325	320, 321, 324	dvbss 25778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → dom (ℝ D 𝑂) ⊆ (𝐴[,]𝐵))
326		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ dom (ℝ D 𝑂))
327	325, 326	sseldd 3944	. . . . . . . . . . . 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 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘𝑗) = (𝑆‘𝑘))
332		oveq1 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
333	332	fveq2d 6844	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝑘 + 1)))
334	331, 333	oveq12d 7387	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
335		ovex 7402	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))) ∈ V
336	334, 18, 335	fvmpt 6950	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
337	336	eleq2d 2814	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ 𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1)))))
338	337	rexbiia 3074	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
339	330, 338	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
340	51, 18	dmmpti 6644	. . . . . . . . . . . . 13 ⊢ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (0..^𝑁)
341	340	rexeqi 3295	. . . . . . . . . . . 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 6538	. . . . . . . . . . 11 ⊢ Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
345		elunirn 7207	. . . . . . . . . . 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 4112	. . . . . . 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 2839	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
353	352	ralrimiva 3125	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
354		dfss3 3932	. . . 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 3985	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
357	24, 175, 310, 356	ssfiunibd 45280	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 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 Vcvv 3444 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 {csn 4585 ∪ cuni 4867 ∪ ciun 4951 class class class wbr 5102 ↦ cmpt 5183 dom cdm 5631 ran crn 5632 ↾ cres 5633 Fun wfun 6493 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 Fincfn 8895 ℂcc 11042 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 · cmul 11049 < clt 11184 ≤ cle 11185 − cmin 11381 -cneg 11382 / cdiv 11811 2c2 12217 (,)cioo 13282 [,]cicc 13285 ...cfz 13444 ..^cfzo 13591 ↑cexp 14002 abscabs 15176 sincsin 16005 cosccos 16006 πcpi 16008 TopOpenctopn 17360 topGenctg 17376 ℂ_fldccnfld 21240 intcnt 22880 D cdv 25740

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 ax-addf 11123

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-supp 8117 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-pm 8779 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9289 df-fi 9338 df-sup 9369 df-inf 9370 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-z 12506 df-dec 12626 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ioc 13287 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-fl 13730 df-mod 13808 df-seq 13943 df-exp 14003 df-fac 14215 df-bc 14244 df-hash 14272 df-shft 15009 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-limsup 15413 df-clim 15430 df-rlim 15431 df-sum 15629 df-ef 16009 df-sin 16011 df-cos 16012 df-pi 16014 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-sca 17212 df-vsca 17213 df-ip 17214 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-hom 17220 df-cco 17221 df-rest 17361 df-topn 17362 df-0g 17380 df-gsum 17381 df-topgen 17382 df-pt 17383 df-prds 17386 df-xrs 17441 df-qtop 17446 df-imas 17447 df-xps 17449 df-mre 17523 df-mrc 17524 df-acs 17526 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19225 df-cmn 19688 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-fbas 21237 df-fg 21238 df-cnfld 21241 df-top 22757 df-topon 22774 df-topsp 22796 df-bases 22809 df-cld 22882 df-ntr 22883 df-cls 22884 df-nei 22961 df-lp 22999 df-perf 23000 df-cn 23090 df-cnp 23091 df-t1 23177 df-haus 23178 df-cmp 23250 df-tx 23425 df-hmeo 23618 df-fil 23709 df-fm 23801 df-flim 23802 df-flf 23803 df-xms 24184 df-ms 24185 df-tms 24186 df-cncf 24747 df-limc 25743 df-dv 25744

This theorem is referenced by: fourierdlem103 46180 fourierdlem104 46181

W3C validator