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 46774

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 13411	. . . . . . . 8 ⊢ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ)
3	2	sselda 3936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ ℝ)
4		iftrue 4486	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
5	4	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
6		fourierdlem97.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
7		ssid 3958	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ
8		dvfre 26010	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
9	6, 7, 8	sylancl 595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
10		fourierdlem97.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (ℝ D 𝐹)
11	10	feq1i 6682	. . . . . . . . . . . . 13 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
12	9, 11	sylibr 236	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
13	12	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
14		id 22	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom 𝐺)
15	10	dmeqi 5880	. . . . . . . . . . . . 13 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
16	14, 15	eleqtrdi 2872	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom (ℝ D 𝐹))
17	16	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝑠 ∈ dom (ℝ D 𝐹))
18	13, 17	ffvelcdmd 7066	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → (𝐺‘𝑠) ∈ ℝ)
19	5, 18	eqeltrd 2862	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
20	19	adantlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
21		iffalse 4489	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
22		0red 11184	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ)
23	21, 22	eqeltrd 2862	. . . . . . . . 9 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
24	23	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ ¬ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
25	20, 24	pm2.61dan 822	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
26	3, 25	syldan 600	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
27		fourierdlem97.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
28	27	fvmpt2 6987	. . . . . 6 ⊢ ((𝑠 ∈ ℝ ∧ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
29	3, 26, 28	syl2anc 593	. . . . 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 13379	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
38	34	rexrd 11232	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
39		pnfxr 11236	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
40	39	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → +∞ ∈ ℝ^*)
41		ioogtlb 46068	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
42	38, 40, 35, 41	syl3anc 1390	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 < 𝐷)
43		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 + (ℎ · 𝑇)) = (𝑥 + (ℎ · 𝑇)))
44	43	eleq1d 2847	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
45	44	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
46	45	cbvrabv 3424	. . . . . . . . . . 11 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄}
47	46	uneq2i 4118	. . . . . . . . . 10 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄})
48		oveq1 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
49	48	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
50	49	eleq1d 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
51	50	cbvrexvw 3241	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
52	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
53	52	rabbiia 3418	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
54	53	uneq2i 4118	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
55		oveq1 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 = ℎ → (𝑙 · 𝑇) = (ℎ · 𝑇))
56	55	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + (ℎ · 𝑇)))
57	56	eleq1d 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
58	57	cbvrexvw 3241	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄)
59	58	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
60	59	rabbiia 3418	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}
61	60	uneq2i 4118	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
62	54, 61	eqtri 2785	. . . . . . . . . . . 12 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
63	62	fveq2i 6870	. . . . . . . . . . 11 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))
64	63	oveq1i 7406	. . . . . . . . . 10 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})) − 1)
65		fourierdlem97.v	. . . . . . . . . 10 ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
66		fourierdlem97.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
67		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ℎ → (𝑘 · 𝑇) = (ℎ · 𝑇))
68	67	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ (𝑘 = ℎ → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (ℎ · 𝑇)))
69	68	breq1d 5110	. . . . . . . . . . . 12 ⊢ (𝑘 = ℎ → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)))
70	69	cbvrabv 3424	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} = {ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}
71	70	supeq1i 9393	. . . . . . . . . 10 ⊢ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
72		fveq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑒 → (𝑄‘𝑗) = (𝑄‘𝑒))
73	72	oveq1d 7411	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑒 → ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) = ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)))
74	73	breq1d 5110	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑒 → (((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)))
75	74	cbvrabv 3424	. . . . . . . . . . 11 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)} = {𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}
76	75	supeq1i 9393	. . . . . . . . . 10 ⊢ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
77	30, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76	fourierdlem64 46741	. . . . . . . . 9 ⊢ (𝜑 → ((sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀) ∧ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
78	77	simprd 499	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
79		simpl1 1205	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝜑)
80		simpl2l 1240	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑖 ∈ (0..^𝑀))
81		fourierdlem97.qcn	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
82		cncff 24952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
84		ffun 6694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ → Fun 𝐺)
85	12, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun 𝐺)
86	85	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → Fun 𝐺)
87		ffvresb 7107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun 𝐺 → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ)))
88	86, 87	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ)))
89	83, 88	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
90	89	r19.21bi 3254	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
91	90	simpld 498	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ dom 𝐺)
92	91	ralrimiva 3154	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
93		dfss3 3925	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
94	92, 93	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
95	79, 80, 94	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
96		simpl2 1206	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ))
97	79, 96	jca 519	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)))
98		simpl3 1207	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
99		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
100	98, 99	sseldd 3937	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
101	31	fourierdlem2 46680	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
102	32, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
103	33, 102	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
104	103	simpld 498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
105		elmapi 8830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
107	106	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
108		elfzofz 13681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
109	108	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
110	107, 109	ffvelcdmd 7066	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
111	110	rexrd 11232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
112	111	adantrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ^*)
113	112	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ^*)
114		fzofzp1 13770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
115	114	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
116	107, 115	ffvelcdmd 7066	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
117	116	adantrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
118	117	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
119	118	rexrd 11232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
120		elioore 13379	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → 𝑡 ∈ ℝ)
121	120	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ ℝ)
122		zre 12572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℝ)
123	122	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
124	123	ad2antlr 737	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑙 ∈ ℝ)
125		fourierdlem97.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
126		fourierdlem97.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
127	125, 126	resubcld 11615	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
128	30, 127	eqeltrid 2866	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
129	128	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑇 ∈ ℝ)
130	124, 129	remulcld 11212	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑙 · 𝑇) ∈ ℝ)
131	121, 130	resubcld 11615	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ℝ)
132	110	adantrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ)
133	122	ad2antll 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑙 ∈ ℝ)
134	128	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑇 ∈ ℝ)
135	133, 134	remulcld 11212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑙 · 𝑇) ∈ ℝ)
136	132, 135	readdcld 11211	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ)
137	136	rexrd 11232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
138	137	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
139	117, 135	readdcld 11211	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ)
140	139	rexrd 11232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
141	140	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
142		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
143		ioogtlb 46068	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
144	138, 141, 142, 143	syl3anc 1390	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
145	132	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ)
146	145, 130, 121	ltaddsubd 11787	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡 ↔ (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇))))
147	144, 146	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇)))
148		iooltub 46083	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
149	138, 141, 142, 148	syl3anc 1390	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
150	121, 130, 118	ltsubaddd 11783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)) ↔ 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
151	149, 150	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)))
152	113, 119, 131, 147, 151	eliood 46071	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
153	97, 100, 152	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
154	95, 153	sseldd 3937	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)
155		elioore 13379	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑡 ∈ ℝ)
156		recn 11163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
157	156	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
158		zcn 12573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℂ)
159	158	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑙 ∈ ℂ)
160	128	recnd 11210	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ ℂ)
161	160	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℂ)
162	159, 161	mulcld 11202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝑙 · 𝑇) ∈ ℂ)
163	157, 162	npcand 11546	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) = 𝑡)
164	163	eqcomd 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
165	164	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
166		ovex 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 − (𝑙 · 𝑇)) ∈ V
167		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 ∈ dom 𝐺 ↔ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺))
168	167	anbi2d 639	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) ↔ ((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)))
169		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 + (𝑙 · 𝑇)) = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
170	169	eleq1d 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ↔ ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺))
171	169	fveq2d 6871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))))
172		fveq2 6867	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘𝑠) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))
173	171, 172	eqeq12d 2778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠) ↔ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
174	170, 173	anbi12d 641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)) ↔ (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))))
175	168, 174	imbi12d 346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠))) ↔ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))))
176		ax-resscn 11130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℂ
177	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ⊆ ℂ)
178	6, 177	fssd 6709	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
179	178	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
180	122	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
181	128	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑇 ∈ ℝ)
182	180, 181	remulcld 11212	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → (𝑙 · 𝑇) ∈ ℝ)
183	178	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
184	128	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
185		simplr 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑙 ∈ ℤ)
186		simpr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
187		fourierdlem97.fper	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
188	187	ad4ant14 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
189	183, 184, 185, 186, 188	fperiodmul 45880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → (𝐹‘(𝑠 + (𝑙 · 𝑇))) = (𝐹‘𝑠))
190	179, 182, 189, 10	fperdvper 46490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)))
191	166, 175, 190	vtocl 3525	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
192	191	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
193	192	adantlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
194	165, 193	eqeltrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 ∈ dom 𝐺)
195	194	ex 416	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
196	155, 195	sylan2 602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
197	196	adantlrl 730	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
198	197	3adantl3 1182	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
199	154, 198	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ dom 𝐺)
200	199	ralrimiva 3154	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
201		dfss3 3925	. . . . . . . . . . 11 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺 ↔ ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
202	200, 201	sylibr 236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
203	202	3exp 1132	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)))
204	203	rexlimdvv 3218	. . . . . . . 8 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺))
205	78, 204	mpd 15	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
206	205	sselda 3936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ dom 𝐺)
207	206	iftrued 4488	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
208	29, 207	eqtr2d 2798	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐺‘𝑠) = (𝐻‘𝑠))
209	208	mpteq2dva 5193	. . 3 ⊢ (𝜑 → (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
210	15	a1i 11	. . . . . 6 ⊢ (𝜑 → dom 𝐺 = dom (ℝ D 𝐹))
211	210	feq2d 6675	. . . . 5 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
212	12, 211	mpbird 259	. . . 4 ⊢ (𝜑 → 𝐺:dom 𝐺⟶ℝ)
213	212, 205	feqresmpt 6936	. . 3 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)))
214	25, 27	fmptd 7095	. . . 4 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
215	214, 2	feqresmpt 6936	. . 3 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
216	209, 213, 215	3eqtr4d 2807	. 2 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))))
217	214, 177	fssd 6709	. . 3 ⊢ (𝜑 → 𝐻:ℝ⟶ℂ)
218	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
219		eleq1 2850	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝑠 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
220		fveq2 6867	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝐺‘𝑠) = (𝐺‘(𝑥 + 𝑇)))
221	219, 220	ifbieq1d 4505	. . . . . . . 8 ⊢ (𝑠 = (𝑥 + 𝑇) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
222	178, 128, 187, 10	fperdvper 46490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))
223	222	simpld 498	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
224	223	iftrued 4488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = (𝐺‘(𝑥 + 𝑇)))
225	221, 224	sylan9eqr 2819	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
226	225	adantllr 729	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
227		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
228	128	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229	227, 228	readdcld 11211	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℝ)
230	229	adantr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
231	212	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐺:dom 𝐺⟶ℝ)
232	223	adantlr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
233	231, 232	ffvelcdmd 7066	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) ∈ ℝ)
234	218, 226, 230, 233	fvmptd 6983	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
235	222	simprd 499	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
236	235	adantlr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
237		eleq1 2850	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝑠 ∈ dom 𝐺 ↔ 𝑥 ∈ dom 𝐺))
238		fveq2 6867	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝐺‘𝑠) = (𝐺‘𝑥))
239	237, 238	ifbieq1d 4505	. . . . . . . 8 ⊢ (𝑠 = 𝑥 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
240	239	adantl 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
241		simplr 778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
242		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
243	242	iftrued 4488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
244	212	ffvelcdmda 7065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℝ)
245	243, 244	eqeltrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
246	245	adantlr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
247	218, 240, 241, 246	fvmptd 6983	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
248		simpr 488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
249	248	iftrued 4488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
250	247, 249	eqtr2d 2798	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐻‘𝑥))
251	234, 236, 250	3eqtrd 2801	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
252	229	recnd 11210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℂ)
253	228	recnd 11210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
254	252, 253	negsubd 11548	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) + -𝑇) = ((𝑥 + 𝑇) − 𝑇))
255	227	recnd 11210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
256	255, 253	pncand 11543	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
257	254, 256	eqtr2d 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
258	257	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
259		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
260		simpll 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝜑)
261	260, 259	jca 519	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺))
262		eleq1 2850	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
263	262	anbi2d 639	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝜑 ∧ 𝑦 ∈ dom 𝐺) ↔ (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺)))
264		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 + -𝑇) = ((𝑥 + 𝑇) + -𝑇))
265	264	eleq1d 2847	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝑦 + -𝑇) ∈ dom 𝐺 ↔ ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺))
266	264	fveq2d 6871	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘(𝑦 + -𝑇)) = (𝐺‘((𝑥 + 𝑇) + -𝑇)))
267		fveq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘𝑦) = (𝐺‘(𝑥 + 𝑇)))
268	266, 267	eqeq12d 2778	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦) ↔ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
269	265, 268	anbi12d 641	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)) ↔ (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
270	263, 269	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦))) ↔ ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))))
271	128	renegcld 11614	. . . . . . . . . . . 12 ⊢ (𝜑 → -𝑇 ∈ ℝ)
272	160	mulm1d 11639	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-1 · 𝑇) = -𝑇)
273	272	eqcomd 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -𝑇 = (-1 · 𝑇))
274	273	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -𝑇 = (-1 · 𝑇))
275	274	oveq2d 7412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + -𝑇) = (𝑦 + (-1 · 𝑇)))
276	275	fveq2d 6871	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘(𝑦 + (-1 · 𝑇))))
277	178	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
278	128	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
279		1zzd 12602	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℤ)
280	279	znegcld 12679	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -1 ∈ ℤ)
281		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
282	187	adantlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
283	277, 278, 280, 281, 282	fperiodmul 45880	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + (-1 · 𝑇))) = (𝐹‘𝑦))
284	276, 283	eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘𝑦))
285	178, 271, 284, 10	fperdvper 46490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)))
286	270, 285	vtoclg 3522	. . . . . . . . . 10 ⊢ ((𝑥 + 𝑇) ∈ dom 𝐺 → ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
287	259, 261, 286	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
288	287	simpld 498	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺)
289	258, 288	eqeltrd 2862	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
290	289	stoic1a 1792	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ (𝑥 + 𝑇) ∈ dom 𝐺)
291	290	iffalsed 4491	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = 0)
292	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
293	221	adantl 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
294	229	adantr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
295		0red 11184	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 0 ∈ ℝ)
296	291, 295	eqeltrd 2862	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) ∈ ℝ)
297	292, 293, 294, 296	fvmptd 6983	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
298		simpr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ 𝑥 ∈ dom 𝐺)
299	298	iffalsed 4491	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = 0)
300	239, 299	sylan9eqr 2819	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
301		simplr 778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
302	292, 300, 301, 295	fvmptd 6983	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = 0)
303	291, 297, 302	3eqtr4d 2807	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
304	251, 303	pm2.61dan 822	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
305		elioore 13379	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
306	305	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
307	305, 25	sylan2 602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
308	306, 307, 28	syl2anc 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
309	308	adantlr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
310	91	iftrued 4488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
311	309, 310	eqtrd 2797	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (𝐺‘𝑠))
312	311	mpteq2dva 5193	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
313	214	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:ℝ⟶ℝ)
314		ioossre 13411	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
315	314	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
316	313, 315	feqresmpt 6936	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
317	212	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺:dom 𝐺⟶ℝ)
318	317, 94	feqresmpt 6936	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
319	312, 316, 318	3eqtr4d 2807	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
320	319, 81	eqeltrd 2862	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
321		eqid 2762	. . 3 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
322		oveq1 7403	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
323	322	eleq1d 2847	. . . . . . 7 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
324	323	rexbidv 3186	. . . . . 6 ⊢ (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
325	324	cbvrabv 3424	. . . . 5 ⊢ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
326	325	uneq2i 4118	. . . 4 ⊢ ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
327	326	eqcomi 2771	. . 3 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
328	54	fveq2i 6870	. . . 4 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
329	328	oveq1i 7406	. . 3 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
330		isoeq5 7305	. . . . . 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 6506	. . . 4 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
333		isoeq1 7301	. . . . 5 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
334	333	cbviotavw 6485	. . . 4 ⊢ (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
335	332, 334, 65	3eqtr4ri 2796	. . 3 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
336		id 22	. . . . 5 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
337		oveq2 7404	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝐵 − 𝑣) = (𝐵 − 𝑥))
338	337	oveq1d 7411	. . . . . . 7 ⊢ (𝑣 = 𝑥 → ((𝐵 − 𝑣) / 𝑇) = ((𝐵 − 𝑥) / 𝑇))
339	338	fveq2d 6871	. . . . . 6 ⊢ (𝑣 = 𝑥 → (⌊‘((𝐵 − 𝑣) / 𝑇)) = (⌊‘((𝐵 − 𝑥) / 𝑇)))
340	339	oveq1d 7411	. . . . 5 ⊢ (𝑣 = 𝑥 → ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
341	336, 340	oveq12d 7414	. . . 4 ⊢ (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
342	341	cbvmptv 5204	. . 3 ⊢ (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
343		eqeq1 2766	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝐵 ↔ 𝑧 = 𝐵))
344		id 22	. . . . 5 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
345	343, 344	ifbieq2d 4507	. . . 4 ⊢ (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
346	345	cbvmptv 5204	. . 3 ⊢ (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
347		eqid 2762	. . 3 ⊢ ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
348		eqid 2762	. . 3 ⊢ (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
349		eqid 2762	. . 3 ⊢ (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
350		fveq2 6867	. . . . . . . 8 ⊢ (𝑖 = 𝑡 → (𝑄‘𝑖) = (𝑄‘𝑡))
351	350	breq1d 5110	. . . . . . 7 ⊢ (𝑖 = 𝑡 → ((𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
352	351	cbvrabv 3424	. . . . . 6 ⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
353		fveq2 6867	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))
354	353	fveq2d 6871	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
355	354	eqcomd 2768	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
356	355	breq2d 5112	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
357	356	rabbidv 3421	. . . . . 6 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
358	352, 357	eqtr2id 2810	. . . . 5 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
359	358	supeq1d 9392	. . . 4 ⊢ (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
360	359	cbvmptv 5204	. . 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 46767	. 2 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
362	216, 361	eqeltrd 2862	1 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 ∀wral 3076 ∃wrex 3086 {crab 3414 ∪ cun 3902 ⊆ wss 3904 ifcif 4480 {cpr 4584 class class class wbr 5100 ↦ cmpt 5181 dom cdm 5647 ran crn 5648 ↾ cres 5649 ℩cio 6475 Fun wfun 6515 ⟶wf 6517 ‘cfv 6521 Isom wiso 6522 (class class class)co 7396 ↑_m cmap 8808 supcsup 9386 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 +∞cpnf 11213 ℝ^*cxr 11215 < clt 11216 ≤ cle 11217 − cmin 11414 -cneg 11415 / cdiv 11844 ℕcn 12210 ℤcz 12568 (,)cioo 13349 (,]cioc 13350 [,]cicc 13352 ...cfz 13512 ..^cfzo 13659 ⌊cfl 13800 ♯chash 14343 –cn→ccncf 24935 D cdv 25922

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-inf2 9596 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8678 df-map 8810 df-pm 8811 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fi 9357 df-sup 9388 df-inf 9389 df-oi 9458 df-dju 9859 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-xnn0 12555 df-z 12569 df-dec 12689 df-uz 12840 df-q 12950 df-rp 12994 df-xneg 13114 df-xadd 13115 df-xmul 13116 df-ioo 13353 df-ioc 13354 df-ico 13355 df-icc 13356 df-fz 13513 df-fzo 13660 df-fl 13802 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-struct 17183 df-slot 17218 df-ndx 17230 df-base 17246 df-plusg 17299 df-mulr 17300 df-starv 17301 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-rest 17451 df-topn 17452 df-topgen 17472 df-psmet 21413 df-xmet 21414 df-met 21415 df-bl 21416 df-mopn 21417 df-fbas 21418 df-fg 21419 df-cnfld 21422 df-top 22951 df-topon 22968 df-topsp 22990 df-bases 23003 df-cld 23076 df-ntr 23077 df-cls 23078 df-nei 23155 df-lp 23193 df-perf 23194 df-cn 23284 df-cnp 23285 df-haus 23372 df-cmp 23444 df-fil 23903 df-fm 23995 df-flim 23996 df-flf 23997 df-xms 24377 df-ms 24378 df-cncf 24937 df-limc 25925 df-dv 25926

This theorem is referenced by: fourierdlem112 46789

W3C validator