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 42482

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 12792	. . . . . . . 8 ⊢ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ)
3	2	sselda 3966	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ ℝ)
4		iftrue 4472	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
5	4	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
6		fourierdlem97.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
7		ssid 3988	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ
8		dvfre 24542	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
9	6, 7, 8	sylancl 588	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
10		fourierdlem97.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (ℝ D 𝐹)
11	10	feq1i 6499	. . . . . . . . . . . . 13 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
12	9, 11	sylibr 236	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
13	12	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
14		id 22	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom 𝐺)
15	10	dmeqi 5767	. . . . . . . . . . . . 13 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
16	14, 15	eleqtrdi 2923	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom (ℝ D 𝐹))
17	16	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝑠 ∈ dom (ℝ D 𝐹))
18	13, 17	ffvelrnd 6846	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → (𝐺‘𝑠) ∈ ℝ)
19	5, 18	eqeltrd 2913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
20	19	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
21		iffalse 4475	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
22		0red 10638	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ)
23	21, 22	eqeltrd 2913	. . . . . . . . 9 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
24	23	adantl 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ ¬ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
25	20, 24	pm2.61dan 811	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
26	3, 25	syldan 593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
27		fourierdlem97.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
28	27	fvmpt2 6773	. . . . . 6 ⊢ ((𝑠 ∈ ℝ ∧ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
29	3, 26, 28	syl2anc 586	. . . . 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 12762	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
38	34	rexrd 10685	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
39		pnfxr 10689	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
40	39	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → +∞ ∈ ℝ^*)
41		ioogtlb 41763	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
42	38, 40, 35, 41	syl3anc 1367	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 < 𝐷)
43		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 + (ℎ · 𝑇)) = (𝑥 + (ℎ · 𝑇)))
44	43	eleq1d 2897	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
45	44	rexbidv 3297	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
46	45	cbvrabv 3491	. . . . . . . . . . 11 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄}
47	46	uneq2i 4135	. . . . . . . . . 10 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄})
48		oveq1 7157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
49	48	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
50	49	eleq1d 2897	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
51	50	cbvrexvw 3450	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
52	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
53	52	rabbiia 3472	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
54	53	uneq2i 4135	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
55		oveq1 7157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 = ℎ → (𝑙 · 𝑇) = (ℎ · 𝑇))
56	55	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + (ℎ · 𝑇)))
57	56	eleq1d 2897	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
58	57	cbvrexvw 3450	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄)
59	58	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
60	59	rabbiia 3472	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}
61	60	uneq2i 4135	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
62	54, 61	eqtri 2844	. . . . . . . . . . . 12 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
63	62	fveq2i 6667	. . . . . . . . . . 11 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))
64	63	oveq1i 7160	. . . . . . . . . 10 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})) − 1)
65		fourierdlem97.v	. . . . . . . . . 10 ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
66		fourierdlem97.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
67		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ℎ → (𝑘 · 𝑇) = (ℎ · 𝑇))
68	67	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (𝑘 = ℎ → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (ℎ · 𝑇)))
69	68	breq1d 5068	. . . . . . . . . . . 12 ⊢ (𝑘 = ℎ → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)))
70	69	cbvrabv 3491	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} = {ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}
71	70	supeq1i 8905	. . . . . . . . . 10 ⊢ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
72		fveq2 6664	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑒 → (𝑄‘𝑗) = (𝑄‘𝑒))
73	72	oveq1d 7165	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑒 → ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) = ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)))
74	73	breq1d 5068	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑒 → (((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)))
75	74	cbvrabv 3491	. . . . . . . . . . 11 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)} = {𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}
76	75	supeq1i 8905	. . . . . . . . . 10 ⊢ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
77	30, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76	fourierdlem64 42449	. . . . . . . . 9 ⊢ (𝜑 → ((sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀) ∧ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
78	77	simprd 498	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
79		simpl1 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝜑)
80		simpl2l 1222	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑖 ∈ (0..^𝑀))
81		fourierdlem97.qcn	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
82		cncff 23495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
84		ffun 6511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ → Fun 𝐺)
85	12, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun 𝐺)
86	85	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → Fun 𝐺)
87		ffvresb 6882	. . . . . . . . . . . . . . . . . . . . 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 3208	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
91	90	simpld 497	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ dom 𝐺)
92	91	ralrimiva 3182	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
93		dfss3 3955	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
94	92, 93	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
95	79, 80, 94	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
96		simpl2 1188	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ))
97	79, 96	jca 514	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)))
98		simpl3 1189	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
99		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
100	98, 99	sseldd 3967	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
101	31	fourierdlem2 42388	. . . . . . . . . . . . . . . . . . . . . . . . 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 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
105		elmapi 8422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
107	106	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
108		elfzofz 13047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
109	108	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
110	107, 109	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
111	110	rexrd 10685	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
112	111	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ^*)
113	112	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ^*)
114		fzofzp1 13128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
115	114	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
116	107, 115	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
117	116	adantrr 715	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
118	117	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
119	118	rexrd 10685	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
120		elioore 12762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → 𝑡 ∈ ℝ)
121	120	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ ℝ)
122		zre 11979	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℝ)
123	122	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
124	123	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑙 ∈ ℝ)
125		fourierdlem97.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
126		fourierdlem97.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
127	125, 126	resubcld 11062	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
128	30, 127	eqeltrid 2917	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
129	128	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑇 ∈ ℝ)
130	124, 129	remulcld 10665	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑙 · 𝑇) ∈ ℝ)
131	121, 130	resubcld 11062	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ℝ)
132	110	adantrr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ)
133	122	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑙 ∈ ℝ)
134	128	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑇 ∈ ℝ)
135	133, 134	remulcld 10665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑙 · 𝑇) ∈ ℝ)
136	132, 135	readdcld 10664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ)
137	136	rexrd 10685	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
138	137	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
139	117, 135	readdcld 10664	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ)
140	139	rexrd 10685	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
141	140	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
142		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
143		ioogtlb 41763	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
144	138, 141, 142, 143	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
145	132	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ)
146	145, 130, 121	ltaddsubd 11234	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡 ↔ (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇))))
147	144, 146	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇)))
148		iooltub 41779	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
149	138, 141, 142, 148	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
150	121, 130, 118	ltsubaddd 11230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)) ↔ 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
151	149, 150	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)))
152	113, 119, 131, 147, 151	eliood 41766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
153	97, 100, 152	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
154	95, 153	sseldd 3967	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)
155		elioore 12762	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑡 ∈ ℝ)
156		recn 10621	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
157	156	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
158		zcn 11980	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℂ)
159	158	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑙 ∈ ℂ)
160	128	recnd 10663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ ℂ)
161	160	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℂ)
162	159, 161	mulcld 10655	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝑙 · 𝑇) ∈ ℂ)
163	157, 162	npcand 10995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) = 𝑡)
164	163	eqcomd 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
165	164	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
166		ovex 7183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 − (𝑙 · 𝑇)) ∈ V
167		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 ∈ dom 𝐺 ↔ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺))
168	167	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) ↔ ((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)))
169		oveq1 7157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 + (𝑙 · 𝑇)) = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
170	169	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ↔ ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺))
171	169	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))))
172		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘𝑠) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))
173	171, 172	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠) ↔ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
174	170, 173	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)) ↔ (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))))
175	168, 174	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠))) ↔ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))))
176		ax-resscn 10588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℂ
177	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ⊆ ℂ)
178	6, 177	fssd 6522	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
179	178	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
180	122	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
181	128	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑇 ∈ ℝ)
182	180, 181	remulcld 10665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → (𝑙 · 𝑇) ∈ ℝ)
183	178	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
184	128	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
185		simplr 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑙 ∈ ℤ)
186		simpr 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
187		fourierdlem97.fper	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
188	187	ad4ant14 750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
189	183, 184, 185, 186, 188	fperiodmul 41564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → (𝐹‘(𝑠 + (𝑙 · 𝑇))) = (𝐹‘𝑠))
190	179, 182, 189, 10	fperdvper 42196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)))
191	166, 175, 190	vtocl 3559	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
192	191	simpld 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
193	192	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
194	165, 193	eqeltrd 2913	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 ∈ dom 𝐺)
195	194	ex 415	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
196	155, 195	sylan2 594	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
197	196	adantlrl 718	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
198	197	3adantl3 1164	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
199	154, 198	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ dom 𝐺)
200	199	ralrimiva 3182	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
201		dfss3 3955	. . . . . . . . . . 11 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺 ↔ ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
202	200, 201	sylibr 236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
203	202	3exp 1115	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)))
204	203	rexlimdvv 3293	. . . . . . . 8 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺))
205	78, 204	mpd 15	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
206	205	sselda 3966	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ dom 𝐺)
207	206	iftrued 4474	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
208	29, 207	eqtr2d 2857	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐺‘𝑠) = (𝐻‘𝑠))
209	208	mpteq2dva 5153	. . 3 ⊢ (𝜑 → (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
210	15	a1i 11	. . . . . 6 ⊢ (𝜑 → dom 𝐺 = dom (ℝ D 𝐹))
211	210	feq2d 6494	. . . . 5 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
212	12, 211	mpbird 259	. . . 4 ⊢ (𝜑 → 𝐺:dom 𝐺⟶ℝ)
213	212, 205	feqresmpt 6728	. . 3 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)))
214	25, 27	fmptd 6872	. . . 4 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
215	214, 2	feqresmpt 6728	. . 3 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
216	209, 213, 215	3eqtr4d 2866	. 2 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))))
217	214, 177	fssd 6522	. . 3 ⊢ (𝜑 → 𝐻:ℝ⟶ℂ)
218	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
219		eleq1 2900	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝑠 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
220		fveq2 6664	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝐺‘𝑠) = (𝐺‘(𝑥 + 𝑇)))
221	219, 220	ifbieq1d 4489	. . . . . . . 8 ⊢ (𝑠 = (𝑥 + 𝑇) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
222	178, 128, 187, 10	fperdvper 42196	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))
223	222	simpld 497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
224	223	iftrued 4474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = (𝐺‘(𝑥 + 𝑇)))
225	221, 224	sylan9eqr 2878	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
226	225	adantllr 717	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
227		simpr 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
228	128	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229	227, 228	readdcld 10664	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℝ)
230	229	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
231	212	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐺:dom 𝐺⟶ℝ)
232	223	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
233	231, 232	ffvelrnd 6846	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) ∈ ℝ)
234	218, 226, 230, 233	fvmptd 6769	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
235	222	simprd 498	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
236	235	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
237		eleq1 2900	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝑠 ∈ dom 𝐺 ↔ 𝑥 ∈ dom 𝐺))
238		fveq2 6664	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝐺‘𝑠) = (𝐺‘𝑥))
239	237, 238	ifbieq1d 4489	. . . . . . . 8 ⊢ (𝑠 = 𝑥 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
240	239	adantl 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
241		simplr 767	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
242		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
243	242	iftrued 4474	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
244	212	ffvelrnda 6845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℝ)
245	243, 244	eqeltrd 2913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
246	245	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
247	218, 240, 241, 246	fvmptd 6769	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
248		simpr 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
249	248	iftrued 4474	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
250	247, 249	eqtr2d 2857	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐻‘𝑥))
251	234, 236, 250	3eqtrd 2860	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
252	229	recnd 10663	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℂ)
253	228	recnd 10663	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
254	252, 253	negsubd 10997	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) + -𝑇) = ((𝑥 + 𝑇) − 𝑇))
255	227	recnd 10663	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
256	255, 253	pncand 10992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
257	254, 256	eqtr2d 2857	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
258	257	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
259		simpr 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
260		simpll 765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝜑)
261	260, 259	jca 514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺))
262		eleq1 2900	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
263	262	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝜑 ∧ 𝑦 ∈ dom 𝐺) ↔ (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺)))
264		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 + -𝑇) = ((𝑥 + 𝑇) + -𝑇))
265	264	eleq1d 2897	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝑦 + -𝑇) ∈ dom 𝐺 ↔ ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺))
266	264	fveq2d 6668	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘(𝑦 + -𝑇)) = (𝐺‘((𝑥 + 𝑇) + -𝑇)))
267		fveq2 6664	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘𝑦) = (𝐺‘(𝑥 + 𝑇)))
268	266, 267	eqeq12d 2837	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦) ↔ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
269	265, 268	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)) ↔ (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
270	263, 269	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦))) ↔ ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))))
271	128	renegcld 11061	. . . . . . . . . . . 12 ⊢ (𝜑 → -𝑇 ∈ ℝ)
272	160	mulm1d 11086	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-1 · 𝑇) = -𝑇)
273	272	eqcomd 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -𝑇 = (-1 · 𝑇))
274	273	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -𝑇 = (-1 · 𝑇))
275	274	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + -𝑇) = (𝑦 + (-1 · 𝑇)))
276	275	fveq2d 6668	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘(𝑦 + (-1 · 𝑇))))
277	178	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
278	128	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
279		1zzd 12007	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℤ)
280	279	znegcld 12083	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -1 ∈ ℤ)
281		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
282	187	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
283	277, 278, 280, 281, 282	fperiodmul 41564	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + (-1 · 𝑇))) = (𝐹‘𝑦))
284	276, 283	eqtrd 2856	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘𝑦))
285	178, 271, 284, 10	fperdvper 42196	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)))
286	270, 285	vtoclg 3567	. . . . . . . . . 10 ⊢ ((𝑥 + 𝑇) ∈ dom 𝐺 → ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
287	259, 261, 286	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
288	287	simpld 497	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺)
289	258, 288	eqeltrd 2913	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
290	289	stoic1a 1769	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ (𝑥 + 𝑇) ∈ dom 𝐺)
291	290	iffalsed 4477	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = 0)
292	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
293	221	adantl 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
294	229	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
295		0red 10638	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 0 ∈ ℝ)
296	291, 295	eqeltrd 2913	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) ∈ ℝ)
297	292, 293, 294, 296	fvmptd 6769	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
298		simpr 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ 𝑥 ∈ dom 𝐺)
299	298	iffalsed 4477	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = 0)
300	239, 299	sylan9eqr 2878	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
301		simplr 767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
302	292, 300, 301, 295	fvmptd 6769	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = 0)
303	291, 297, 302	3eqtr4d 2866	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
304	251, 303	pm2.61dan 811	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
305		elioore 12762	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
306	305	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
307	305, 25	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
308	306, 307, 28	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
309	308	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
310	91	iftrued 4474	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
311	309, 310	eqtrd 2856	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (𝐺‘𝑠))
312	311	mpteq2dva 5153	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
313	214	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:ℝ⟶ℝ)
314		ioossre 12792	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
315	314	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
316	313, 315	feqresmpt 6728	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
317	212	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺:dom 𝐺⟶ℝ)
318	317, 94	feqresmpt 6728	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
319	312, 316, 318	3eqtr4d 2866	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
320	319, 81	eqeltrd 2913	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
321		eqid 2821	. . 3 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
322		oveq1 7157	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
323	322	eleq1d 2897	. . . . . . 7 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
324	323	rexbidv 3297	. . . . . 6 ⊢ (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
325	324	cbvrabv 3491	. . . . 5 ⊢ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
326	325	uneq2i 4135	. . . 4 ⊢ ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
327	326	eqcomi 2830	. . 3 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
328	54	fveq2i 6667	. . . 4 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
329	328	oveq1i 7160	. . 3 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
330		isoeq5 7068	. . . . . 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 6334	. . . 4 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
333		isoeq1 7064	. . . . 5 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
334	333	cbviotavw 6316	. . . 4 ⊢ (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
335	332, 334, 65	3eqtr4ri 2855	. . 3 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
336		id 22	. . . . 5 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
337		oveq2 7158	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝐵 − 𝑣) = (𝐵 − 𝑥))
338	337	oveq1d 7165	. . . . . . 7 ⊢ (𝑣 = 𝑥 → ((𝐵 − 𝑣) / 𝑇) = ((𝐵 − 𝑥) / 𝑇))
339	338	fveq2d 6668	. . . . . 6 ⊢ (𝑣 = 𝑥 → (⌊‘((𝐵 − 𝑣) / 𝑇)) = (⌊‘((𝐵 − 𝑥) / 𝑇)))
340	339	oveq1d 7165	. . . . 5 ⊢ (𝑣 = 𝑥 → ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
341	336, 340	oveq12d 7168	. . . 4 ⊢ (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
342	341	cbvmptv 5161	. . 3 ⊢ (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
343		eqeq1 2825	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝐵 ↔ 𝑧 = 𝐵))
344		id 22	. . . . 5 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
345	343, 344	ifbieq2d 4491	. . . 4 ⊢ (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
346	345	cbvmptv 5161	. . 3 ⊢ (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
347		eqid 2821	. . 3 ⊢ ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
348		eqid 2821	. . 3 ⊢ (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
349		eqid 2821	. . 3 ⊢ (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
350		fveq2 6664	. . . . . . . 8 ⊢ (𝑖 = 𝑡 → (𝑄‘𝑖) = (𝑄‘𝑡))
351	350	breq1d 5068	. . . . . . 7 ⊢ (𝑖 = 𝑡 → ((𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
352	351	cbvrabv 3491	. . . . . 6 ⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
353		fveq2 6664	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))
354	353	fveq2d 6668	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
355	354	eqcomd 2827	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
356	355	breq2d 5070	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
357	356	rabbidv 3480	. . . . . 6 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
358	352, 357	syl5req 2869	. . . . 5 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
359	358	supeq1d 8904	. . . 4 ⊢ (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
360	359	cbvmptv 5161	. . 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 42475	. 2 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
362	216, 361	eqeltrd 2913	1 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 {crab 3142 ∪ cun 3933 ⊆ wss 3935 ifcif 4466 {cpr 4562 class class class wbr 5058 ↦ cmpt 5138 dom cdm 5549 ran crn 5550 ↾ cres 5551 ℩cio 6306 Fun wfun 6343 ⟶wf 6345 ‘cfv 6349 Isom wiso 6350 (class class class)co 7150 ↑_m cmap 8400 supcsup 8898 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 +∞cpnf 10666 ℝ^*cxr 10668 < clt 10669 ≤ cle 10670 − cmin 10864 -cneg 10865 / cdiv 11291 ℕcn 11632 ℤcz 11975 (,)cioo 12732 (,]cioc 12733 [,]cicc 12735 ...cfz 12886 ..^cfzo 13027 ⌊cfl 13154 ♯chash 13684 –cn→ccncf 23478 D cdv 24455

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-iin 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-se 5509 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-isom 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-map 8402 df-pm 8403 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-fi 8869 df-sup 8900 df-inf 8901 df-oi 8968 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-4 11696 df-5 11697 df-6 11698 df-7 11699 df-8 11700 df-9 11701 df-n0 11892 df-xnn0 11962 df-z 11976 df-dec 12093 df-uz 12238 df-q 12343 df-rp 12384 df-xneg 12501 df-xadd 12502 df-xmul 12503 df-ioo 12736 df-ioc 12737 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-fl 13156 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-struct 16479 df-ndx 16480 df-slot 16481 df-base 16483 df-plusg 16572 df-mulr 16573 df-starv 16574 df-tset 16578 df-ple 16579 df-ds 16581 df-unif 16582 df-rest 16690 df-topn 16691 df-topgen 16711 df-psmet 20531 df-xmet 20532 df-met 20533 df-bl 20534 df-mopn 20535 df-fbas 20536 df-fg 20537 df-cnfld 20540 df-top 21496 df-topon 21513 df-topsp 21535 df-bases 21548 df-cld 21621 df-ntr 21622 df-cls 21623 df-nei 21700 df-lp 21738 df-perf 21739 df-cn 21829 df-cnp 21830 df-haus 21917 df-cmp 21989 df-fil 22448 df-fm 22540 df-flim 22541 df-flf 22542 df-xms 22924 df-ms 22925 df-cncf 23480 df-limc 24458 df-dv 24459

This theorem is referenced by: fourierdlem112 42497

W3C validator