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

Theorem fourierdlem97 42687
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.
StepHypRef Expression
1 ioossre 12784 . . . . . . . 8 ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ
21a1i 11 . . . . . . 7 (𝜑 → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ)
32sselda 3951 . . . . . 6 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ ℝ)
4 iftrue 4454 . . . . . . . . . . 11 (𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
54adantl 485 . . . . . . . . . 10 ((𝜑𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
6 fourierdlem97.f . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶ℝ)
7 ssid 3973 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ
8 dvfre 24543 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
96, 7, 8sylancl 589 . . . . . . . . . . . . 13 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
10 fourierdlem97.g . . . . . . . . . . . . . 14 𝐺 = (ℝ D 𝐹)
1110feq1i 6486 . . . . . . . . . . . . 13 (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
129, 11sylibr 237 . . . . . . . . . . . 12 (𝜑𝐺:dom (ℝ D 𝐹)⟶ℝ)
1312adantr 484 . . . . . . . . . . 11 ((𝜑𝑠 ∈ dom 𝐺) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
14 id 22 . . . . . . . . . . . . 13 (𝑠 ∈ dom 𝐺𝑠 ∈ dom 𝐺)
1510dmeqi 5754 . . . . . . . . . . . . 13 dom 𝐺 = dom (ℝ D 𝐹)
1614, 15eleqtrdi 2926 . . . . . . . . . . . 12 (𝑠 ∈ dom 𝐺𝑠 ∈ dom (ℝ D 𝐹))
1716adantl 485 . . . . . . . . . . 11 ((𝜑𝑠 ∈ dom 𝐺) → 𝑠 ∈ dom (ℝ D 𝐹))
1813, 17ffvelrnd 6833 . . . . . . . . . 10 ((𝜑𝑠 ∈ dom 𝐺) → (𝐺𝑠) ∈ ℝ)
195, 18eqeltrd 2916 . . . . . . . . 9 ((𝜑𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
2019adantlr 714 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
21 iffalse 4457 . . . . . . . . . 10 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = 0)
22 0red 10629 . . . . . . . . . 10 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ)
2321, 22eqeltrd 2916 . . . . . . . . 9 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
2423adantl 485 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ ¬ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
2520, 24pm2.61dan 812 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
263, 25syldan 594 . . . . . 6 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
27 fourierdlem97.h . . . . . . 7 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
2827fvmpt2 6760 . . . . . 6 ((𝑠 ∈ ℝ ∧ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
293, 26, 28syl2anc 587 . . . . 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 12754 . . . . . . . . . . 11 (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
3735, 36syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ)
3834rexrd 10676 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℝ*)
39 pnfxr 10680 . . . . . . . . . . . 12 +∞ ∈ ℝ*
4039a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
41 ioogtlb 41974 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
4238, 40, 35, 41syl3anc 1368 . . . . . . . . . 10 (𝜑𝐶 < 𝐷)
43 oveq1 7145 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 + ( · 𝑇)) = (𝑥 + ( · 𝑇)))
4443eleq1d 2900 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝑦 + ( · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + ( · 𝑇)) ∈ ran 𝑄))
4544rexbidv 3289 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄 ↔ ∃ ∈ ℤ (𝑥 + ( · 𝑇)) ∈ ran 𝑄))
4645cbvrabv 3476 . . . . . . . . . . 11 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑥 + ( · 𝑇)) ∈ ran 𝑄}
4746uneq2i 4120 . . . . . . . . . 10 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑥 + ( · 𝑇)) ∈ ran 𝑄})
48 oveq1 7145 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
4948oveq2d 7154 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
5049eleq1d 2900 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
5150cbvrexvw 3435 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
5251a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
5352rabbiia 3457 . . . . . . . . . . . . . 14 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
5453uneq2i 4120 . . . . . . . . . . . . 13 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
55 oveq1 7145 . . . . . . . . . . . . . . . . . . 19 (𝑙 = → (𝑙 · 𝑇) = ( · 𝑇))
5655oveq2d 7154 . . . . . . . . . . . . . . . . . 18 (𝑙 = → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + ( · 𝑇)))
5756eleq1d 2900 . . . . . . . . . . . . . . . . 17 (𝑙 = → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + ( · 𝑇)) ∈ ran 𝑄))
5857cbvrexvw 3435 . . . . . . . . . . . . . . . 16 (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄)
5958a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄))
6059rabbiia 3457 . . . . . . . . . . . . . 14 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}
6160uneq2i 4120 . . . . . . . . . . . . 13 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})
6254, 61eqtri 2847 . . . . . . . . . . . 12 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})
6362fveq2i 6654 . . . . . . . . . . 11 (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}))
6463oveq1i 7148 . . . . . . . . . 10 ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})) − 1)
65 fourierdlem97.v . . . . . . . . . 10 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})))
66 fourierdlem97.j . . . . . . . . . 10 (𝜑𝐽 ∈ (0..^((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
67 oveq1 7145 . . . . . . . . . . . . . 14 (𝑘 = → (𝑘 · 𝑇) = ( · 𝑇))
6867oveq2d 7154 . . . . . . . . . . . . 13 (𝑘 = → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ( · 𝑇)))
6968breq1d 5057 . . . . . . . . . . . 12 (𝑘 = → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽) ↔ ((𝑄‘0) + ( · 𝑇)) ≤ (𝑉𝐽)))
7069cbvrabv 3476 . . . . . . . . . . 11 {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)} = { ∈ ℤ ∣ ((𝑄‘0) + ( · 𝑇)) ≤ (𝑉𝐽)}
7170supeq1i 8895 . . . . . . . . . 10 sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) = sup({ ∈ ℤ ∣ ((𝑄‘0) + ( · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < )
72 fveq2 6651 . . . . . . . . . . . . . 14 (𝑗 = 𝑒 → (𝑄𝑗) = (𝑄𝑒))
7372oveq1d 7153 . . . . . . . . . . . . 13 (𝑗 = 𝑒 → ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) = ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)))
7473breq1d 5057 . . . . . . . . . . . 12 (𝑗 = 𝑒 → (((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽) ↔ ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)))
7574cbvrabv 3476 . . . . . . . . . . 11 {𝑗 ∈ (0..^𝑀) ∣ ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)} = {𝑒 ∈ (0..^𝑀) ∣ ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}
7675supeq1i 8895 . . . . . . . . . 10 sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) = sup({𝑒 ∈ (0..^𝑀) ∣ ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < )
7730, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76fourierdlem64 42654 . . . . . . . . 9 (𝜑 → ((sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) ∈ (0..^𝑀) ∧ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
7877simprd 499 . . . . . . . 8 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
79 simpl1 1188 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝜑)
80 simpl2l 1223 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑖 ∈ (0..^𝑀))
81 fourierdlem97.qcn . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
82 cncff 23487 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
84 ffun 6498 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺:dom (ℝ D 𝐹)⟶ℝ → Fun 𝐺)
8512, 84syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun 𝐺)
8685adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → Fun 𝐺)
87 ffvresb 6869 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝐺 → ((𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ)))
8886, 87syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ)))
8983, 88mpbid 235 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ))
9089r19.21bi 3202 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ))
9190simpld 498 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ dom 𝐺)
9291ralrimiva 3176 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
93 dfss3 3940 . . . . . . . . . . . . . . . 16 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺 ↔ ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
9492, 93sylibr 237 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
9579, 80, 94syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
96 simpl2 1189 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ))
9779, 96jca 515 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)))
98 simpl3 1190 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
99 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))))
10098, 99sseldd 3952 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
10131fourierdlem2 42593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
10232, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
10333, 102mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
104103simpld 498 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
105 elmapi 8411 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑄:(0...𝑀)⟶ℝ)
107106adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
108 elfzofz 13046 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
109108adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
110107, 109ffvelrnd 6833 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
111110rexrd 10676 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
112111adantrr 716 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄𝑖) ∈ ℝ*)
113112adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄𝑖) ∈ ℝ*)
114 fzofzp1 13127 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
115114adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
116107, 115ffvelrnd 6833 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
117116adantrr 716 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
118117adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
119118rexrd 10676 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
120 elioore 12754 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → 𝑡 ∈ ℝ)
121120adantl 485 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ ℝ)
122 zre 11971 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ ℤ → 𝑙 ∈ ℝ)
123122adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
124123ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑙 ∈ ℝ)
125 fourierdlem97.a . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
126 fourierdlem97.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ ℝ)
127125, 126resubcld 11053 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
12830, 127eqeltrid 2920 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
129128ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑇 ∈ ℝ)
130124, 129remulcld 10656 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑙 · 𝑇) ∈ ℝ)
131121, 130resubcld 11053 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ℝ)
132110adantrr 716 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄𝑖) ∈ ℝ)
133122ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑙 ∈ ℝ)
134128adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑇 ∈ ℝ)
135133, 134remulcld 10656 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑙 · 𝑇) ∈ ℝ)
136132, 135readdcld 10655 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ)
137136rexrd 10676 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ*)
138137adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ*)
139117, 135readdcld 10655 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ)
140139rexrd 10676 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*)
141140adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*)
142 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
143 ioogtlb 41974 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄𝑖) + (𝑙 · 𝑇)) < 𝑡)
144138, 141, 142, 143syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄𝑖) + (𝑙 · 𝑇)) < 𝑡)
145132adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄𝑖) ∈ ℝ)
146145, 130, 121ltaddsubd 11225 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (((𝑄𝑖) + (𝑙 · 𝑇)) < 𝑡 ↔ (𝑄𝑖) < (𝑡 − (𝑙 · 𝑇))))
147144, 146mpbid 235 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄𝑖) < (𝑡 − (𝑙 · 𝑇)))
148 iooltub 41989 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
149138, 141, 142, 148syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
150121, 130, 118ltsubaddd 11221 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)) ↔ 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
151149, 150mpbird 260 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)))
152113, 119, 131, 147, 151eliood 41977 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
15397, 100, 152syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
15495, 153sseldd 3952 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)
155 elioore 12754 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑡 ∈ ℝ)
156 recn 10612 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
157156adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
158 zcn 11972 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ ℤ → 𝑙 ∈ ℂ)
159158ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑙 ∈ ℂ)
160128recnd 10654 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑇 ∈ ℂ)
161160ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℂ)
162159, 161mulcld 10646 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝑙 · 𝑇) ∈ ℂ)
163157, 162npcand 10986 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) = 𝑡)
164163eqcomd 2830 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
165164adantr 484 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
166 ovex 7171 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 − (𝑙 · 𝑇)) ∈ V
167 eleq1 2903 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 ∈ dom 𝐺 ↔ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺))
168167anbi2d 631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) ↔ ((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)))
169 oveq1 7145 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 + (𝑙 · 𝑇)) = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
170169eleq1d 2900 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ↔ ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺))
171169fveq2d 6655 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))))
172 fveq2 6651 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺𝑠) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))
173171, 172eqeq12d 2840 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠) ↔ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
174170, 173anbi12d 633 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠)) ↔ (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))))
175168, 174imbi12d 348 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠))) ↔ (((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))))
176 ax-resscn 10579 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℂ
177176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ⊆ ℂ)
1786, 177fssd 6509 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:ℝ⟶ℂ)
179178adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑙 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
180122adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
181128adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑙 ∈ ℤ) → 𝑇 ∈ ℝ)
182180, 181remulcld 10656 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑙 ∈ ℤ) → (𝑙 · 𝑇) ∈ ℝ)
183178ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
184128ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
185 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑙 ∈ ℤ)
186 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
187 fourierdlem97.fper . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
188187ad4ant14 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
189183, 184, 185, 186, 188fperiodmul 41778 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → (𝐹‘(𝑠 + (𝑙 · 𝑇))) = (𝐹𝑠))
190179, 182, 189, 10fperdvper 42403 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠)))
191166, 175, 190vtocl 3544 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
192191simpld 498 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
193192adantlr 714 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
194165, 193eqeltrd 2916 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 ∈ dom 𝐺)
195194ex 416 . . . . . . . . . . . . . . . 16 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
196155, 195sylan2 595 . . . . . . . . . . . . . . 15 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
197196adantlrl 719 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
1981973adantl3 1165 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
199154, 198mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ dom 𝐺)
200199ralrimiva 3176 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ∀𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
201 dfss3 3940 . . . . . . . . . . 11 (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺 ↔ ∀𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
202200, 201sylibr 237 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
2032023exp 1116 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)))
204203rexlimdvv 3285 . . . . . . . 8 (𝜑 → (∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺))
20578, 204mpd 15 . . . . . . 7 (𝜑 → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
206205sselda 3951 . . . . . 6 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ dom 𝐺)
207206iftrued 4456 . . . . 5 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
20829, 207eqtr2d 2860 . . . 4 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐺𝑠) = (𝐻𝑠))
209208mpteq2dva 5142 . . 3 (𝜑 → (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺𝑠)) = (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻𝑠)))
21015a1i 11 . . . . . 6 (𝜑 → dom 𝐺 = dom (ℝ D 𝐹))
211210feq2d 6481 . . . . 5 (𝜑 → (𝐺:dom 𝐺⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
21212, 211mpbird 260 . . . 4 (𝜑𝐺:dom 𝐺⟶ℝ)
213212, 205feqresmpt 6715 . . 3 (𝜑 → (𝐺 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺𝑠)))
21425, 27fmptd 6859 . . . 4 (𝜑𝐻:ℝ⟶ℝ)
215214, 2feqresmpt 6715 . . 3 (𝜑 → (𝐻 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻𝑠)))
216209, 213, 2153eqtr4d 2869 . 2 (𝜑 → (𝐺 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝐻 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))))
217214, 177fssd 6509 . . 3 (𝜑𝐻:ℝ⟶ℂ)
21827a1i 11 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0)))
219 eleq1 2903 . . . . . . . . 9 (𝑠 = (𝑥 + 𝑇) → (𝑠 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
220 fveq2 6651 . . . . . . . . 9 (𝑠 = (𝑥 + 𝑇) → (𝐺𝑠) = (𝐺‘(𝑥 + 𝑇)))
221219, 220ifbieq1d 4471 . . . . . . . 8 (𝑠 = (𝑥 + 𝑇) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
222178, 128, 187, 10fperdvper 42403 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺𝑥)))
223222simpld 498 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
224223iftrued 4456 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = (𝐺‘(𝑥 + 𝑇)))
225221, 224sylan9eqr 2881 . . . . . . 7 (((𝜑𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
226225adantllr 718 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
227 simpr 488 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
228128adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229227, 228readdcld 10655 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℝ)
230229adantr 484 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
231212ad2antrr 725 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐺:dom 𝐺⟶ℝ)
232223adantlr 714 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
233231, 232ffvelrnd 6833 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) ∈ ℝ)
234218, 226, 230, 233fvmptd 6756 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
235222simprd 499 . . . . . 6 ((𝜑𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺𝑥))
236235adantlr 714 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺𝑥))
237 eleq1 2903 . . . . . . . . 9 (𝑠 = 𝑥 → (𝑠 ∈ dom 𝐺𝑥 ∈ dom 𝐺))
238 fveq2 6651 . . . . . . . . 9 (𝑠 = 𝑥 → (𝐺𝑠) = (𝐺𝑥))
239237, 238ifbieq1d 4471 . . . . . . . 8 (𝑠 = 𝑥 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0))
240239adantl 485 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0))
241 simplr 768 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
242 simpr 488 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
243242iftrued 4456 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) = (𝐺𝑥))
244212ffvelrnda 6832 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐺) → (𝐺𝑥) ∈ ℝ)
245243, 244eqeltrd 2916 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) ∈ ℝ)
246245adantlr 714 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) ∈ ℝ)
247218, 240, 241, 246fvmptd 6756 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻𝑥) = if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0))
248 simpr 488 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
249248iftrued 4456 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) = (𝐺𝑥))
250247, 249eqtr2d 2860 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺𝑥) = (𝐻𝑥))
251234, 236, 2503eqtrd 2863 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻𝑥))
252229recnd 10654 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℂ)
253228recnd 10654 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
254252, 253negsubd 10988 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → ((𝑥 + 𝑇) + -𝑇) = ((𝑥 + 𝑇) − 𝑇))
255227recnd 10654 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
256255, 253pncand 10983 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
257254, 256eqtr2d 2860 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
258257adantr 484 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
259 simpr 488 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
260 simpll 766 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝜑)
261260, 259jca 515 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺))
262 eleq1 2903 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 𝑇) → (𝑦 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
263262anbi2d 631 . . . . . . . . . . . 12 (𝑦 = (𝑥 + 𝑇) → ((𝜑𝑦 ∈ dom 𝐺) ↔ (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺)))
264 oveq1 7145 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 + 𝑇) → (𝑦 + -𝑇) = ((𝑥 + 𝑇) + -𝑇))
265264eleq1d 2900 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 𝑇) → ((𝑦 + -𝑇) ∈ dom 𝐺 ↔ ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺))
266264fveq2d 6655 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 + 𝑇) → (𝐺‘(𝑦 + -𝑇)) = (𝐺‘((𝑥 + 𝑇) + -𝑇)))
267 fveq2 6651 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 + 𝑇) → (𝐺𝑦) = (𝐺‘(𝑥 + 𝑇)))
268266, 267eqeq12d 2840 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 𝑇) → ((𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦) ↔ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
269265, 268anbi12d 633 . . . . . . . . . . . 12 (𝑦 = (𝑥 + 𝑇) → (((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦)) ↔ (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
270263, 269imbi12d 348 . . . . . . . . . . 11 (𝑦 = (𝑥 + 𝑇) → (((𝜑𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦))) ↔ ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))))
271128renegcld 11052 . . . . . . . . . . . 12 (𝜑 → -𝑇 ∈ ℝ)
272160mulm1d 11077 . . . . . . . . . . . . . . . . 17 (𝜑 → (-1 · 𝑇) = -𝑇)
273272eqcomd 2830 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑇 = (-1 · 𝑇))
274273adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → -𝑇 = (-1 · 𝑇))
275274oveq2d 7154 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + -𝑇) = (𝑦 + (-1 · 𝑇)))
276275fveq2d 6655 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘(𝑦 + (-1 · 𝑇))))
277178adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
278128adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
279 1zzd 11999 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 1 ∈ ℤ)
280279znegcld 12075 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → -1 ∈ ℤ)
281 simpr 488 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
282187adantlr 714 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
283277, 278, 280, 281, 282fperiodmul 41778 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + (-1 · 𝑇))) = (𝐹𝑦))
284276, 283eqtrd 2859 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹𝑦))
285178, 271, 284, 10fperdvper 42403 . . . . . . . . . . 11 ((𝜑𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦)))
286270, 285vtoclg 3552 . . . . . . . . . 10 ((𝑥 + 𝑇) ∈ dom 𝐺 → ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
287259, 261, 286sylc 65 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
288287simpld 498 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺)
289258, 288eqeltrd 2916 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
290289stoic1a 1774 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ (𝑥 + 𝑇) ∈ dom 𝐺)
291290iffalsed 4459 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = 0)
29227a1i 11 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0)))
293221adantl 485 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
294229adantr 484 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
295 0red 10629 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 0 ∈ ℝ)
296291, 295eqeltrd 2916 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) ∈ ℝ)
297292, 293, 294, 296fvmptd 6756 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
298 simpr 488 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ 𝑥 ∈ dom 𝐺)
299298iffalsed 4459 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) = 0)
300239, 299sylan9eqr 2881 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = 0)
301 simplr 768 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
302292, 300, 301, 295fvmptd 6756 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻𝑥) = 0)
303291, 297, 3023eqtr4d 2869 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻𝑥))
304251, 303pm2.61dan 812 . . 3 ((𝜑𝑥 ∈ ℝ) → (𝐻‘(𝑥 + 𝑇)) = (𝐻𝑥))
305 elioore 12754 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
306305adantl 485 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
307305, 25sylan2 595 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
308306, 307, 28syl2anc 587 . . . . . . . 8 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
309308adantlr 714 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
31091iftrued 4456 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
311309, 310eqtrd 2859 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = (𝐺𝑠))
312311mpteq2dva 5142 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺𝑠)))
313214adantr 484 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻:ℝ⟶ℝ)
314 ioossre 12784 . . . . . . 7 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
315314a1i 11 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
316313, 315feqresmpt 6715 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)))
317212adantr 484 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐺:dom 𝐺⟶ℝ)
318317, 94feqresmpt 6715 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺𝑠)))
319312, 316, 3183eqtr4d 2869 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
320319, 81eqeltrd 2916 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
321 eqid 2824 . . 3 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
322 oveq1 7145 . . . . . . . 8 (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
323322eleq1d 2900 . . . . . . 7 (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
324323rexbidv 3289 . . . . . 6 (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
325324cbvrabv 3476 . . . . 5 {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
326325uneq2i 4120 . . . 4 ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
327326eqcomi 2833 . . 3 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
32854fveq2i 6654 . . . 4 (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
329328oveq1i 7148 . . 3 ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
330 isoeq5 7056 . . . . . 6 (({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}) → (𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}))))
33161, 330ax-mp 5 . . . . 5 (𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})))
332331iotabii 6321 . . . 4 (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})))
333 isoeq1 7052 . . . . 5 (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
334333cbviotavw 6303 . . . 4 (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
335332, 334, 653eqtr4ri 2858 . . 3 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
336 id 22 . . . . 5 (𝑣 = 𝑥𝑣 = 𝑥)
337 oveq2 7146 . . . . . . . 8 (𝑣 = 𝑥 → (𝐵𝑣) = (𝐵𝑥))
338337oveq1d 7153 . . . . . . 7 (𝑣 = 𝑥 → ((𝐵𝑣) / 𝑇) = ((𝐵𝑥) / 𝑇))
339338fveq2d 6655 . . . . . 6 (𝑣 = 𝑥 → (⌊‘((𝐵𝑣) / 𝑇)) = (⌊‘((𝐵𝑥) / 𝑇)))
340339oveq1d 7153 . . . . 5 (𝑣 = 𝑥 → ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
341336, 340oveq12d 7156 . . . 4 (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
342341cbvmptv 5150 . . 3 (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
343 eqeq1 2828 . . . . 5 (𝑢 = 𝑧 → (𝑢 = 𝐵𝑧 = 𝐵))
344 id 22 . . . . 5 (𝑢 = 𝑧𝑢 = 𝑧)
345343, 344ifbieq2d 4473 . . . 4 (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
346345cbvmptv 5150 . . 3 (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
347 eqid 2824 . . 3 ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
348 eqid 2824 . . 3 (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
349 eqid 2824 . . 3 (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
350 fveq2 6651 . . . . . . . 8 (𝑖 = 𝑡 → (𝑄𝑖) = (𝑄𝑡))
351350breq1d 5057 . . . . . . 7 (𝑖 = 𝑡 → ((𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
352351cbvrabv 3476 . . . . . 6 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
353 fveq2 6651 . . . . . . . . . 10 (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))
354353fveq2d 6655 . . . . . . . . 9 (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
355354eqcomd 2830 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
356355breq2d 5059 . . . . . . 7 (𝑤 = 𝑥 → ((𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
357356rabbidv 3465 . . . . . 6 (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
358352, 357syl5req 2872 . . . . 5 (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
359358supeq1d 8894 . . . 4 (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
360359cbvmptv 5150 . . 3 (𝑤 ∈ ℝ ↦ sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < )) = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
36131, 30, 32, 33, 217, 304, 320, 34, 35, 321, 327, 329, 335, 342, 346, 66, 347, 348, 349, 360fourierdlem90 42680 . 2 (𝜑 → (𝐻 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
362216, 361eqeltrd 2916 1 (𝜑 → (𝐺 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  wral 3132  wrex 3133  {crab 3136  cun 3916  wss 3918  ifcif 4448  {cpr 4550   class class class wbr 5047  cmpt 5127  dom cdm 5536  ran crn 5537  cres 5538  cio 6293  Fun wfun 6330  wf 6332  cfv 6336   Isom wiso 6337  (class class class)co 7138  m cmap 8389  supcsup 8888  cc 10520  cr 10521  0cc0 10522  1c1 10523   + caddc 10525   · cmul 10527  +∞cpnf 10657  *cxr 10659   < clt 10660  cle 10661  cmin 10855  -cneg 10856   / cdiv 11282  cn 11623  cz 11967  (,)cioo 12724  (,]cioc 12725  [,]cicc 12727  ...cfz 12883  ..^cfzo 13026  cfl 13153  chash 13684  cnccncf 23470   D cdv 24455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-inf2 9088  ax-cnex 10578  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-mulrcl 10585  ax-mulcom 10586  ax-addass 10587  ax-mulass 10588  ax-distr 10589  ax-i2m1 10590  ax-1ne0 10591  ax-1rid 10592  ax-rnegex 10593  ax-rrecex 10594  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597  ax-pre-ltadd 10598  ax-pre-mulgt0 10599  ax-pre-sup 10600
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-int 4858  df-iun 4902  df-iin 4903  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-se 5496  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-om 7564  df-1st 7672  df-2nd 7673  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fi 8859  df-sup 8890  df-inf 8891  df-oi 8958  df-dju 9314  df-card 9352  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-sub 10857  df-neg 10858  df-div 11283  df-nn 11624  df-2 11686  df-3 11687  df-4 11688  df-5 11689  df-6 11690  df-7 11691  df-8 11692  df-9 11693  df-n0 11884  df-xnn0 11954  df-z 11968  df-dec 12085  df-uz 12230  df-q 12335  df-rp 12376  df-xneg 12493  df-xadd 12494  df-xmul 12495  df-ioo 12728  df-ioc 12729  df-ico 12730  df-icc 12731  df-fz 12884  df-fzo 13027  df-fl 13155  df-seq 13363  df-exp 13424  df-hash 13685  df-cj 14447  df-re 14448  df-im 14449  df-sqrt 14583  df-abs 14584  df-struct 16474  df-ndx 16475  df-slot 16476  df-base 16478  df-plusg 16567  df-mulr 16568  df-starv 16569  df-tset 16573  df-ple 16574  df-ds 16576  df-unif 16577  df-rest 16685  df-topn 16686  df-topgen 16706  df-psmet 20523  df-xmet 20524  df-met 20525  df-bl 20526  df-mopn 20527  df-fbas 20528  df-fg 20529  df-cnfld 20532  df-top 21488  df-topon 21505  df-topsp 21527  df-bases 21540  df-cld 21613  df-ntr 21614  df-cls 21615  df-nei 21692  df-lp 21730  df-perf 21731  df-cn 21821  df-cnp 21822  df-haus 21909  df-cmp 21981  df-fil 22440  df-fm 22532  df-flim 22533  df-flf 22534  df-xms 22916  df-ms 22917  df-cncf 23472  df-limc 24458  df-dv 24459
This theorem is referenced by:  fourierdlem112  42702
  Copyright terms: Public domain W3C validator