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 46721

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 7399	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
3	2	fveq2d 6866	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
4	3	oveq1d 7406	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) = ((𝐹‘(𝑋 + 𝑡)) − 𝐶))
5		oveq1 7398	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑠 / 2) = (𝑡 / 2))
6	5	fveq2d 6866	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (sin‘(𝑠 / 2)) = (sin‘(𝑡 / 2)))
7	6	oveq2d 7407	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (2 · (sin‘(𝑠 / 2))) = (2 · (sin‘(𝑡 / 2))))
8	4, 7	oveq12d 7409	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) = (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
9	8	cbvmptv 5201	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
10	1, 9	eqtr2i 2785	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))) = 𝑂
11	10	oveq2i 7402	. . . . . . 7 ⊢ (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = (ℝ D 𝑂)
12	11	dmeqi 5876	. . . . . 6 ⊢ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = dom (ℝ D 𝑂)
13	12	ineq2i 4167	. . . . 5 ⊢ (ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))))) = (ran 𝑆 ∩ dom (ℝ D 𝑂))
14	13	sneqi 4590	. . . 4 ⊢ {(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} = {(ran 𝑆 ∩ dom (ℝ D 𝑂))}
15	14	uneq1i 4115	. . 3 ⊢ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
16		snfi 9018	. . . . 5 ⊢ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin
17		fzofi 13981	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
18		eqid 2761	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
19	18	rnmptfi 45710	. . . . . 6 ⊢ ((0..^𝑁) ∈ Fin → ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin)
20	17, 19	ax-mp 5	. . . . 5 ⊢ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin
21		unfi 9133	. . . . 5 ⊢ (({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin ∧ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin) → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
22	16, 20, 21	mp2an 702	. . . 4 ⊢ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin
23	22	a1i 11	. . 3 ⊢ (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
24	15, 23	eqeltrid 2865	. 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 4874	. . . 4 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
27	25, 26	eleqtrdi 2871	. . 3 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
28		simpl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → 𝜑)
29		uniun 4885	. . . . . . . . 9 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
30	29	eleq2i 2853	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ 𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
31		elun 4104	. . . . . . . 8 ⊢ (𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
32	30, 31	sylbb 221	. . . . . . 7 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
33	32	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
34		fourierdlem80.sf	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
35		ovex 7424	. . . . . . . . . . . 12 ⊢ (0...𝑁) ∈ V
36	35	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ V)
37	34, 36	fexd 7206	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ V)
38		rnexg 7878	. . . . . . . . . 10 ⊢ (𝑆 ∈ V → ran 𝑆 ∈ V)
39		inex1g 5272	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ V → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
40		unisng 4880	. . . . . . . . . 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 2847	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
43	42	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
44	43	orbi1d 927	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))))
45	33, 44	mpbid 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
46		dvf 25957	. . . . . . . . 9 ⊢ (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ
47	46	a1i 11	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
48		elinel2 4152	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → 𝑠 ∈ dom (ℝ D 𝑂))
49	47, 48	ffvelcdmd 7061	. . . . . . 7 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
50	49	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
51		ovex 7424	. . . . . . . . . . 11 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∈ V
52	51	dfiun3 5942	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
53	52	eleq2i 2853	. . . . . . . . 9 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
54	53	bilanri 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
55		eliun 4950	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
56	54, 55	sylib 220	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
57		nfv 1933	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
58		nfmpt1 5196	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
59	58	nfrn 5924	. . . . . . . . . . 11 ⊢ Ⅎ𝑗ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
60	59	nfuni 4869	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
61	60	nfcri 2915	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
62	57, 61	nfan 1918	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
63		nfv 1933	. . . . . . . 8 ⊢ Ⅎ𝑗((ℝ D 𝑂)‘𝑠) ∈ ℂ
64	46	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
65		fourierdlem80.y	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
66	1	reseq1i 5957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
67		ioossicc 13431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
68		fourierdlem80.sjss	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
69	67, 68	sstrid 3945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
70	69	resmptd 6025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
71	66, 70	eqtrid 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
72	65, 71	eqtr4id 2815	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
73	72	oveq2d 7407	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
74		ax-resscn 11124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ℝ ⊆ ℂ)
76		fourierdlem80.f	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
77	76	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
78		fourierdlem80.xre	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ ℝ)
79	78	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
80		fourierdlem80.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ ℝ)
81		fourierdlem80.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ℝ)
82	80, 81	iccssred 13432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
83	82	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
84	79, 83	readdcld 11205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
85	77, 84	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
86	85	recnd 11204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
87		fourierdlem80.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ∈ ℝ)
88	87	recnd 11204	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℂ)
89	88	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)
90	86, 89	subcld 11536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
91		2cnd 12290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
92	82, 75	sstrd 3944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
93	92	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℂ)
94	93	halfcld 12460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑠 / 2) ∈ ℂ)
95	94	sincld 16153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
96	91, 95	mulcld 11196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
97		2ne0 12318	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ≠ 0
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
99		fourierdlem80.ab	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
100	99	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (-π[,]π))
101		eqcom 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
102	101	bilani 508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
103		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴[,]𝐵))
104	102, 103	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
105	104	adantll 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
106		fourierdlem80.n0	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
107	106	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
108	105, 107	pm2.65da 826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ¬ 𝑠 = 0)
109	108	neqned 2963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
110		fourierdlem44 46686	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
111	100, 109, 110	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
112	91, 95, 98, 111	mulne0d 11833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
113	90, 96, 112	divcld 11961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
114	113, 1	fmptd 7090	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑂:(𝐴[,]𝐵)⟶ℂ)
115		ioossre 13405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
117		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
118		tgioo4 24853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
119	117, 118	dvres 25961	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℝ ⊆ ℂ ∧ 𝑂:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
120	75, 114, 82, 116, 119	syl22anc 849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
121		ioontr 46048	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))
122	121	reseq2i 5958	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
123	120, 122	eqtrdi 2812	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
124	123	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
125	73, 124	eqtr2d 2797	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (ℝ D 𝑌))
126	125	dmeqd 5877	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = dom (ℝ D 𝑌))
127	76	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℝ)
128	78	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑋 ∈ ℝ)
129	82	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
130	34	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
131		elfzofz 13675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
132	131	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
133	130, 132	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
134	129, 133	sseldd 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
135		fzofzp1 13764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
136	135	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
137	130, 136	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
138	129, 137	sseldd 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
139		fdv	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ)
140		fourierdlem80.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
141	140	feq2i 6678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ ↔ (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
142	139, 141	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
143	140	reseq2i 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ↾ 𝐼) = (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
144	143	oveq2i 7402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ D (𝐹 ↾ 𝐼)) = (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))
145	144	feq1i 6677	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ ↔ (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
146	142, 145	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
147	99	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ (-π[,]π))
148	69, 147	sstrd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
149	106	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ (𝐴[,]𝐵))
150	69, 149	ssneldd 3937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
151	87	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
152	127, 128, 134, 138, 146, 148, 150, 151, 65	fourierdlem57 46698	. . . . . . . . . . . . . . . . . 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))))
153	152	simpli 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
154	153	simpld 498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ)
155		fdm 6696	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
156	154, 155	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
157	126, 156	eqtr2d 2797	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
158		resss 5983	. . . . . . . . . . . . . . 15 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂)
159		dmss 5874	. . . . . . . . . . . . . . 15 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
160	158, 159	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
161	157, 160	eqsstrd 3968	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
162	161	3adant3 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
163		simp3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
164	162, 163	sseldd 3935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ dom (ℝ D 𝑂))
165	64, 164	ffvelcdmd 7061	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
166	165	3exp 1131	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
167	166	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
168	62, 63, 167	rexlimd 3268	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ))
169	56, 168	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
170	50, 169	jaodan 970	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
171	28, 45, 170	syl2anc 593	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
172	171	abscld 15457	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
173	27, 172	sylan2 602	. 2 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
174		id 22	. . . 4 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
175	174, 15	eleqtrdi 2871	. . 3 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
176		elsni 4596	. . . . . 6 ⊢ (𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
177		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
178		fzfid 13980	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
179		rnffi 45714	. . . . . . . . . . 11 ⊢ ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ Fin) → ran 𝑆 ∈ Fin)
180	34, 178, 179	syl2anc 593	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑆 ∈ Fin)
181		infi 9208	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ Fin → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
182	180, 181	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
183	182	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
184	177, 183	eqeltrd 2861	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 ∈ Fin)
185		nfv 1933	. . . . . . . . 9 ⊢ Ⅎ𝑠𝜑
186		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑠ran 𝑆
187		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠ℝ
188		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠 D
189		nfmpt1 5196	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
190	1, 189	nfcxfr 2921	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠𝑂
191	187, 188, 190	nfov 7421	. . . . . . . . . . . 12 ⊢ Ⅎ𝑠(ℝ D 𝑂)
192	191	nfdm 5923	. . . . . . . . . . 11 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
193	186, 192	nfin 4174	. . . . . . . . . 10 ⊢ Ⅎ𝑠(ran 𝑆 ∩ dom (ℝ D 𝑂))
194	193	nfeq2 2940	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))
195	185, 194	nfan 1918	. . . . . . . 8 ⊢ Ⅎ𝑠(𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
196		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ 𝑟)
197		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
198	196, 197	eleqtrd 2863	. . . . . . . . . . . 12 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
199	198, 48	syl 17	. . . . . . . . . . 11 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
200	199	adantll 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
201	46	ffvelcdmi 7059	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
202	201	abscld 15457	. . . . . . . . . 10 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
203	200, 202	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
204	203	ex 416	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (𝑠 ∈ 𝑟 → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ))
205	195, 204	ralrimi 3259	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
206		fimaxre3 12132	. . . . . . 7 ⊢ ((𝑟 ∈ Fin ∧ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
207	184, 205, 206	syl2anc 593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
208	176, 207	sylan2 602	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
209	208	adantlr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
210		simpll 776	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝜑)
211		elunnel1 4105	. . . . . 6 ⊢ ((𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
212	211	adantll 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
213		vex 3457	. . . . . . . 8 ⊢ 𝑟 ∈ V
214	18	elrnmpt 5930	. . . . . . . 8 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
215	213, 214	ax-mp 5	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
216	215	bilani 508	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
217	59	nfcri 2915	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
218	57, 217	nfan 1918	. . . . . . 7 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
219		nfv 1933	. . . . . . 7 ⊢ Ⅎ𝑗∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦
220		fourierdlem80.fbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
221		fourierdlem80.fdvbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
222		reeanv 3233	. . . . . . . . . . . . 13 ⊢ (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) ↔ (∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
223	220, 221, 222	sylanbrc 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
224		simp1 1148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
225		simp2l 1212	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑤 ∈ ℝ)
226		simp2r 1213	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑧 ∈ ℝ)
227	224, 225, 226	jca31 522	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ))
228		simp3l 1214	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
229		simp3r 1215	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
230	227, 228, 229	jca31 522	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
231		fourierdlem80.ch	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
232	230, 231	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝜒)
233	231	biimpi 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
234		simp-5l 794	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝜑)
235	233, 234	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝜑)
236	235, 76	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
237	235, 78	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑋 ∈ ℝ)
238		simp-4l 792	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
239	233, 238	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
240	239, 134	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
241	239, 138	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
242		fourierdlem80.slt	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
243	239, 242	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
244	68, 147	sstrd 3944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
245	239, 244	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
246	68, 149	ssneldd 3937	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
247	239, 246	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
248	239, 146	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
249		simp-4r 793	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑤 ∈ ℝ)
250	233, 249	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑤 ∈ ℝ)
251	233	simplrd 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
252		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
253	252, 140	eleqtrrdi 2872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ 𝐼)
254		rspa 3250	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ 𝑡 ∈ 𝐼) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
255	251, 253, 254	syl2an 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
256		simpllr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑧 ∈ ℝ)
257	233, 256	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ)
258	144	fveq1i 6863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D (𝐹 ↾ 𝐼))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)
259	258	fveq2i 6865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡))
260	233	simprd 499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
261	260	r19.21bi 3253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
262	259, 261	eqbrtrrid 5133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
263	253, 262	sylan2 602	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
264	235, 87	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐶 ∈ ℝ)
265	236, 237, 240, 241, 243, 245, 247, 248, 250, 255, 257, 263, 264, 65	fourierdlem68 46709	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
266	265	simprd 499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
267	265	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
268	267	raleqdv 3319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
269	268	rexbidv 3185	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
270	266, 269	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
271	121	eqcomi 2770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
272	271	reseq2i 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
273	272	fveq1i 6863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠)
274		fvres 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
275	274	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
276	239, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
277	276	resmptd 6025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
278	66, 277	eqtrid 2808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
279	65, 278	eqtr4id 2815	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
280	279	oveq2d 7407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
281	280	fveq1d 6864	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D 𝑌)‘𝑠) = ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
282	120	fveq1d 6864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
283	235, 282	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
284	281, 283	eqtr2d 2797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
285	284	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
286	273, 275, 285	3eqtr3a 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) = ((ℝ D 𝑌)‘𝑠))
287	286	fveq2d 6866	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D 𝑌)‘𝑠)))
288	287	breq1d 5107	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ (abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
289	288	ralbidva 3182	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
290	289	rexbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
291	270, 290	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
292	232, 291	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
293	292	3exp 1131	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
294	293	rexlimdvv 3217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
295	223, 294	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
296	295	3adant3 1144	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
297		raleq 3316	. . . . . . . . . . . 12 ⊢ (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
298	297	3ad2ant3 1147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
299	298	rexbidv 3185	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
300	296, 299	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
301	300	3exp 1131	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
302	301	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
303	218, 219, 302	rexlimd 3268	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
304	216, 303	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
305	210, 212, 304	syl2anc 593	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
306	209, 305	pm2.61dan 822	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
307	175, 306	sylan2 602	. 2 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
308		pm3.22 463	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
309		elin 3918	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ↔ (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
310	308, 309	sylibr 236	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
311	310	adantll 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
312	41	eqcomd 2767	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
313	312	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
314	311, 313	eleqtrd 2863	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
315	314	orcd 884	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
316		simpll 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝜑)
317	74	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → ℝ ⊆ ℂ)
318	114	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑂:(𝐴[,]𝐵)⟶ℂ)
319	80	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐴 ∈ ℝ)
320	81	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐵 ∈ ℝ)
321	319, 320	iccssred 13432	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝐴[,]𝐵) ⊆ ℝ)
322	317, 318, 321	dvbss 25951	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → dom (ℝ D 𝑂) ⊆ (𝐴[,]𝐵))
323		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ dom (ℝ D 𝑂))
324	322, 323	sseldd 3935	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (𝐴[,]𝐵))
325	324	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (𝐴[,]𝐵))
326		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ¬ 𝑟 ∈ ran 𝑆)
327		fourierdlem80.relioo	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
328		fveq2 6862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘𝑗) = (𝑆‘𝑘))
329		oveq1 7398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
330	329	fveq2d 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝑘 + 1)))
331	328, 330	oveq12d 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
332		ovex 7424	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))) ∈ V
333	331, 18, 332	fvmpt 6970	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
334	333	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ 𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1)))))
335	334	rexbiia 3106	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
336	327, 335	sylibr 236	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
337	51, 18	dmmpti 6660	. . . . . . . . . . . . 13 ⊢ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (0..^𝑁)
338	337	rexeqi 3318	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
339	336, 338	sylibr 236	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
340	316, 325, 326, 339	syl21anc 848	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
341		funmpt 6554	. . . . . . . . . . 11 ⊢ Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
342		elunirn 7230	. . . . . . . . . . 11 ⊢ (Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
343	341, 342	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
344	340, 343	mpbird 259	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
345	344	olcd 885	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
346	315, 345	pm2.61dan 822	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
347		elun 4104	. . . . . . 7 ⊢ (𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
348	346, 347	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
349	348, 29	eleqtrrdi 2872	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
350	349	ralrimiva 3153	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
351		dfss3 3923	. . . 4 ⊢ (dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
352	350, 351	sylibr 236	. . 3 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
353	352, 26	sseqtrrdi 3975	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
354	24, 173, 307, 353	ssfiunibd 45849	1 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∃wrex 3085 Vcvv 3453 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 {csn 4579 ∪ cuni 4862 ∪ ciun 4946 class class class wbr 5097 ↦ cmpt 5178 dom cdm 5643 ran crn 5644 ↾ cres 5645 Fun wfun 6510 ⟶wf 6512 ‘cfv 6516 (class class class)co 7391 Fincfn 8921 ℂcc 11065 ℝcr 11066 0cc0 11067 1c1 11068 + caddc 11070 · cmul 11072 < clt 11210 ≤ cle 11211 − cmin 11408 -cneg 11409 / cdiv 11838 2c2 12266 (,)cioo 13343 [,]cicc 13346 ...cfz 13506 ..^cfzo 13653 ↑cexp 14068 abscabs 15252 sincsin 16084 cosccos 16085 πcpi 16087 TopOpenctopn 17441 topGenctg 17457 ℂ_fldccnfld 21412 intcnt 23065 D cdv 25913

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-inf2 9590 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145 ax-addf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-om 7842 df-1st 7965 df-2nd 7966 df-supp 8135 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-er 8672 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9302 df-fi 9351 df-sup 9382 df-inf 9383 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-z 12563 df-dec 12683 df-uz 12834 df-q 12944 df-rp 12988 df-xneg 13108 df-xadd 13109 df-xmul 13110 df-ioo 13347 df-ioc 13348 df-ico 13349 df-icc 13350 df-fz 13507 df-fzo 13654 df-fl 13796 df-mod 13874 df-seq 14009 df-exp 14069 df-fac 14281 df-bc 14310 df-hash 14338 df-shft 15074 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-limsup 15489 df-clim 15506 df-rlim 15507 df-sum 15705 df-ef 16088 df-sin 16090 df-cos 16091 df-pi 16093 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-starv 17292 df-sca 17293 df-vsca 17294 df-ip 17295 df-tset 17296 df-ple 17297 df-ds 17299 df-unif 17300 df-hom 17301 df-cco 17302 df-rest 17442 df-topn 17443 df-0g 17461 df-gsum 17462 df-topgen 17463 df-pt 17464 df-prds 17467 df-xrs 17523 df-qtop 17528 df-imas 17529 df-xps 17531 df-mre 17605 df-mrc 17606 df-acs 17608 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-mulg 19101 df-cntz 19348 df-cmn 19813 df-psmet 21404 df-xmet 21405 df-met 21406 df-bl 21407 df-mopn 21408 df-fbas 21409 df-fg 21410 df-cnfld 21413 df-top 22942 df-topon 22959 df-topsp 22981 df-bases 22994 df-cld 23067 df-ntr 23068 df-cls 23069 df-nei 23146 df-lp 23184 df-perf 23185 df-cn 23275 df-cnp 23276 df-t1 23362 df-haus 23363 df-cmp 23435 df-tx 23610 df-hmeo 23803 df-fil 23894 df-fm 23986 df-flim 23987 df-flf 23988 df-xms 24368 df-ms 24369 df-tms 24370 df-cncf 24928 df-limc 25916 df-dv 25917

This theorem is referenced by: fourierdlem103 46744 fourierdlem104 46745

W3C validator