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 43744

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 13140	. . . . . . . 8 ⊢ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ)
3	2	sselda 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ ℝ)
4		iftrue 4465	. . . . . . . . . . 11 ⊢ (𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
5	4	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
6		fourierdlem97.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
7		ssid 3943	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℝ
8		dvfre 25115	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
10		fourierdlem97.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (ℝ D 𝐹)
11	10	feq1i 6591	. . . . . . . . . . . . 13 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
12	9, 11	sylibr 233	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
13	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
14		id 22	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom 𝐺)
15	10	dmeqi 5813	. . . . . . . . . . . . 13 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
16	14, 15	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom (ℝ D 𝐹))
17	16	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → 𝑠 ∈ dom (ℝ D 𝐹))
18	13, 17	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → (𝐺‘𝑠) ∈ ℝ)
19	5, 18	eqeltrd 2839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
20	19	adantlr 712	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
21		iffalse 4468	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
22		0red 10978	. . . . . . . . . 10 ⊢ (¬ 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ)
23	21, 22	eqeltrd 2839	. . . . . . . . 9 ⊢ (¬ 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
24	23	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ ¬ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
25	20, 24	pm2.61dan 810	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
26	3, 25	syldan 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
27		fourierdlem97.h	. . . . . . 7 ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
28	27	fvmpt2 6886	. . . . . 6 ⊢ ((𝑠 ∈ ℝ ∧ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
29	3, 26, 28	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
30		fourierdlem97.t	. . . . . . . . . 10 ⊢ 𝑇 = (𝐵 − 𝐴)
31		fourierdlem97.p	. . . . . . . . . 10 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
32		fourierdlem97.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
33		fourierdlem97.q	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
34		fourierdlem97.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
35		fourierdlem97.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
36		elioore 13109	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℝ)
38	34	rexrd 11025	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
39		pnfxr 11029	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
40	39	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → +∞ ∈ ℝ^*)
41		ioogtlb 43033	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
42	38, 40, 35, 41	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 < 𝐷)
43		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 + (ℎ · 𝑇)) = (𝑥 + (ℎ · 𝑇)))
44	43	eleq1d 2823	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → ((𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
45	44	rexbidv 3226	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄))
46	45	cbvrabv 3426	. . . . . . . . . . 11 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄}
47	46	uneq2i 4094	. . . . . . . . . 10 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑥 + (ℎ · 𝑇)) ∈ ran 𝑄})
48		oveq1 7282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
49	48	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
50	49	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
51	50	cbvrexvw 3384	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
52	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
53	52	rabbiia 3407	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
54	53	uneq2i 4094	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
55		oveq1 7282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑙 = ℎ → (𝑙 · 𝑇) = (ℎ · 𝑇))
56	55	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + (ℎ · 𝑇)))
57	56	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
58	57	cbvrexvw 3384	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄)
59	58	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄))
60	59	rabbiia 3407	. . . . . . . . . . . . . 14 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}
61	60	uneq2i 4094	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
62	54, 61	eqtri 2766	. . . . . . . . . . . 12 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})
63	62	fveq2i 6777	. . . . . . . . . . 11 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄}))
64	63	oveq1i 7285	. . . . . . . . . 10 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})) − 1)
65		fourierdlem97.v	. . . . . . . . . 10 ⊢ 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
66		fourierdlem97.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
67		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ℎ → (𝑘 · 𝑇) = (ℎ · 𝑇))
68	67	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝑘 = ℎ → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + (ℎ · 𝑇)))
69	68	breq1d 5084	. . . . . . . . . . . 12 ⊢ (𝑘 = ℎ → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)))
70	69	cbvrabv 3426	. . . . . . . . . . 11 ⊢ {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)} = {ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}
71	70	supeq1i 9206	. . . . . . . . . 10 ⊢ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({ℎ ∈ ℤ ∣ ((𝑄‘0) + (ℎ · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
72		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑒 → (𝑄‘𝑗) = (𝑄‘𝑒))
73	72	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑒 → ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) = ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)))
74	73	breq1d 5084	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑒 → (((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽) ↔ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)))
75	74	cbvrabv 3426	. . . . . . . . . . 11 ⊢ {𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)} = {𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}
76	75	supeq1i 9206	. . . . . . . . . 10 ⊢ sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) = sup({𝑒 ∈ (0..^𝑀) ∣ ((𝑄‘𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )
77	30, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76	fourierdlem64 43711	. . . . . . . . 9 ⊢ (𝜑 → ((sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ (0..^𝑀) ∧ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < ) ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
78	77	simprd 496	. . . . . . . 8 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
79		simpl1 1190	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝜑)
80		simpl2l 1225	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑖 ∈ (0..^𝑀))
81		fourierdlem97.qcn	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
82		cncff 24056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
84		ffun 6603	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺:dom (ℝ D 𝐹)⟶ℝ → Fun 𝐺)
85	12, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun 𝐺)
86	85	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → Fun 𝐺)
87		ffvresb 6998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun 𝐺 → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ)))
88	86, 87	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ)))
89	83, 88	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
90	89	r19.21bi 3134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 ∈ dom 𝐺 ∧ (𝐺‘𝑠) ∈ ℂ))
91	90	simpld 495	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ dom 𝐺)
92	91	ralrimiva 3103	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
93		dfss3 3909	. . . . . . . . . . . . . . . 16 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺 ↔ ∀𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
94	92, 93	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
95	79, 80, 94	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
96		simpl2 1191	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ))
97	79, 96	jca 512	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)))
98		simpl3 1192	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
99		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))))
100	98, 99	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
101	31	fourierdlem2 43650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
102	32, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
103	33, 102	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
104	103	simpld 495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
105		elmapi 8637	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
107	106	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
108		elfzofz 13403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
109	108	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
110	107, 109	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
111	110	rexrd 11025	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
112	111	adantrr 714	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ^*)
113	112	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ^*)
114		fzofzp1 13484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
115	114	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
116	107, 115	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
117	116	adantrr 714	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
118	117	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
119	118	rexrd 11025	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
120		elioore 13109	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → 𝑡 ∈ ℝ)
121	120	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ ℝ)
122		zre 12323	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℝ)
123	122	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
124	123	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑙 ∈ ℝ)
125		fourierdlem97.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℝ)
126		fourierdlem97.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℝ)
127	125, 126	resubcld 11403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
128	30, 127	eqeltrid 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑇 ∈ ℝ)
129	128	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑇 ∈ ℝ)
130	124, 129	remulcld 11005	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑙 · 𝑇) ∈ ℝ)
131	121, 130	resubcld 11403	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ℝ)
132	110	adantrr 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘𝑖) ∈ ℝ)
133	122	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑙 ∈ ℝ)
134	128	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑇 ∈ ℝ)
135	133, 134	remulcld 11005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑙 · 𝑇) ∈ ℝ)
136	132, 135	readdcld 11004	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ)
137	136	rexrd 11025	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
138	137	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^*)
139	117, 135	readdcld 11004	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ)
140	139	rexrd 11025	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
141	140	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^*)
142		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
143		ioogtlb 43033	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
144	138, 141, 142, 143	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡)
145	132	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) ∈ ℝ)
146	145, 130, 121	ltaddsubd 11575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (((𝑄‘𝑖) + (𝑙 · 𝑇)) < 𝑡 ↔ (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇))))
147	144, 146	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘𝑖) < (𝑡 − (𝑙 · 𝑇)))
148		iooltub 43048	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑄‘𝑖) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ^* ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
149	138, 141, 142, 148	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
150	121, 130, 118	ltsubaddd 11571	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)) ↔ 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
151	149, 150	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)))
152	113, 119, 131, 147, 151	eliood 43036	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
153	97, 100, 152	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
154	95, 153	sseldd 3922	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)
155		elioore 13109	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑡 ∈ ℝ)
156		recn 10961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
157	156	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
158		zcn 12324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑙 ∈ ℤ → 𝑙 ∈ ℂ)
159	158	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑙 ∈ ℂ)
160	128	recnd 11003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ ℂ)
161	160	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℂ)
162	159, 161	mulcld 10995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝑙 · 𝑇) ∈ ℂ)
163	157, 162	npcand 11336	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) = 𝑡)
164	163	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
165	164	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
166		ovex 7308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 − (𝑙 · 𝑇)) ∈ V
167		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 ∈ dom 𝐺 ↔ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺))
168	167	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) ↔ ((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)))
169		oveq1 7282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 + (𝑙 · 𝑇)) = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
170	169	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ↔ ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺))
171	169	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))))
172		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘𝑠) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))
173	171, 172	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠) ↔ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
174	170, 173	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)) ↔ (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))))
175	168, 174	imbi12d 345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠))) ↔ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))))
176		ax-resscn 10928	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℂ
177	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ⊆ ℂ)
178	6, 177	fssd 6618	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
179	178	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
180	122	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
181	128	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → 𝑇 ∈ ℝ)
182	180, 181	remulcld 11005	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑙 ∈ ℤ) → (𝑙 · 𝑇) ∈ ℝ)
183	178	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
184	128	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
185		simplr 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑙 ∈ ℤ)
186		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
187		fourierdlem97.fper	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
188	187	ad4ant14 749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
189	183, 184, 185, 186, 188	fperiodmul 42843	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → (𝐹‘(𝑠 + (𝑙 · 𝑇))) = (𝐹‘𝑠))
190	179, 182, 189, 10	fperdvper 43460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘𝑠)))
191	166, 175, 190	vtocl 3498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
192	191	simpld 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
193	192	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
194	165, 193	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 ∈ dom 𝐺)
195	194	ex 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
196	155, 195	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑙 ∈ ℤ) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
197	196	adantlrl 717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
198	197	3adantl3 1167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺))
199	154, 198	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ dom 𝐺)
200	199	ralrimiva 3103	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
201		dfss3 3909	. . . . . . . . . . 11 ⊢ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺 ↔ ∀𝑡 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
202	200, 201	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
203	202	3exp 1118	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)))
204	203	rexlimdvv 3222	. . . . . . . 8 ⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺))
205	78, 204	mpd 15	. . . . . . 7 ⊢ (𝜑 → ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
206	205	sselda 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ dom 𝐺)
207	206	iftrued 4467	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
208	29, 207	eqtr2d 2779	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐺‘𝑠) = (𝐻‘𝑠))
209	208	mpteq2dva 5174	. . 3 ⊢ (𝜑 → (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
210	15	a1i 11	. . . . . 6 ⊢ (𝜑 → dom 𝐺 = dom (ℝ D 𝐹))
211	210	feq2d 6586	. . . . 5 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
212	12, 211	mpbird 256	. . . 4 ⊢ (𝜑 → 𝐺:dom 𝐺⟶ℝ)
213	212, 205	feqresmpt 6838	. . 3 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺‘𝑠)))
214	25, 27	fmptd 6988	. . . 4 ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
215	214, 2	feqresmpt 6838	. . 3 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻‘𝑠)))
216	209, 213, 215	3eqtr4d 2788	. 2 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))))
217	214, 177	fssd 6618	. . 3 ⊢ (𝜑 → 𝐻:ℝ⟶ℂ)
218	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
219		eleq1 2826	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝑠 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
220		fveq2 6774	. . . . . . . . 9 ⊢ (𝑠 = (𝑥 + 𝑇) → (𝐺‘𝑠) = (𝐺‘(𝑥 + 𝑇)))
221	219, 220	ifbieq1d 4483	. . . . . . . 8 ⊢ (𝑠 = (𝑥 + 𝑇) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
222	178, 128, 187, 10	fperdvper 43460	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))
223	222	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
224	223	iftrued 4467	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = (𝐺‘(𝑥 + 𝑇)))
225	221, 224	sylan9eqr 2800	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
226	225	adantllr 716	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
227		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
228	128	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229	227, 228	readdcld 11004	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℝ)
230	229	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
231	212	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐺:dom 𝐺⟶ℝ)
232	223	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
233	231, 232	ffvelrnd 6962	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) ∈ ℝ)
234	218, 226, 230, 233	fvmptd 6882	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
235	222	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
236	235	adantlr 712	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))
237		eleq1 2826	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝑠 ∈ dom 𝐺 ↔ 𝑥 ∈ dom 𝐺))
238		fveq2 6774	. . . . . . . . 9 ⊢ (𝑠 = 𝑥 → (𝐺‘𝑠) = (𝐺‘𝑥))
239	237, 238	ifbieq1d 4483	. . . . . . . 8 ⊢ (𝑠 = 𝑥 → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
240	239	adantl 482	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
241		simplr 766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
242		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
243	242	iftrued 4467	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
244	212	ffvelrnda 6961	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℝ)
245	243, 244	eqeltrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
246	245	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) ∈ ℝ)
247	218, 240, 241, 246	fvmptd 6882	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0))
248		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
249	248	iftrued 4467	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = (𝐺‘𝑥))
250	247, 249	eqtr2d 2779	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐻‘𝑥))
251	234, 236, 250	3eqtrd 2782	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
252	229	recnd 11003	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℂ)
253	228	recnd 11003	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
254	252, 253	negsubd 11338	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) + -𝑇) = ((𝑥 + 𝑇) − 𝑇))
255	227	recnd 11003	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
256	255, 253	pncand 11333	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
257	254, 256	eqtr2d 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
258	257	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
259		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
260		simpll 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝜑)
261	260, 259	jca 512	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺))
262		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
263	262	anbi2d 629	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝜑 ∧ 𝑦 ∈ dom 𝐺) ↔ (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺)))
264		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝑦 + -𝑇) = ((𝑥 + 𝑇) + -𝑇))
265	264	eleq1d 2823	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝑦 + -𝑇) ∈ dom 𝐺 ↔ ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺))
266	264	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘(𝑦 + -𝑇)) = (𝐺‘((𝑥 + 𝑇) + -𝑇)))
267		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 + 𝑇) → (𝐺‘𝑦) = (𝐺‘(𝑥 + 𝑇)))
268	266, 267	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑥 + 𝑇) → ((𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦) ↔ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
269	265, 268	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)) ↔ (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
270	263, 269	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑥 + 𝑇) → (((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦))) ↔ ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))))
271	128	renegcld 11402	. . . . . . . . . . . 12 ⊢ (𝜑 → -𝑇 ∈ ℝ)
272	160	mulm1d 11427	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-1 · 𝑇) = -𝑇)
273	272	eqcomd 2744	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → -𝑇 = (-1 · 𝑇))
274	273	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -𝑇 = (-1 · 𝑇))
275	274	oveq2d 7291	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + -𝑇) = (𝑦 + (-1 · 𝑇)))
276	275	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘(𝑦 + (-1 · 𝑇))))
277	178	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
278	128	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
279		1zzd 12351	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℤ)
280	279	znegcld 12428	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → -1 ∈ ℤ)
281		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
282	187	adantlr 712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
283	277, 278, 280, 281, 282	fperiodmul 42843	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + (-1 · 𝑇))) = (𝐹‘𝑦))
284	276, 283	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘𝑦))
285	178, 271, 284, 10	fperdvper 43460	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺‘𝑦)))
286	270, 285	vtoclg 3505	. . . . . . . . . 10 ⊢ ((𝑥 + 𝑇) ∈ dom 𝐺 → ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
287	259, 261, 286	sylc 65	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
288	287	simpld 495	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺)
289	258, 288	eqeltrd 2839	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
290	289	stoic1a 1775	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ (𝑥 + 𝑇) ∈ dom 𝐺)
291	290	iffalsed 4470	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = 0)
292	27	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0)))
293	221	adantl 482	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
294	229	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
295		0red 10978	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 0 ∈ ℝ)
296	291, 295	eqeltrd 2839	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) ∈ ℝ)
297	292, 293, 294, 296	fvmptd 6882	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
298		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ 𝑥 ∈ dom 𝐺)
299	298	iffalsed 4470	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺‘𝑥), 0) = 0)
300	239, 299	sylan9eqr 2800	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = 0)
301		simplr 766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
302	292, 300, 301, 295	fvmptd 6882	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘𝑥) = 0)
303	291, 297, 302	3eqtr4d 2788	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
304	251, 303	pm2.61dan 810	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐻‘(𝑥 + 𝑇)) = (𝐻‘𝑥))
305		elioore 13109	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
306	305	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
307	305, 25	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) ∈ ℝ)
308	306, 307, 28	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
309	308	adantlr 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0))
310	91	iftrued 4467	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺‘𝑠), 0) = (𝐺‘𝑠))
311	309, 310	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻‘𝑠) = (𝐺‘𝑠))
312	311	mpteq2dva 5174	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
313	214	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻:ℝ⟶ℝ)
314		ioossre 13140	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
315	314	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
316	313, 315	feqresmpt 6838	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻‘𝑠)))
317	212	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺:dom 𝐺⟶ℝ)
318	317, 94	feqresmpt 6838	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺‘𝑠)))
319	312, 316, 318	3eqtr4d 2788	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
320	319, 81	eqeltrd 2839	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
321		eqid 2738	. . 3 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
322		oveq1 7282	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
323	322	eleq1d 2823	. . . . . . 7 ⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
324	323	rexbidv 3226	. . . . . 6 ⊢ (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
325	324	cbvrabv 3426	. . . . 5 ⊢ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
326	325	uneq2i 4094	. . . 4 ⊢ ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
327	326	eqcomi 2747	. . 3 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
328	54	fveq2i 6777	. . . 4 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
329	328	oveq1i 7285	. . 3 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
330		isoeq5 7192	. . . . . 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 6418	. . . 4 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ℎ ∈ ℤ (𝑦 + (ℎ · 𝑇)) ∈ ran 𝑄})))
333		isoeq1 7188	. . . . 5 ⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
334	333	cbviotavw 6399	. . . 4 ⊢ (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
335	332, 334, 65	3eqtr4ri 2777	. . 3 ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
336		id 22	. . . . 5 ⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥)
337		oveq2 7283	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → (𝐵 − 𝑣) = (𝐵 − 𝑥))
338	337	oveq1d 7290	. . . . . . 7 ⊢ (𝑣 = 𝑥 → ((𝐵 − 𝑣) / 𝑇) = ((𝐵 − 𝑥) / 𝑇))
339	338	fveq2d 6778	. . . . . 6 ⊢ (𝑣 = 𝑥 → (⌊‘((𝐵 − 𝑣) / 𝑇)) = (⌊‘((𝐵 − 𝑥) / 𝑇)))
340	339	oveq1d 7290	. . . . 5 ⊢ (𝑣 = 𝑥 → ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))
341	336, 340	oveq12d 7293	. . . 4 ⊢ (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
342	341	cbvmptv 5187	. . 3 ⊢ (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
343		eqeq1 2742	. . . . 5 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝐵 ↔ 𝑧 = 𝐵))
344		id 22	. . . . 5 ⊢ (𝑢 = 𝑧 → 𝑢 = 𝑧)
345	343, 344	ifbieq2d 4485	. . . 4 ⊢ (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
346	345	cbvmptv 5187	. . 3 ⊢ (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
347		eqid 2738	. . 3 ⊢ ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
348		eqid 2738	. . 3 ⊢ (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
349		eqid 2738	. . 3 ⊢ (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
350		fveq2 6774	. . . . . . . 8 ⊢ (𝑖 = 𝑡 → (𝑄‘𝑖) = (𝑄‘𝑡))
351	350	breq1d 5084	. . . . . . 7 ⊢ (𝑖 = 𝑡 → ((𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
352	351	cbvrabv 3426	. . . . . 6 ⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
353		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))
354	353	fveq2d 6778	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
355	354	eqcomd 2744	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
356	355	breq2d 5086	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
357	356	rabbidv 3414	. . . . . 6 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
358	352, 357	eqtr2id 2791	. . . . 5 ⊢ (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
359	358	supeq1d 9205	. . . 4 ⊢ (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄‘𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵 − 𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
360	359	cbvmptv 5187	. . 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 43737	. 2 ⊢ (𝜑 → (𝐻 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
362	216, 361	eqeltrd 2839	1 ⊢ (𝜑 → (𝐺 ↾ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 {crab 3068 ∪ cun 3885 ⊆ wss 3887 ifcif 4459 {cpr 4563 class class class wbr 5074 ↦ cmpt 5157 dom cdm 5589 ran crn 5590 ↾ cres 5591 ℩cio 6389 Fun wfun 6427 ⟶wf 6429 ‘cfv 6433 Isom wiso 6434 (class class class)co 7275 ↑_m cmap 8615 supcsup 9199 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 +∞cpnf 11006 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 -cneg 11206 / cdiv 11632 ℕcn 11973 ℤcz 12319 (,)cioo 13079 (,]cioc 13080 [,]cicc 13082 ...cfz 13239 ..^cfzo 13382 ⌊cfl 13510 ♯chash 14044 –cn→ccncf 24039 D cdv 25027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-oadd 8301 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-xnn0 12306 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ioc 13084 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-seq 13722 df-exp 13783 df-hash 14045 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-struct 16848 df-slot 16883 df-ndx 16895 df-base 16913 df-plusg 16975 df-mulr 16976 df-starv 16977 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-rest 17133 df-topn 17134 df-topgen 17154 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-fbas 20594 df-fg 20595 df-cnfld 20598 df-top 22043 df-topon 22060 df-topsp 22082 df-bases 22096 df-cld 22170 df-ntr 22171 df-cls 22172 df-nei 22249 df-lp 22287 df-perf 22288 df-cn 22378 df-cnp 22379 df-haus 22466 df-cmp 22538 df-fil 22997 df-fm 23089 df-flim 23090 df-flf 23091 df-xms 23473 df-ms 23474 df-cncf 24041 df-limc 25030 df-dv 25031

This theorem is referenced by: fourierdlem112 43759

W3C validator