Theorem fourierdlem98 46175

Description: 𝐹 is continuous on the intervals induced by the moved partition 𝑉. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem98.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem98.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem98.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem98.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem98.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem98.fper	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierdlem98.qcn	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem98.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem98.d	⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
fourierdlem98.j	⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
fourierdlem98.v	⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))

Assertion

Ref	Expression
fourierdlem98	⊢ (𝜑 → (𝐹 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Distinct variable groups:   𝑄,𝑔   𝑖,𝑀,𝑥   𝜑,𝑖,𝑥   𝑇,𝑖,𝑘,𝑥   𝑄,ℎ   𝑇,ℎ,𝑦   𝑇,𝑚,𝑝,𝑦   𝑄,𝑘,𝑚,𝑝,𝑦   𝑚,𝑀,𝑝,𝑖   𝑄,𝑖,𝑥   𝑖,𝐽,𝑥   𝑖,𝐹,𝑥   𝑥,𝐶,𝑦,𝑖   𝐶,𝑚,𝑝   𝑉,𝑝,𝑖   𝑥,𝑉   𝑥,𝐴,𝑖   𝐴,𝑚,𝑝   𝑇,𝑔,𝑘   𝐷,𝑚,𝑝,𝑖   𝑥,𝐷,𝑦,𝑖   𝐵,𝑖,𝑥   𝐷,𝑔   𝐶,𝑔,𝑦   𝐵,𝑚,𝑝

Allowed substitution hints:   𝜑(𝑦,𝑔,ℎ,𝑘,𝑚,𝑝)   𝐴(𝑦,𝑔,ℎ,𝑘)   𝐵(𝑦,𝑔,ℎ,𝑘)   𝐶(ℎ,𝑘)   𝐷(ℎ,𝑘)   𝑃(𝑥,𝑦,𝑔,ℎ,𝑖,𝑘,𝑚,𝑝)   𝐹(𝑦,𝑔,ℎ,𝑘,𝑚,𝑝)   𝐽(𝑦,𝑔,ℎ,𝑘,𝑚,𝑝)   𝑀(𝑦,𝑔,ℎ,𝑘)   𝑉(𝑦,𝑔,ℎ,𝑘,𝑚)

Proof of Theorem fourierdlem98

Dummy variables 𝑓 𝑢 𝑧 𝑙 𝑡 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem98.p	. 2 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
2		fourierdlem98.t	. 2 ⊢ 𝑇 = (𝐵 − 𝐴)
3		fourierdlem98.m	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		fourierdlem98.q	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
5		fourierdlem98.f	. . 3 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
6		ax-resscn 11101	. . . 4 ⊢ ℝ ⊆ ℂ
7	6	a1i 11	. . 3 ⊢ (𝜑 → ℝ ⊆ ℂ)
8	5, 7	fssd 6687	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
9		fourierdlem98.fper	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
10		fourierdlem98.qcn	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
11		fourierdlem98.c	. 2 ⊢ (𝜑 → 𝐶 ∈ ℝ)
12		fourierdlem98.d	. 2 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
13		eqid 2729	. 2 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
14		oveq1 7376	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
15	14	eleq1d 2813	. . . . . 6 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
16	15	rexbidv 3157	. . . . 5 ⊢ (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
17	16	cbvrabv 3413	. . . 4 ⊢ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
18	17	uneq2i 4124	. . 3 ⊢ ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
19	18	eqcomi 2738	. 2 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
20		oveq1 7376	. . . . . . . . . 10 ⊢ (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
21	20	oveq2d 7385	. . . . . . . . 9 ⊢ (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
22	21	eleq1d 2813	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
23	22	cbvrexvw 3214	. . . . . . 7 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
24	23	a1i 11	. . . . . 6 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
25	24	rabbiia 3406	. . . . 5 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
26	25	uneq2i 4124	. . . 4 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
27	26	fveq2i 6843	. . 3 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
28	27	oveq1i 7379	. 2 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
29		oveq1 7376	. . . . . . . . . . 11 ⊢ (𝑙 = ℎ → (𝑙 · 𝑇) = (ℎ · 𝑇))
30	29	oveq2d 7385	. . . . . . . . . 10 ⊢ (𝑙 = ℎ → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + (ℎ · 𝑇)))
31	30	eleq1d 2813	. . . . . . . . 9 ⊢ (𝑙 = ℎ → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
32	31	cbvrexvw 3214	. . . . . . . 8 ⊢ (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄)
33	32	a1i 11	. . . . . . 7 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
34	33	rabbiia 3406	. . . . . 6 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}
35	34	uneq2i 4124	. . . . 5 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
36		isoeq5 7278	. . . . 5 ⊢ (({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}) → (𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))))
37	35, 36	ax-mp 5	. . . 4 ⊢ (𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
38	37	iotabii 6484	. . 3 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
39		isoeq1 7274	. . . 4 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
40	39	cbviotavw 6460	. . 3 ⊢ (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
41		fourierdlem98.v	. . 3 ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
42	38, 40, 41	3eqtr4ri 2763	. 2 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
43		id 22	. . . 4 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
44		oveq2 7377	. . . . . . 7 ⊢ (𝑣 = 𝑥 → (𝐵 − 𝑣) = (𝐵 − 𝑥))
45	44	oveq1d 7384	. . . . . 6 ⊢ (𝑣 = 𝑥 → ((𝐵 − 𝑣) / 𝑇) = ((𝐵 − 𝑥) / 𝑇))
46	45	fveq2d 6844	. . . . 5 ⊢ (𝑣 = 𝑥 → (⌊‘((𝐵 − 𝑣) / 𝑇)) = (⌊‘((𝐵 − 𝑥) / 𝑇)))
47	46	oveq1d 7384	. . . 4 ⊢ (𝑣 = 𝑥 → ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
48	43, 47	oveq12d 7387	. . 3 ⊢ (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
49	48	cbvmptv 5206	. 2 ⊢ (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
50		eqeq1 2733	. . . 4 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝐵 ↔ 𝑧 = 𝐵))
51		id 22	. . . 4 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
52	50, 51	ifbieq2d 4511	. . 3 ⊢ (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
53	52	cbvmptv 5206	. 2 ⊢ (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
54		fourierdlem98.j	. 2 ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
55		eqid 2729	. 2 ⊢ ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
56		eqid 2729	. 2 ⊢ (𝐹 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐹 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
57		eqid 2729	. 2 ⊢ (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐹 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐹 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
58		fveq2 6840	. . . . . . 7 ⊢ (𝑖 = 𝑡 → (𝑄‘𝑖) = (𝑄‘𝑡))
59	58	breq1d 5112	. . . . . 6 ⊢ (𝑖 = 𝑡 → ((𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
60	59	cbvrabv 3413	. . . . 5 ⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
61		fveq2 6840	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))
62	61	fveq2d 6844	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
63	62	eqcomd 2735	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
64	63	breq2d 5114	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
65	64	rabbidv 3410	. . . . 5 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
66	60, 65	eqtr2id 2777	. . . 4 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
67	66	supeq1d 9373	. . 3 ⊢ (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
68	67	cbvmptv 5206	. 2 ⊢ (𝑤 ∈ ℝ ↦ sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < )) = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
69	1, 2, 3, 4, 8, 9, 10, 11, 12, 13, 19, 28, 42, 49, 53, 54, 55, 56, 57, 68	fourierdlem90 46167	1 ⊢ (𝜑 → (𝐹 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  {crab 3402   ∪ cun 3909   ⊆ wss 3911  ifcif 4484  {cpr 4587   class class class wbr 5102   ↦ cmpt 5183  ran crn 5632   ↾ cres 5633  ℩cio 6450  ⟶wf 6495  ‘cfv 6499   Isom wiso 6500  (class class class)co 7369   ↑_m cmap 8776  supcsup 9367  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   · cmul 11049  +∞cpnf 11181   < clt 11184   ≤ cle 11185   − cmin 11381   / cdiv 11811  ℕcn 12162  ℤcz 12505  (,)cioo 13282  (,]cioc 13283  [,]cicc 13285  ...cfz 13444  ..^cfzo 13591  ⌊cfl 13728  ♯chash 14271  –cn→ccncf 24745

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-oadd 8415  df-er 8648  df-map 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fi 9338  df-sup 9369  df-inf 9370  df-oi 9439  df-dju 9830  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-xnn0 12492  df-z 12506  df-uz 12770  df-q 12884  df-rp 12928  df-xneg 13048  df-xadd 13049  df-xmul 13050  df-ioo 13286  df-ioc 13287  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-fl 13730  df-seq 13943  df-exp 14003  df-hash 14272  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-rest 17361  df-topgen 17382  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-top 22757  df-topon 22774  df-bases 22809  df-cld 22882  df-ntr 22883  df-cls 22884  df-nei 22961  df-lp 22999  df-cmp 23250  df-cncf 24747

This theorem is referenced by:  fourierdlem112  46189