fourierdlem97 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem97		Structured version Visualization version GIF version

Theorem fourierdlem97 46174

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

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

**Assertion**
Ref	Expression
fourierdlem97	⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Distinct variable groups: 𝑇,𝑖,𝑠,𝑥 𝐷,𝑖,𝑥,𝑦 𝑖,𝐽,𝑠,𝑥 𝐶,𝑖,𝑝 𝑄,ℎ ℎ,𝑀,𝑖,𝑥 𝑥,𝐶,𝑦 𝑄,𝑘 𝑥,𝐵 𝑉,𝑝 𝑖,𝐻,𝑠,𝑥 𝐷,𝑚,𝑝 𝑄,𝑔,ℎ 𝑇,ℎ 𝜑,𝑠 𝑀,𝑠 𝜑,ℎ,𝑦 𝑄,𝑚,𝑝,𝑦,𝑘 𝑥,𝐹,𝑦 𝑇,𝑔,𝑘,𝑦 𝐴,𝑖,𝑚,𝑝 𝑇,𝑚 𝜑,𝑖,𝑥 𝑇,𝑝 𝑖,𝑉,𝑘,𝑥 𝐶,𝑚 𝜑,𝑔 ℎ,𝑉 ℎ,𝐽,𝑘 𝑚,𝑀,𝑝 𝑉,𝑠 𝑦,𝐺 𝐵,𝑖,𝑝 𝑄,𝑖,𝑠,𝑥 𝐶,𝑔 𝐺,𝑠 𝑔,𝑉 𝐵,𝑚 𝐹,𝑠 𝐷,𝑔 𝑖,𝐺 𝑥,𝐴 Allowed substitution hints: 𝜑(𝑘,𝑚,𝑝) 𝐴(𝑦,𝑔,ℎ,𝑘,𝑠) 𝐵(𝑦,𝑔,ℎ,𝑘,𝑠) 𝐶(ℎ,𝑘,𝑠) 𝐷(ℎ,𝑘,𝑠) 𝑃(𝑥,𝑦,𝑔,ℎ,𝑖,𝑘,𝑚,𝑠,𝑝) 𝐹(𝑔,ℎ,𝑖,𝑘,𝑚,𝑝) 𝐺(𝑥,𝑔,ℎ,𝑘,𝑚,𝑝) 𝐻(𝑦,𝑔,ℎ,𝑘,𝑚,𝑝) 𝐽(𝑦,𝑔,𝑚,𝑝) 𝑀(𝑦,𝑔,𝑘) 𝑉(𝑦,𝑚)

