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 43222

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 7163	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡))
3	2	fveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡)))
4	3	oveq1d 7170	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) = ((𝐹‘(𝑋 + 𝑡)) − 𝐶))
5		oveq1 7162	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑡 → (𝑠 / 2) = (𝑡 / 2))
6	5	fveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (sin‘(𝑠 / 2)) = (sin‘(𝑡 / 2)))
7	6	oveq2d 7171	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (2 · (sin‘(𝑠 / 2))) = (2 · (sin‘(𝑡 / 2))))
8	4, 7	oveq12d 7173	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) = (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
9	8	cbvmptv 5138	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))
10	1, 9	eqtr2i 2782	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))) = 𝑂
11	10	oveq2i 7166	. . . . . . 7 ⊢ (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = (ℝ D 𝑂)
12	11	dmeqi 5749	. . . . . 6 ⊢ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))) = dom (ℝ D 𝑂)
13	12	ineq2i 4116	. . . . 5 ⊢ (ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2))))))) = (ran 𝑆 ∩ dom (ℝ D 𝑂))
14	13	sneqi 4536	. . . 4 ⊢ {(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} = {(ran 𝑆 ∩ dom (ℝ D 𝑂))}
15	14	uneq1i 4066	. . 3 ⊢ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
16		snfi 8619	. . . . 5 ⊢ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin
17		fzofi 13396	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
18		eqid 2758	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
19	18	rnmptfi 42194	. . . . . 6 ⊢ ((0..^𝑁) ∈ Fin → ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin)
20	17, 19	ax-mp 5	. . . . 5 ⊢ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin
21		unfi 8746	. . . . 5 ⊢ (({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∈ Fin ∧ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ Fin) → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
22	16, 20, 21	mp2an 691	. . . 4 ⊢ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin
23	22	a1i 11	. . 3 ⊢ (𝜑 → ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∈ Fin)
24	15, 23	eqeltrid 2856	. 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 4814	. . . 4 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
27	25, 26	eleqtrdi 2862	. . 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 4826	. . . . . . . . 9 ⊢ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
30	29	eleq2i 2843	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ 𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
31		elun 4056	. . . . . . . 8 ⊢ (𝑠 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
32	30, 31	sylbb 222	. . . . . . 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	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
35		ovex 7188	. . . . . . . . . . . . . 14 ⊢ (0...𝑁) ∈ V
36	35	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...𝑁) ∈ V)
37		fex 6985	. . . . . . . . . . . . 13 ⊢ ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ V) → 𝑆 ∈ V)
38	34, 36, 37	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ V)
39		rnexg 7619	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ran 𝑆 ∈ V)
40	38, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝑆 ∈ V)
41		inex1g 5192	. . . . . . . . . . 11 ⊢ (ran 𝑆 ∈ V → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
42	40, 41	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V)
43		unisng 4822	. . . . . . . . . 10 ⊢ ((ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ V → ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
44	42, 43	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
45	44	eleq2d 2837	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
46	45	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ↔ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))))
47	46	orbi1d 914	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((𝑠 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))))
48	33, 47	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
49		dvf 24611	. . . . . . . . 9 ⊢ (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ
50	49	a1i 11	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
51		elinel2 4103	. . . . . . . 8 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → 𝑠 ∈ dom (ℝ D 𝑂))
52	50, 51	ffvelrnd 6848	. . . . . . 7 ⊢ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
53	52	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
54		ovex 7188	. . . . . . . . . . . 12 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∈ V
55	54	dfiun3 5811	. . . . . . . . . . 11 ⊢ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
56	55	eleq2i 2843	. . . . . . . . . 10 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
57	56	biimpri 231	. . . . . . . . 9 ⊢ (𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
58	57	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
59		eliun 4890	. . . . . . . 8 ⊢ (𝑠 ∈ ∪ 𝑗 ∈ (0..^𝑁)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
60	58, 59	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
61		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
62		nfmpt1 5133	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
63	62	nfrn 5797	. . . . . . . . . . 11 ⊢ Ⅎ𝑗ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
64	63	nfuni 4808	. . . . . . . . . 10 ⊢ Ⅎ𝑗∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
65	64	nfcri 2906	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
66	61, 65	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
67		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑗((ℝ D 𝑂)‘𝑠) ∈ ℂ
68	49	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (ℝ D 𝑂):dom (ℝ D 𝑂)⟶ℂ)
69		fourierdlem80.y	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑌 = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
70	1	reseq1i 5823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
71		ioossicc 12870	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
72		fourierdlem80.sjss	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
73	71, 72	sstrid 3905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
74	73	resmptd 5884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
75	70, 74	syl5eq 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
76	69, 75	eqtr4id 2812	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
77	76	oveq2d 7171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
78		ax-resscn 10637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
79	78	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ℝ ⊆ ℂ)
80		fourierdlem80.f	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
81	80	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℝ)
82		fourierdlem80.xre	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ ℝ)
83	82	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑋 ∈ ℝ)
84		fourierdlem80.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐴 ∈ ℝ)
85		fourierdlem80.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ ℝ)
86	84, 85	iccssred 12871	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
87	86	sselda 3894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℝ)
88	83, 87	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
89	81, 88	ffvelrnd 6848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
90	89	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
91		fourierdlem80.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐶 ∈ ℝ)
92	91	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐶 ∈ ℂ)
93	92	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)
94	90, 93	subcld 11040	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
95		2cnd 11757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
96	86, 79	sstrd 3904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
97	96	sselda 3894	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ ℂ)
98	97	halfcld 11924	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (𝑠 / 2) ∈ ℂ)
99	98	sincld 15536	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
100	95, 99	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
101		2ne0 11783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ≠ 0
102	101	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
103		fourierdlem80.ab	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
104	103	sselda 3894	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ∈ (-π[,]π))
105		eqcom 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
106	105	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 0 → 0 = 𝑠)
107	106	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
108		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴[,]𝐵))
109	107, 108	eqeltrd 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑠 ∈ (𝐴[,]𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
110	109	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴[,]𝐵))
111		fourierdlem80.n0	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
112	111	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
113	110, 112	pm2.65da 816	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → ¬ 𝑠 = 0)
114	113	neqned 2958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑠 ≠ 0)
115		fourierdlem44 43187	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
116	104, 114, 115	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
117	95, 99, 102, 116	mulne0d 11335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
118	94, 100, 117	divcld 11459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴[,]𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
119	118, 1	fmptd 6874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑂:(𝐴[,]𝐵)⟶ℂ)
120		ioossre 12845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)
122		eqid 2758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
123	122	tgioo2 23509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
124	122, 123	dvres 24615	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℝ ⊆ ℂ ∧ 𝑂:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ℝ)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
125	79, 119, 86, 121, 124	syl22anc 837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
126		ioontr 42542	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))
127	126	reseq2i 5824	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
128	125, 127	eqtrdi 2809	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
129	128	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) = ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
130	77, 129	eqtr2d 2794	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (ℝ D 𝑌))
131	130	dmeqd 5750	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = dom (ℝ D 𝑌))
132	80	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℝ)
133	82	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑋 ∈ ℝ)
134	86	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
135	34	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐴[,]𝐵))
136		elfzofz 13107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
137	136	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
138	135, 137	ffvelrnd 6848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐴[,]𝐵))
139	134, 138	sseldd 3895	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
140		fzofzp1 13188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
141	140	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
142	135, 141	ffvelrnd 6848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐴[,]𝐵))
143	134, 142	sseldd 3895	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
144		fdv	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ)
145		fourierdlem80.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))
146	145	feq2i 6494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):𝐼⟶ℝ ↔ (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
147	144, 146	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
148	145	reseq2i 5824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹 ↾ 𝐼) = (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
149	148	oveq2i 7166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℝ D (𝐹 ↾ 𝐼)) = (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))
150	149	feq1i 6493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℝ D (𝐹 ↾ 𝐼)):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ ↔ (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
151	147, 150	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
152	103	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ (-π[,]π))
153	73, 152	sstrd 3904	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
154	111	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ (𝐴[,]𝐵))
155	73, 154	ssneldd 3897	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
156	91	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
157	132, 133, 139, 143, 151, 153, 155, 156, 69	fourierdlem57 43199	. . . . . . . . . . . . . . . . . 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))))
158	157	simpli 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ ∧ (ℝ D 𝑌) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
159	158	simpld 498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ)
160		fdm 6510	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ D 𝑌):((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))⟶ℝ → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
161	159, 160	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
162	131, 161	eqtr2d 2794	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
163		resss 5852	. . . . . . . . . . . . . . 15 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂)
164		dmss 5747	. . . . . . . . . . . . . . 15 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ (ℝ D 𝑂) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
165	163, 164	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → dom ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ⊆ dom (ℝ D 𝑂))
166	162, 165	eqsstrd 3932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
167	166	3adant3 1129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ dom (ℝ D 𝑂))
168		simp3 1135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
169	167, 168	sseldd 3895	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → 𝑠 ∈ dom (ℝ D 𝑂))
170	68, 169	ffvelrnd 6848	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
171	170	3exp 1116	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
172	171	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)))
173	66, 67, 172	rexlimd 3241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ))
174	60, 173	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
175	53, 174	jaodan 955	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∨ 𝑠 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
176	28, 48, 175	syl2anc 587	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
177	176	abscld 14849	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
178	27, 177	sylan2 595	. 2 ⊢ ((𝜑 ∧ 𝑠 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
179		id 22	. . . 4 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
180	179, 15	eleqtrdi 2862	. . 3 ⊢ (𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
181		elsni 4542	. . . . . 6 ⊢ (𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
182		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
183		fzfid 13395	. . . . . . . . . . 11 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
184		rnffi 42198	. . . . . . . . . . 11 ⊢ ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (0...𝑁) ∈ Fin) → ran 𝑆 ∈ Fin)
185	34, 183, 184	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑆 ∈ Fin)
186		infi 8784	. . . . . . . . . 10 ⊢ (ran 𝑆 ∈ Fin → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
187	185, 186	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
188	187	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∈ Fin)
189	182, 188	eqeltrd 2852	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → 𝑟 ∈ Fin)
190		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑠𝜑
191		nfcv 2919	. . . . . . . . . . 11 ⊢ Ⅎ𝑠ran 𝑆
192		nfcv 2919	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠ℝ
193		nfcv 2919	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠 D
194		nfmpt1 5133	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
195	1, 194	nfcxfr 2917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑠𝑂
196	192, 193, 195	nfov 7185	. . . . . . . . . . . 12 ⊢ Ⅎ𝑠(ℝ D 𝑂)
197	196	nfdm 5796	. . . . . . . . . . 11 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
198	191, 197	nfin 4123	. . . . . . . . . 10 ⊢ Ⅎ𝑠(ran 𝑆 ∩ dom (ℝ D 𝑂))
199	198	nfeq2 2936	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))
200	190, 199	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑠(𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
201		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ 𝑟)
202		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)))
203	201, 202	eleqtrd 2854	. . . . . . . . . . . 12 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
204	203, 51	syl 17	. . . . . . . . . . 11 ⊢ ((𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂)) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
205	204	adantll 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → 𝑠 ∈ dom (ℝ D 𝑂))
206	49	ffvelrni 6846	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → ((ℝ D 𝑂)‘𝑠) ∈ ℂ)
207	206	abscld 14849	. . . . . . . . . 10 ⊢ (𝑠 ∈ dom (ℝ D 𝑂) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
208	205, 207	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) ∧ 𝑠 ∈ 𝑟) → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
209	208	ex 416	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → (𝑠 ∈ 𝑟 → (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ))
210	200, 209	ralrimi 3144	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ)
211		fimaxre3 11629	. . . . . . 7 ⊢ ((𝑟 ∈ Fin ∧ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
212	189, 210, 211	syl2anc 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 = (ran 𝑆 ∩ dom (ℝ D 𝑂))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
213	181, 212	sylan2 595	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
214	213	adantlr 714	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
215		simpll 766	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝜑)
216		elunnel1 4057	. . . . . 6 ⊢ ((𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
217	216	adantll 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
218		vex 3413	. . . . . . . . 9 ⊢ 𝑟 ∈ V
219	18	elrnmpt 5801	. . . . . . . . 9 ⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
220	218, 219	ax-mp 5	. . . . . . . 8 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
221	220	biimpi 219	. . . . . . 7 ⊢ (𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
222	221	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
223	63	nfcri 2906	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
224	61, 223	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
225		nfv 1915	. . . . . . 7 ⊢ Ⅎ𝑗∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦
226		fourierdlem80.fbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
227		fourierdlem80.fdvbdioo	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
228		reeanv 3285	. . . . . . . . . . . . 13 ⊢ (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) ↔ (∃𝑤 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∃𝑧 ∈ ℝ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
229	226, 227, 228	sylanbrc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
230		simp1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
231		simp2l 1196	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑤 ∈ ℝ)
232		simp2r 1197	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝑧 ∈ ℝ)
233	230, 231, 232	jca31 518	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ))
234		simp3l 1198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
235		simp3r 1199	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
236	233, 234, 235	jca31 518	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
237		fourierdlem80.ch	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
238	236, 237	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → 𝜒)
239	237	biimpi 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜒 → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧))
240		simp-5l 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝜑)
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → 𝜑)
242	241, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐹:ℝ⟶ℝ)
243	241, 82	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑋 ∈ ℝ)
244		simp-4l 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
245	239, 244	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
246	245, 139	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) ∈ ℝ)
247	245, 143	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘(𝑗 + 1)) ∈ ℝ)
248		fourierdlem80.slt	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
249	245, 248	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
250	72, 152	sstrd 3904	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
251	245, 250	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (-π[,]π))
252	72, 154	ssneldd 3897	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
253	245, 252	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → ¬ 0 ∈ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))))
254	245, 151	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → (ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))):((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))⟶ℝ)
255		simp-4r 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑤 ∈ ℝ)
256	239, 255	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑤 ∈ ℝ)
257	239	simplrd 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤)
258		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))))
259	258, 145	eleqtrrdi 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1)))) → 𝑡 ∈ 𝐼)
260		rspa 3135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ 𝑡 ∈ 𝐼) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
261	257, 259, 260	syl2an 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘(𝐹‘𝑡)) ≤ 𝑤)
262		simpllr 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑤 ∈ ℝ) ∧ 𝑧 ∈ ℝ) ∧ ∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤) ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → 𝑧 ∈ ℝ)
263	239, 262	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝑧 ∈ ℝ)
264	149	fveq1i 6663	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D (𝐹 ↾ 𝐼))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)
265	264	fveq2i 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡))
266	239	simprd 499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
267	266	r19.21bi 3137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)
268	265, 267	eqbrtrrid 5071	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑡 ∈ 𝐼) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
269	259, 268	sylan2 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑡 ∈ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + (𝑆‘𝑗))(,)(𝑋 + (𝑆‘(𝑗 + 1))))))‘𝑡)) ≤ 𝑧)
270	241, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → 𝐶 ∈ ℝ)
271	242, 243, 246, 247, 249, 251, 253, 254, 256, 261, 263, 269, 270, 69	fourierdlem68 43210	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ∧ ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
272	271	simprd 499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
273	271	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜒 → dom (ℝ D 𝑌) = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
274	273	raleqdv 3329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜒 → (∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
275	274	rexbidv 3221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑌)(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
276	272, 275	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦)
277	126	eqcomi 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
278	277	reseq2i 5824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
279	278	fveq1i 6663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠)
280		fvres 6681	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
281	280	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑠) = ((ℝ D 𝑂)‘𝑠))
282	245, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜒 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐴[,]𝐵))
283	282	resmptd 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜒 → ((𝑠 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
284	70, 283	syl5eq 2805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜒 → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
285	69, 284	eqtr4id 2812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜒 → 𝑌 = (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
286	285	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜒 → (ℝ D 𝑌) = (ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
287	286	fveq1d 6664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D 𝑌)‘𝑠) = ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
288	125	fveq1d 6664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
289	241, 288	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜒 → ((ℝ D (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠))
290	287, 289	eqtr2d 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜒 → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
291	290	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (((ℝ D 𝑂) ↾ ((int‘(topGen‘ran (,)))‘((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))‘𝑠) = ((ℝ D 𝑌)‘𝑠))
292	279, 281, 291	3eqtr3a 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((ℝ D 𝑂)‘𝑠) = ((ℝ D 𝑌)‘𝑠))
293	292	fveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D 𝑌)‘𝑠)))
294	293	breq1d 5045	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜒 ∧ 𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ (abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
295	294	ralbidva 3125	. . . . . . . . . . . . . . . . 17 ⊢ (𝜒 → (∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
296	295	rexbidv 3221	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑌)‘𝑠)) ≤ 𝑦))
297	276, 296	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
298	238, 297	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
299	298	3exp 1116	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
300	299	rexlimdvv 3217	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (∃𝑤 ∈ ℝ ∃𝑧 ∈ ℝ (∀𝑡 ∈ 𝐼 (abs‘(𝐹‘𝑡)) ≤ 𝑤 ∧ ∀𝑡 ∈ 𝐼 (abs‘((ℝ D (𝐹 ↾ 𝐼))‘𝑡)) ≤ 𝑧) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
301	229, 300	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
302	301	3adant3 1129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
303		raleq 3323	. . . . . . . . . . . 12 ⊢ (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
304	303	3ad2ant3 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
305	304	rexbidv 3221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑠 ∈ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
306	302, 305	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
307	306	3exp 1116	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
308	307	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (𝑗 ∈ (0..^𝑁) → (𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)))
309	224, 225, 308	rexlimd 3241	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → (∃𝑗 ∈ (0..^𝑁)𝑟 = ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦))
310	222, 309	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
311	215, 217, 310	syl2anc 587	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) ∧ ¬ 𝑟 ∈ {(ran 𝑆 ∩ dom (ℝ D 𝑂))}) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
312	214, 311	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
313	180, 312	sylan2 595	. 2 ⊢ ((𝜑 ∧ 𝑟 ∈ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))) → ∃𝑦 ∈ ℝ ∀𝑠 ∈ 𝑟 (abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑦)
314		pm3.22 463	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
315		elin 3876	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)) ↔ (𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom (ℝ D 𝑂)))
316	314, 315	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ dom (ℝ D 𝑂) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
317	316	adantll 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (ran 𝑆 ∩ dom (ℝ D 𝑂)))
318	44	eqcomd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
319	318	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (ran 𝑆 ∩ dom (ℝ D 𝑂)) = ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
320	317, 319	eleqtrd 2854	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))})
321	320	orcd 870	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
322		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝜑)
323	78	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → ℝ ⊆ ℂ)
324	119	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑂:(𝐴[,]𝐵)⟶ℂ)
325	84	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐴 ∈ ℝ)
326	85	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝐵 ∈ ℝ)
327	325, 326	iccssred 12871	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝐴[,]𝐵) ⊆ ℝ)
328	323, 324, 327	dvbss 24605	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → dom (ℝ D 𝑂) ⊆ (𝐴[,]𝐵))
329		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ dom (ℝ D 𝑂))
330	328, 329	sseldd 3895	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (𝐴[,]𝐵))
331	330	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ (𝐴[,]𝐵))
332		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ¬ 𝑟 ∈ ran 𝑆)
333		fourierdlem80.relioo	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
334		fveq2 6662	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘𝑗) = (𝑆‘𝑘))
335		oveq1 7162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1))
336	335	fveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑘 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝑘 + 1)))
337	334, 336	oveq12d 7173	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
338		ovex 7188	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))) ∈ V
339	337, 18, 338	fvmpt 6763	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0..^𝑁) → ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) = ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
340	339	eleq2d 2837	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0..^𝑁) → (𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ 𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1)))))
341	340	rexbiia 3174	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑆‘𝑘)(,)(𝑆‘(𝑘 + 1))))
342	333, 341	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
343	54, 18	dmmpti 6479	. . . . . . . . . . . . 13 ⊢ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (0..^𝑁)
344	343	rexeqi 3328	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘) ↔ ∃𝑘 ∈ (0..^𝑁)𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
345	342, 344	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
346	322, 331, 332, 345	syl21anc 836	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘))
347		funmpt 6377	. . . . . . . . . . 11 ⊢ Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))
348		elunirn 7007	. . . . . . . . . . 11 ⊢ (Fun (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
349	347, 348	mp1i 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ↔ ∃𝑘 ∈ dom (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))𝑟 ∈ ((𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))‘𝑘)))
350	346, 349	mpbird 260	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
351	350	olcd 871	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) ∧ ¬ 𝑟 ∈ ran 𝑆) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
352	321, 351	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
353		elun 4056	. . . . . . 7 ⊢ (𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ (𝑟 ∈ ∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∨ 𝑟 ∈ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
354	352, 353	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ (∪ {(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
355	354, 29	eleqtrrdi 2863	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ dom (ℝ D 𝑂)) → 𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
356	355	ralrimiva 3113	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
357		dfss3 3882	. . . 4 ⊢ (dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))) ↔ ∀𝑟 ∈ dom (ℝ D 𝑂)𝑟 ∈ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
358	356, 357	sylibr 237	. . 3 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D 𝑂))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
359	358, 26	sseqtrrdi 3945	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) ⊆ ∪ ({(ran 𝑆 ∩ dom (ℝ D (𝑡 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘(𝑋 + 𝑡)) − 𝐶) / (2 · (sin‘(𝑡 / 2)))))))} ∪ ran (𝑗 ∈ (0..^𝑁) ↦ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))))))
360	24, 178, 313, 359	ssfiunibd 42337	1 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ∀wral 3070 ∃wrex 3071 Vcvv 3409 ∪ cun 3858 ∩ cin 3859 ⊆ wss 3860 {csn 4525 ∪ cuni 4801 ∪ ciun 4886 class class class wbr 5035 ↦ cmpt 5115 dom cdm 5527 ran crn 5528 ↾ cres 5529 Fun wfun 6333 ⟶wf 6335 ‘cfv 6339 (class class class)co 7155 Fincfn 8532 ℂcc 10578 ℝcr 10579 0cc0 10580 1c1 10581 + caddc 10583 · cmul 10585 < clt 10718 ≤ cle 10719 − cmin 10913 -cneg 10914 / cdiv 11340 2c2 11734 (,)cioo 12784 [,]cicc 12787 ...cfz 12944 ..^cfzo 13087 ↑cexp 13484 abscabs 14646 sincsin 15470 cosccos 15471 πcpi 15473 TopOpenctopn 16758 topGenctg 16774 ℂ_fldccnfld 20171 intcnt 21722 D cdv 24567

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 ax-inf2 9142 ax-cnex 10636 ax-resscn 10637 ax-1cn 10638 ax-icn 10639 ax-addcl 10640 ax-addrcl 10641 ax-mulcl 10642 ax-mulrcl 10643 ax-mulcom 10644 ax-addass 10645 ax-mulass 10646 ax-distr 10647 ax-i2m1 10648 ax-1ne0 10649 ax-1rid 10650 ax-rnegex 10651 ax-rrecex 10652 ax-cnre 10653 ax-pre-lttri 10654 ax-pre-lttrn 10655 ax-pre-ltadd 10656 ax-pre-mulgt0 10657 ax-pre-sup 10658 ax-addf 10659 ax-mulf 10660

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-iin 4889 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-se 5487 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-of 7410 df-om 7585 df-1st 7698 df-2nd 7699 df-supp 7841 df-wrecs 7962 df-recs 8023 df-rdg 8061 df-1o 8117 df-2o 8118 df-er 8304 df-map 8423 df-pm 8424 df-ixp 8485 df-en 8533 df-dom 8534 df-sdom 8535 df-fin 8536 df-fsupp 8872 df-fi 8913 df-sup 8944 df-inf 8945 df-oi 9012 df-card 9406 df-pnf 10720 df-mnf 10721 df-xr 10722 df-ltxr 10723 df-le 10724 df-sub 10915 df-neg 10916 df-div 11341 df-nn 11680 df-2 11742 df-3 11743 df-4 11744 df-5 11745 df-6 11746 df-7 11747 df-8 11748 df-9 11749 df-n0 11940 df-z 12026 df-dec 12143 df-uz 12288 df-q 12394 df-rp 12436 df-xneg 12553 df-xadd 12554 df-xmul 12555 df-ioo 12788 df-ioc 12789 df-ico 12790 df-icc 12791 df-fz 12945 df-fzo 13088 df-fl 13216 df-mod 13292 df-seq 13424 df-exp 13485 df-fac 13689 df-bc 13718 df-hash 13746 df-shft 14479 df-cj 14511 df-re 14512 df-im 14513 df-sqrt 14647 df-abs 14648 df-limsup 14881 df-clim 14898 df-rlim 14899 df-sum 15096 df-ef 15474 df-sin 15476 df-cos 15477 df-pi 15479 df-struct 16548 df-ndx 16549 df-slot 16550 df-base 16552 df-sets 16553 df-ress 16554 df-plusg 16641 df-mulr 16642 df-starv 16643 df-sca 16644 df-vsca 16645 df-ip 16646 df-tset 16647 df-ple 16648 df-ds 16650 df-unif 16651 df-hom 16652 df-cco 16653 df-rest 16759 df-topn 16760 df-0g 16778 df-gsum 16779 df-topgen 16780 df-pt 16781 df-prds 16784 df-xrs 16838 df-qtop 16843 df-imas 16844 df-xps 16846 df-mre 16920 df-mrc 16921 df-acs 16923 df-mgm 17923 df-sgrp 17972 df-mnd 17983 df-submnd 18028 df-mulg 18297 df-cntz 18519 df-cmn 18980 df-psmet 20163 df-xmet 20164 df-met 20165 df-bl 20166 df-mopn 20167 df-fbas 20168 df-fg 20169 df-cnfld 20172 df-top 21599 df-topon 21616 df-topsp 21638 df-bases 21651 df-cld 21724 df-ntr 21725 df-cls 21726 df-nei 21803 df-lp 21841 df-perf 21842 df-cn 21932 df-cnp 21933 df-t1 22019 df-haus 22020 df-cmp 22092 df-tx 22267 df-hmeo 22460 df-fil 22551 df-fm 22643 df-flim 22644 df-flf 22645 df-xms 23027 df-ms 23028 df-tms 23029 df-cncf 23584 df-limc 24570 df-dv 24571

This theorem is referenced by: fourierdlem103 43245 fourierdlem104 43246

W3C validator