Proof of Theorem fourierdlem97 Dummy variables 𝑓 𝑙 𝑡 𝑢 𝑤 𝑧 𝑒 𝑗 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioossre 13344	. . . . . . . 8 ⊢ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ)
3	2	sselda 3943	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ ℝ)
4		iftrue 4490	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
5	4	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
6		fourierdlem97.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
7		ssid 3966	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ
8		dvfre 25831	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
10		fourierdlem97.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (ℝ D 𝐹)
11	10	feq1i 6661	. . . . . . . . . . . . 13 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
12	9, 11	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
14		id 22	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom 𝐺)
15	10	dmeqi 5858	. . . . . . . . . . . . 13 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
16	14, 15	eleqtrdi 2838	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom (ℝ D 𝐹))
17	16	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝑠 ∈ dom (ℝ D 𝐹))
18	13, 17	ffvelcdmd 7039	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → (𝐺‘𝑠) ∈ ℝ)
19	5, 18	eqeltrd 2828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
20	19	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
21		iffalse 4493	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
22		0red 11153	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ)
23	21, 22	eqeltrd 2828	. . . . . . . . 9 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
24	23	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ ¬ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
25	20, 24	pm2.61dan 812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
26	3, 25	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
27		fourierdlem97.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
28	27	fvmpt2 6961	. . . . . 6 ⊢ ((𝑠 ∈ ℝ ∧ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
29	3, 26, 28	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
30		fourierdlem97.t	. . . . . . . . . 10 ⊢ 𝑇 = (𝐵 − 𝐴)
31		fourierdlem97.p	. . . . . . . . . 10 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
32		fourierdlem97.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
33		fourierdlem97.q	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
34		fourierdlem97.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
35		fourierdlem97.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
36		elioore 13312	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
38	34	rexrd 11200	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
39		pnfxr 11204	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
40	39	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → +∞ ∈ ℝ^*)
41		ioogtlb 45466	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
42	38, 40, 35, 41	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 < 𝐷)
43		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 + (ℎ · 𝑇)) = (𝑥 + (ℎ · 𝑇)))
44	43	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
45	44	rexbidv 3157	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
46	45	cbvrabv 3413	. . . . . . . . . . 11 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄}
47	46	uneq2i 4124	. . . . . . . . . 10 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄})
48		oveq1 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
49	48	oveq2d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
50	49	eleq1d 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
51	50	cbvrexvw 3214	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
52	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
53	52	rabbiia 3406	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
54	53	uneq2i 4124	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
55		oveq1 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 = ℎ → (𝑙 · 𝑇) = (ℎ · 𝑇))
56	55	oveq2d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + (ℎ · 𝑇)))
57	56	eleq1d 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
58	57	cbvrexvw 3214	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄)
59	58	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
60	59	rabbiia 3406	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}
61	60	uneq2i 4124	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
62	54, 61	eqtri 2752	. . . . . . . . . . . 12 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
63	62	fveq2i 6843	. . . . . . . . . . 11 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))
64	63	oveq1i 7379	. . . . . . . . . 10 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})) − 1)
65		fourierdlem97.v	. . . . . . . . . 10 ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
66		fourierdlem97.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
67		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ℎ → (𝑘 · 𝑇) = (ℎ · 𝑇))
68	67	oveq2d 7385	. . . . . . . . . . . . 13 ⊢ (𝑘 = ℎ → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (ℎ · 𝑇)))
69	68	breq1d 5112	. . . . . . . . . . . 12 ⊢ (𝑘 = ℎ → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)))
70	69	cbvrabv 3413	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} = {ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}
71	70	supeq1i 9374	. . . . . . . . . 10 ⊢ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
72		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑒 → (𝑄‘𝑗) = (𝑄‘𝑒))
73	72	oveq1d 7384	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑒 → ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) = ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)))
74	73	breq1d 5112	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑒 → (((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)))
75	74	cbvrabv 3413	. . . . . . . . . . 11 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)} = {𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}
76	75	supeq1i 9374	. . . . . . . . . 10 ⊢ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
77	30, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76	fourierdlem64 46141	. . . . . . . . 9 ⊢ (𝜑 → ((sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀) ∧ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
78	77	simprd 495	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
79		simpl1 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝜑)
80		simpl2l 1227	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑖 ∈ (0..^𝑀))
81		fourierdlem97.qcn	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
82		cncff 24762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
84		ffun 6673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ → Fun 𝐺)
85	12, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun 𝐺)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → Fun 𝐺)
87		ffvresb 7079	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun 𝐺 → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ)))
88	86, 87	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ)))
89	83, 88	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
90	89	r19.21bi 3227	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
91	90	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ dom 𝐺)
92	91	ralrimiva 3125	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
93		dfss3 3932	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
94	92, 93	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
95	79, 80, 94	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
96		simpl2 1193	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ))
97	79, 96	jca 511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)))
98		simpl3 1194	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
99		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
100	98, 99	sseldd 3944	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
101	31	fourierdlem2 46080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
102	32, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
103	33, 102	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
104	103	simpld 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
105		elmapi 8799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
107	106	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
108		elfzofz 13612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
109	108	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
110	107, 109	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
111	110	rexrd 11200	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
112	111	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ^*)
113	112	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ^*)
114		fzofzp1 13701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
115	114	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
116	107, 115	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
117	116	adantrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
118	117	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
119	118	rexrd 11200	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
120		elioore 13312	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → 𝑡 ∈ ℝ)
121	120	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ ℝ)
122		zre 12509	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℝ)
123	122	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
124	123	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑙 ∈ ℝ)
125		fourierdlem97.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
126		fourierdlem97.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
127	125, 126	resubcld 11582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
128	30, 127	eqeltrid 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
129	128	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑇 ∈ ℝ)
130	124, 129	remulcld 11180	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑙 · 𝑇) ∈ ℝ)
131	121, 130	resubcld 11582	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ℝ)
132	110	adantrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ)
133	122	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑙 ∈ ℝ)
134	128	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑇 ∈ ℝ)
135	133, 134	remulcld 11180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑙 · 𝑇) ∈ ℝ)
136	132, 135	readdcld 11179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ)
137	136	rexrd 11200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
138	137	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
139	117, 135	readdcld 11179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ)
140	139	rexrd 11200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
141	140	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
142		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
143		ioogtlb 45466	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
144	138, 141, 142, 143	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
145	132	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ)
146	145, 130, 121	ltaddsubd 11754	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡 ↔ (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇))))
147	144, 146	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇)))
148		iooltub 45481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
149	138, 141, 142, 148	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
150	121, 130, 118	ltsubaddd 11750	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)) ↔ 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
151	149, 150	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)))
152	113, 119, 131, 147, 151	eliood 45469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
153	97, 100, 152	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
154	95, 153	sseldd 3944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)
155		elioore 13312	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑡 ∈ ℝ)
156		recn 11134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
157	156	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
158		zcn 12510	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℂ)
159	158	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑙 ∈ ℂ)
160	128	recnd 11178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ ℂ)
161	160	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℂ)
162	159, 161	mulcld 11170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝑙 · 𝑇) ∈ ℂ)
163	157, 162	npcand 11513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) = 𝑡)
164	163	eqcomd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
165	164	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
166		ovex 7402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 − (𝑙 · 𝑇)) ∈ V
167		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 ∈ dom 𝐺 ↔ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺))
168	167	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) ↔ ((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)))
169		oveq1 7376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 + (𝑙 · 𝑇)) = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
170	169	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ↔ ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺))
171	169	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))))
172		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘𝑠) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))
173	171, 172	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠) ↔ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
174	170, 173	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)) ↔ (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))))
175	168, 174	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠))) ↔ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))))
176		ax-resscn 11101	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℂ
177	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ⊆ ℂ)
178	6, 177	fssd 6687	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
179	178	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
180	122	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
181	128	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑇 ∈ ℝ)
182	180, 181	remulcld 11180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → (𝑙 · 𝑇) ∈ ℝ)
183	178	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
184	128	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
185		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑙 ∈ ℤ)
186		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
187		fourierdlem97.fper	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
188	187	ad4ant14 752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
189	183, 184, 185, 186, 188	fperiodmul 45275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → (𝐹‘(𝑠 + (𝑙 · 𝑇))) = (𝐹‘𝑠))
190	179, 182, 189, 10	fperdvper 45890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)))
191	166, 175, 190	vtocl 3521	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
192	191	simpld 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
193	192	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
194	165, 193	eqeltrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 ∈ dom 𝐺)
195	194	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
196	155, 195	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
197	196	adantlrl 720	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
198	197	3adantl3 1169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
199	154, 198	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ dom 𝐺)
200	199	ralrimiva 3125	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
201		dfss3 3932	. . . . . . . . . . 11 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺 ↔ ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
202	200, 201	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
203	202	3exp 1119	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)))
204	203	rexlimdvv 3191	. . . . . . . 8 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺))
205	78, 204	mpd 15	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
206	205	sselda 3943	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ dom 𝐺)
207	206	iftrued 4492	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
208	29, 207	eqtr2d 2765	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐺‘𝑠) = (𝐻‘𝑠))
209	208	mpteq2dva 5195	. . 3 ⊢ (𝜑 → (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
210	15	a1i 11	. . . . . 6 ⊢ (𝜑 → dom 𝐺 = dom (ℝ D 𝐹))
211	210	feq2d 6654	. . . . 5 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
212	12, 211	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐺:dom 𝐺⟶ℝ)
213	212, 205	feqresmpt 6912	. . 3 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)))
214	25, 27	fmptd 7068	. . . 4 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
215	214, 2	feqresmpt 6912	. . 3 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
216	209, 213, 215	3eqtr4d 2774	. 2 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))))
217	214, 177	fssd 6687	. . 3 ⊢ (𝜑 → 𝐻:ℝ⟶ℂ)
218	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
219		eleq1 2816	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝑠 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
220		fveq2 6840	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝐺‘𝑠) = (𝐺‘(𝑥 + 𝑇)))
221	219, 220	ifbieq1d 4509	. . . . . . . 8 ⊢ (𝑠 = (𝑥 + 𝑇) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
222	178, 128, 187, 10	fperdvper 45890	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))
223	222	simpld 494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
224	223	iftrued 4492	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = (𝐺‘(𝑥 + 𝑇)))
225	221, 224	sylan9eqr 2786	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
226	225	adantllr 719	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
227		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
228	128	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229	227, 228	readdcld 11179	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℝ)
230	229	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
231	212	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐺:dom 𝐺⟶ℝ)
232	223	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
233	231, 232	ffvelcdmd 7039	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) ∈ ℝ)
234	218, 226, 230, 233	fvmptd 6957	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
235	222	simprd 495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
236	235	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
237		eleq1 2816	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝑠 ∈ dom 𝐺 ↔ 𝑥 ∈ dom 𝐺))
238		fveq2 6840	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝐺‘𝑠) = (𝐺‘𝑥))
239	237, 238	ifbieq1d 4509	. . . . . . . 8 ⊢ (𝑠 = 𝑥 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
240	239	adantl 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
241		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
242		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
243	242	iftrued 4492	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
244	212	ffvelcdmda 7038	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℝ)
245	243, 244	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
246	245	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
247	218, 240, 241, 246	fvmptd 6957	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
248		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
249	248	iftrued 4492	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
250	247, 249	eqtr2d 2765	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐻‘𝑥))
251	234, 236, 250	3eqtrd 2768	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
252	229	recnd 11178	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℂ)
253	228	recnd 11178	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
254	252, 253	negsubd 11515	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) + -𝑇) = ((𝑥 + 𝑇) − 𝑇))
255	227	recnd 11178	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
256	255, 253	pncand 11510	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
257	254, 256	eqtr2d 2765	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
258	257	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
259		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
260		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝜑)
261	260, 259	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺))
262		eleq1 2816	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
263	262	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝜑 ∧ 𝑦 ∈ dom 𝐺) ↔ (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺)))
264		oveq1 7376	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 + -𝑇) = ((𝑥 + 𝑇) + -𝑇))
265	264	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝑦 + -𝑇) ∈ dom 𝐺 ↔ ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺))
266	264	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘(𝑦 + -𝑇)) = (𝐺‘((𝑥 + 𝑇) + -𝑇)))
267		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘𝑦) = (𝐺‘(𝑥 + 𝑇)))
268	266, 267	eqeq12d 2745	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦) ↔ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
269	265, 268	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)) ↔ (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
270	263, 269	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦))) ↔ ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))))
271	128	renegcld 11581	. . . . . . . . . . . 12 ⊢ (𝜑 → -𝑇 ∈ ℝ)
272	160	mulm1d 11606	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-1 · 𝑇) = -𝑇)
273	272	eqcomd 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -𝑇 = (-1 · 𝑇))
274	273	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -𝑇 = (-1 · 𝑇))
275	274	oveq2d 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + -𝑇) = (𝑦 + (-1 · 𝑇)))
276	275	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘(𝑦 + (-1 · 𝑇))))
277	178	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
278	128	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
279		1zzd 12540	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℤ)
280	279	znegcld 12616	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -1 ∈ ℤ)
281		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
282	187	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
283	277, 278, 280, 281, 282	fperiodmul 45275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + (-1 · 𝑇))) = (𝐹‘𝑦))
284	276, 283	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘𝑦))
285	178, 271, 284, 10	fperdvper 45890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)))
286	270, 285	vtoclg 3517	. . . . . . . . . 10 ⊢ ((𝑥 + 𝑇) ∈ dom 𝐺 → ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
287	259, 261, 286	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
288	287	simpld 494	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺)
289	258, 288	eqeltrd 2828	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
290	289	stoic1a 1772	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ (𝑥 + 𝑇) ∈ dom 𝐺)
291	290	iffalsed 4495	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = 0)
292	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
293	221	adantl 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
294	229	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
295		0red 11153	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 0 ∈ ℝ)
296	291, 295	eqeltrd 2828	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) ∈ ℝ)
297	292, 293, 294, 296	fvmptd 6957	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
298		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ 𝑥 ∈ dom 𝐺)
299	298	iffalsed 4495	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = 0)
300	239, 299	sylan9eqr 2786	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
301		simplr 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
302	292, 300, 301, 295	fvmptd 6957	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = 0)
303	291, 297, 302	3eqtr4d 2774	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
304	251, 303	pm2.61dan 812	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
305		elioore 13312	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
306	305	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
307	305, 25	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
308	306, 307, 28	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
309	308	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
310	91	iftrued 4492	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
311	309, 310	eqtrd 2764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (𝐺‘𝑠))
312	311	mpteq2dva 5195	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
313	214	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:ℝ⟶ℝ)
314		ioossre 13344	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
315	314	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
316	313, 315	feqresmpt 6912	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
317	212	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺:dom 𝐺⟶ℝ)
318	317, 94	feqresmpt 6912	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
319	312, 316, 318	3eqtr4d 2774	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
320	319, 81	eqeltrd 2828	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
321		eqid 2729	. . 3 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
322		oveq1 7376	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
323	322	eleq1d 2813	. . . . . . 7 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
324	323	rexbidv 3157	. . . . . 6 ⊢ (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
325	324	cbvrabv 3413	. . . . 5 ⊢ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
326	325	uneq2i 4124	. . . 4 ⊢ ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
327	326	eqcomi 2738	. . 3 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
328	54	fveq2i 6843	. . . 4 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
329	328	oveq1i 7379	. . 3 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
330		isoeq5 7278	. . . . . 6 ⊢ (({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}) → (𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))))
331	61, 330	ax-mp 5	. . . . 5 ⊢ (𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
332	331	iotabii 6484	. . . 4 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
333		isoeq1 7274	. . . . 5 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
334	333	cbviotavw 6460	. . . 4 ⊢ (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
335	332, 334, 65	3eqtr4ri 2763	. . 3 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
336		id 22	. . . . 5 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
337		oveq2 7377	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝐵 − 𝑣) = (𝐵 − 𝑥))
338	337	oveq1d 7384	. . . . . . 7 ⊢ (𝑣 = 𝑥 → ((𝐵 − 𝑣) / 𝑇) = ((𝐵 − 𝑥) / 𝑇))
339	338	fveq2d 6844	. . . . . 6 ⊢ (𝑣 = 𝑥 → (⌊‘((𝐵 − 𝑣) / 𝑇)) = (⌊‘((𝐵 − 𝑥) / 𝑇)))
340	339	oveq1d 7384	. . . . 5 ⊢ (𝑣 = 𝑥 → ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
341	336, 340	oveq12d 7387	. . . 4 ⊢ (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
342	341	cbvmptv 5206	. . 3 ⊢ (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
343		eqeq1 2733	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝐵 ↔ 𝑧 = 𝐵))
344		id 22	. . . . 5 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
345	343, 344	ifbieq2d 4511	. . . 4 ⊢ (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
346	345	cbvmptv 5206	. . 3 ⊢ (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
347		eqid 2729	. . 3 ⊢ ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
348		eqid 2729	. . 3 ⊢ (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
349		eqid 2729	. . 3 ⊢ (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
350		fveq2 6840	. . . . . . . 8 ⊢ (𝑖 = 𝑡 → (𝑄‘𝑖) = (𝑄‘𝑡))
351	350	breq1d 5112	. . . . . . 7 ⊢ (𝑖 = 𝑡 → ((𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
352	351	cbvrabv 3413	. . . . . 6 ⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
353		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))
354	353	fveq2d 6844	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
355	354	eqcomd 2735	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
356	355	breq2d 5114	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
357	356	rabbidv 3410	. . . . . 6 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
358	352, 357	eqtr2id 2777	. . . . 5 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
359	358	supeq1d 9373	. . . 4 ⊢ (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
360	359	cbvmptv 5206	. . 3 ⊢ (𝑤 ∈ ℝ ↦ sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < )) = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
361	31, 30, 32, 33, 217, 304, 320, 34, 35, 321, 327, 329, 335, 342, 346, 66, 347, 348, 349, 360	fourierdlem90 46167	. 2 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
362	216, 361	eqeltrd 2828	1 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = 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 dom cdm 5631 ran crn 5632 ↾ cres 5633 ℩cio 6450 Fun wfun 6493 ⟶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 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 − cmin 11381 -cneg 11382 / cdiv 11811 ℕcn 12162 ℤcz 12505 (,)cioo 13282 (,]cioc 13283 [,]cicc 13285 ...cfz 13444 ..^cfzo 13591 ⌊cfl 13728 ♯chash 14271 –cn→ccncf 24745 D cdv 25740

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

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-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-pm 8779 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-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-xnn0 12492 df-z 12506 df-dec 12626 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ioc 13287 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-fl 13730 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-struct 17093 df-slot 17128 df-ndx 17140 df-base 17156 df-plusg 17209 df-mulr 17210 df-starv 17211 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-rest 17361 df-topn 17362 df-topgen 17382 df-psmet 21232 df-xmet 21233 df-met 21234 df-bl 21235 df-mopn 21236 df-fbas 21237 df-fg 21238 df-cnfld 21241 df-top 22757 df-topon 22774 df-topsp 22796 df-bases 22809 df-cld 22882 df-ntr 22883 df-cls 22884 df-nei 22961 df-lp 22999 df-perf 23000 df-cn 23090 df-cnp 23091 df-haus 23178 df-cmp 23250 df-fil 23709 df-fm 23801 df-flim 23802 df-flf 23803 df-xms 24184 df-ms 24185 df-cncf 24747 df-limc 25743 df-dv 25744

This theorem is referenced by: fourierdlem112 46189

W3C validator