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 38896
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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 12058 . . . . . . . 8 ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ
21a1i 11 . . . . . . 7 (𝜑 → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ ℝ)
32sselda 3563 . . . . . 6 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ ℝ)
4 iftrue 4037 . . . . . . . . . . 11 (𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
54adantl 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
6 fourierdlem97.f . . . . . . . . . . . . . 14 (𝜑𝐹:ℝ⟶ℝ)
7 ssid 3582 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ
8 dvfre 23433 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
96, 7, 8sylancl 692 . . . . . . . . . . . . 13 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
10 fourierdlem97.g . . . . . . . . . . . . . 14 𝐺 = (ℝ D 𝐹)
1110feq1i 5931 . . . . . . . . . . . . 13 (𝐺:dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
129, 11sylibr 222 . . . . . . . . . . . 12 (𝜑𝐺:dom (ℝ D 𝐹)⟶ℝ)
1312adantr 479 . . . . . . . . . . 11 ((𝜑𝑠 ∈ dom 𝐺) → 𝐺:dom (ℝ D 𝐹)⟶ℝ)
14 id 22 . . . . . . . . . . . . 13 (𝑠 ∈ dom 𝐺𝑠 ∈ dom 𝐺)
1510dmeqi 5230 . . . . . . . . . . . . 13 dom 𝐺 = dom (ℝ D 𝐹)
1614, 15syl6eleq 2693 . . . . . . . . . . . 12 (𝑠 ∈ dom 𝐺𝑠 ∈ dom (ℝ D 𝐹))
1716adantl 480 . . . . . . . . . . 11 ((𝜑𝑠 ∈ dom 𝐺) → 𝑠 ∈ dom (ℝ D 𝐹))
1813, 17ffvelrnd 6249 . . . . . . . . . 10 ((𝜑𝑠 ∈ dom 𝐺) → (𝐺𝑠) ∈ ℝ)
195, 18eqeltrd 2683 . . . . . . . . 9 ((𝜑𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
2019adantlr 746 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
21 iffalse 4040 . . . . . . . . . 10 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = 0)
22 0red 9893 . . . . . . . . . 10 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ)
2321, 22eqeltrd 2683 . . . . . . . . 9 𝑠 ∈ dom 𝐺 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
2423adantl 480 . . . . . . . 8 (((𝜑𝑠 ∈ ℝ) ∧ ¬ 𝑠 ∈ dom 𝐺) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
2520, 24pm2.61dan 827 . . . . . . 7 ((𝜑𝑠 ∈ ℝ) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
263, 25syldan 485 . . . . . 6 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
27 fourierdlem97.h . . . . . . 7 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
2827fvmpt2 6181 . . . . . 6 ((𝑠 ∈ ℝ ∧ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
293, 26, 28syl2anc 690 . . . . 5 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
30 fourierdlem97.t . . . . . . . . . 10 𝑇 = (𝐵𝐴)
31 fourierdlem97.p . . . . . . . . . 10 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
32 fourierdlem97.m . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
33 fourierdlem97.q . . . . . . . . . 10 (𝜑𝑄 ∈ (𝑃𝑀))
34 fourierdlem97.c . . . . . . . . . 10 (𝜑𝐶 ∈ ℝ)
35 fourierdlem97.d . . . . . . . . . . 11 (𝜑𝐷 ∈ (𝐶(,)+∞))
36 elioore 12028 . . . . . . . . . . 11 (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
3735, 36syl 17 . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ)
3834rexrd 9941 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℝ*)
39 pnfxr 11777 . . . . . . . . . . . 12 +∞ ∈ ℝ*
4039a1i 11 . . . . . . . . . . 11 (𝜑 → +∞ ∈ ℝ*)
41 ioogtlb 38364 . . . . . . . . . . 11 ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
4238, 40, 35, 41syl3anc 1317 . . . . . . . . . 10 (𝜑𝐶 < 𝐷)
43 oveq1 6530 . . . . . . . . . . . . . 14 (𝑦 = 𝑥 → (𝑦 + ( · 𝑇)) = (𝑥 + ( · 𝑇)))
4443eleq1d 2667 . . . . . . . . . . . . 13 (𝑦 = 𝑥 → ((𝑦 + ( · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + ( · 𝑇)) ∈ ran 𝑄))
4544rexbidv 3029 . . . . . . . . . . . 12 (𝑦 = 𝑥 → (∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄 ↔ ∃ ∈ ℤ (𝑥 + ( · 𝑇)) ∈ ran 𝑄))
4645cbvrabv 3167 . . . . . . . . . . 11 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑥 + ( · 𝑇)) ∈ ran 𝑄}
4746uneq2i 3721 . . . . . . . . . 10 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑥 + ( · 𝑇)) ∈ ran 𝑄})
48 oveq1 6530 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑙 → (𝑘 · 𝑇) = (𝑙 · 𝑇))
4948oveq2d 6539 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
5049eleq1d 2667 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
5150cbvrexv 3143 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄)
5251a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
5352rabbiia 3156 . . . . . . . . . . . . . 14 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
5453uneq2i 3721 . . . . . . . . . . . . 13 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
55 oveq1 6530 . . . . . . . . . . . . . . . . . . 19 (𝑙 = → (𝑙 · 𝑇) = ( · 𝑇))
5655oveq2d 6539 . . . . . . . . . . . . . . . . . 18 (𝑙 = → (𝑦 + (𝑙 · 𝑇)) = (𝑦 + ( · 𝑇)))
5756eleq1d 2667 . . . . . . . . . . . . . . . . 17 (𝑙 = → ((𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + ( · 𝑇)) ∈ ran 𝑄))
5857cbvrexv 3143 . . . . . . . . . . . . . . . 16 (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄)
5958a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐶[,]𝐷) → (∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄))
6059rabbiia 3156 . . . . . . . . . . . . . 14 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}
6160uneq2i 3721 . . . . . . . . . . . . 13 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})
6254, 61eqtri 2627 . . . . . . . . . . . 12 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})
6362fveq2i 6087 . . . . . . . . . . 11 (#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄}))
6463oveq1i 6533 . . . . . . . . . 10 ((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})) − 1)
65 fourierdlem97.v . . . . . . . . . 10 𝑉 = (℩𝑔𝑔 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})))
66 fourierdlem97.j . . . . . . . . . 10 (𝜑𝐽 ∈ (0..^((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)))
67 oveq1 6530 . . . . . . . . . . . . . 14 (𝑘 = → (𝑘 · 𝑇) = ( · 𝑇))
6867oveq2d 6539 . . . . . . . . . . . . 13 (𝑘 = → ((𝑄‘0) + (𝑘 · 𝑇)) = ((𝑄‘0) + ( · 𝑇)))
6968breq1d 4583 . . . . . . . . . . . 12 (𝑘 = → (((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽) ↔ ((𝑄‘0) + ( · 𝑇)) ≤ (𝑉𝐽)))
7069cbvrabv 3167 . . . . . . . . . . 11 {𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)} = { ∈ ℤ ∣ ((𝑄‘0) + ( · 𝑇)) ≤ (𝑉𝐽)}
7170supeq1i 8209 . . . . . . . . . 10 sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) = sup({ ∈ ℤ ∣ ((𝑄‘0) + ( · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < )
72 fveq2 6084 . . . . . . . . . . . . . 14 (𝑗 = 𝑒 → (𝑄𝑗) = (𝑄𝑒))
7372oveq1d 6538 . . . . . . . . . . . . 13 (𝑗 = 𝑒 → ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) = ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)))
7473breq1d 4583 . . . . . . . . . . . 12 (𝑗 = 𝑒 → (((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽) ↔ ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)))
7574cbvrabv 3167 . . . . . . . . . . 11 {𝑗 ∈ (0..^𝑀) ∣ ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)} = {𝑒 ∈ (0..^𝑀) ∣ ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}
7675supeq1i 8209 . . . . . . . . . 10 sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) = sup({𝑒 ∈ (0..^𝑀) ∣ ((𝑄𝑒) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < )
7730, 31, 32, 33, 34, 37, 42, 47, 64, 65, 66, 71, 76fourierdlem64 38863 . . . . . . . . 9 (𝜑 → ((sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄𝑗) + (sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) ∈ (0..^𝑀) ∧ sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉𝐽)}, ℝ, < ) ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
7877simprd 477 . . . . . . . 8 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
79 simpl1 1056 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝜑)
80 simpl2l 1106 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑖 ∈ (0..^𝑀))
81 fourierdlem97.qcn . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
82 cncff 22431 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
84 ffun 5943 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺:dom (ℝ D 𝐹)⟶ℝ → Fun 𝐺)
8512, 84syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun 𝐺)
8685adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → Fun 𝐺)
87 ffvresb 6282 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝐺 → ((𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ)))
8886, 87syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ↔ ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ)))
8983, 88mpbid 220 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ))
9089r19.21bi 2911 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 ∈ dom 𝐺 ∧ (𝐺𝑠) ∈ ℂ))
9190simpld 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ dom 𝐺)
9291ralrimiva 2944 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
93 dfss3 3553 . . . . . . . . . . . . . . . 16 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺 ↔ ∀𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑠 ∈ dom 𝐺)
9492, 93sylibr 222 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
9579, 80, 94syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐺)
96 simpl2 1057 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ))
9779, 96jca 552 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)))
98 simpl3 1058 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
99 simpr 475 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))))
10098, 99sseldd 3564 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
10131fourierdlem2 38802 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
10232, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
10333, 102mpbid 220 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
104103simpld 473 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
105 elmapi 7738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑄:(0...𝑀)⟶ℝ)
107106adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
108 elfzofz 12305 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
109108adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
110107, 109ffvelrnd 6249 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
111110rexrd 9941 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
112111adantrr 748 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄𝑖) ∈ ℝ*)
113112adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄𝑖) ∈ ℝ*)
114 fzofzp1 12382 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
115114adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
116107, 115ffvelrnd 6249 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
117116adantrr 748 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
118117adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
119118rexrd 9941 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
120 elioore 12028 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → 𝑡 ∈ ℝ)
121120adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ ℝ)
122 zre 11210 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ ℤ → 𝑙 ∈ ℝ)
123122adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
124123ad2antlr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑙 ∈ ℝ)
125 fourierdlem97.a . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℝ)
126 fourierdlem97.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ ℝ)
127125, 126resubcld 10305 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐵𝐴) ∈ ℝ)
12830, 127syl5eqel 2687 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ∈ ℝ)
129128ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑇 ∈ ℝ)
130124, 129remulcld 9922 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑙 · 𝑇) ∈ ℝ)
131121, 130resubcld 10305 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ℝ)
132110adantrr 748 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑄𝑖) ∈ ℝ)
133122ad2antll 760 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑙 ∈ ℝ)
134128adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → 𝑇 ∈ ℝ)
135133, 134remulcld 9922 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → (𝑙 · 𝑇) ∈ ℝ)
136132, 135readdcld 9921 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ)
137136rexrd 9941 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ*)
138137adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ*)
139117, 135readdcld 9921 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ)
140139rexrd 9941 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*)
141140adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*)
142 simpr 475 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
143 ioogtlb 38364 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄𝑖) + (𝑙 · 𝑇)) < 𝑡)
144138, 141, 142, 143syl3anc 1317 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑄𝑖) + (𝑙 · 𝑇)) < 𝑡)
145132adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄𝑖) ∈ ℝ)
146145, 130, 121ltaddsubd 10472 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (((𝑄𝑖) + (𝑙 · 𝑇)) < 𝑡 ↔ (𝑄𝑖) < (𝑡 − (𝑙 · 𝑇))))
147144, 146mpbid 220 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑄𝑖) < (𝑡 − (𝑙 · 𝑇)))
148 iooltub 38382 . . . . . . . . . . . . . . . . . 18 ((((𝑄𝑖) + (𝑙 · 𝑇)) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)) ∈ ℝ*𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
149138, 141, 142, 148syl3anc 1317 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))
150121, 130, 118ltsubaddd 10468 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)) ↔ 𝑡 < ((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))))
151149, 150mpbird 245 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) < (𝑄‘(𝑖 + 1)))
152113, 119, 131, 147, 151eliood 38367 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
15397, 100, 152syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
15495, 153sseldd 3564 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)
155 elioore 12028 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) → 𝑡 ∈ ℝ)
156 recn 9878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
157156adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
158 zcn 11211 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 ∈ ℤ → 𝑙 ∈ ℂ)
159158ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑙 ∈ ℂ)
160128recnd 9920 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑇 ∈ ℂ)
161160ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℂ)
162159, 161mulcld 9912 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝑙 · 𝑇) ∈ ℂ)
163157, 162npcand 10243 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) = 𝑡)
164163eqcomd 2611 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
165164adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
166 ovex 6551 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 − (𝑙 · 𝑇)) ∈ V
167 eleq1 2671 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 ∈ dom 𝐺 ↔ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺))
168167anbi2d 735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) ↔ ((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺)))
169 oveq1 6530 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝑠 + (𝑙 · 𝑇)) = ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)))
170169eleq1d 2667 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ↔ ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺))
171169fveq2d 6088 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))))
172 fveq2 6084 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (𝐺𝑠) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))
173171, 172eqeq12d 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠) ↔ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
174170, 173anbi12d 742 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → (((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠)) ↔ (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇))))))
175168, 174imbi12d 332 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑡 − (𝑙 · 𝑇)) → ((((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠))) ↔ (((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))))
176 ax-resscn 9845 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℂ
177176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ⊆ ℂ)
1786, 177fssd 5952 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:ℝ⟶ℂ)
179178adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑙 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
180122adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑙 ∈ ℤ) → 𝑙 ∈ ℝ)
181128adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑙 ∈ ℤ) → 𝑇 ∈ ℝ)
182180, 181remulcld 9922 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑙 ∈ ℤ) → (𝑙 · 𝑇) ∈ ℝ)
183178ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
184128ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑇 ∈ ℝ)
185 simplr 787 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑙 ∈ ℤ)
186 simpr 475 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → 𝑠 ∈ ℝ)
187 fourierdlem97.fper . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
188187ad4ant14 1284 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
189183, 184, 185, 186, 188fperiodmul 38258 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ ℝ) → (𝐹‘(𝑠 + (𝑙 · 𝑇))) = (𝐹𝑠))
190179, 182, 189, 10fperdvper 38608 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑙 ∈ ℤ) ∧ 𝑠 ∈ dom 𝐺) → ((𝑠 + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘(𝑠 + (𝑙 · 𝑇))) = (𝐺𝑠)))
191166, 175, 190vtocl 3227 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → (((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺 ∧ (𝐺‘((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇))) = (𝐺‘(𝑡 − (𝑙 · 𝑇)))))
192191simpld 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑙 ∈ ℤ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
193192adantlr 746 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → ((𝑡 − (𝑙 · 𝑇)) + (𝑙 · 𝑇)) ∈ dom 𝐺)
194165, 193eqeltrd 2683 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ (𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺) → 𝑡 ∈ dom 𝐺)
195194ex 448 . . . . . . . . . . . . . . . 16 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
196155, 195sylan2 489 . . . . . . . . . . . . . . 15 (((𝜑𝑙 ∈ ℤ) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
197196adantlrl 751 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ)) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
1981973adantl3 1211 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → ((𝑡 − (𝑙 · 𝑇)) ∈ dom 𝐺𝑡 ∈ dom 𝐺))
199154, 198mpd 15 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) ∧ 𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑡 ∈ dom 𝐺)
200199ralrimiva 2944 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ∀𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
201 dfss3 3553 . . . . . . . . . . 11 (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺 ↔ ∀𝑡 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))𝑡 ∈ dom 𝐺)
202200, 201sylibr 222 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) ∧ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
2032023exp 1255 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑙 ∈ ℤ) → (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)))
204203rexlimdvv 3014 . . . . . . . 8 (𝜑 → (∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇))) → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺))
20578, 204mpd 15 . . . . . . 7 (𝜑 → ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ dom 𝐺)
206205sselda 3563 . . . . . 6 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → 𝑠 ∈ dom 𝐺)
207206iftrued 4039 . . . . 5 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
20829, 207eqtr2d 2640 . . . 4 ((𝜑𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) → (𝐺𝑠) = (𝐻𝑠))
209208mpteq2dva 4662 . . 3 (𝜑 → (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺𝑠)) = (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻𝑠)))
21015a1i 11 . . . . . 6 (𝜑 → dom 𝐺 = dom (ℝ D 𝐹))
211210feq2d 5926 . . . . 5 (𝜑 → (𝐺:dom 𝐺⟶ℝ ↔ 𝐺:dom (ℝ D 𝐹)⟶ℝ))
21212, 211mpbird 245 . . . 4 (𝜑𝐺:dom 𝐺⟶ℝ)
213212, 205feqresmpt 6141 . . 3 (𝜑 → (𝐺 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐺𝑠)))
21425, 27fmptd 6273 . . . 4 (𝜑𝐻:ℝ⟶ℝ)
215214, 2feqresmpt 6141 . . 3 (𝜑 → (𝐻 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝑠 ∈ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1))) ↦ (𝐻𝑠)))
216209, 213, 2153eqtr4d 2649 . 2 (𝜑 → (𝐺 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) = (𝐻 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))))
217214, 177fssd 5952 . . 3 (𝜑𝐻:ℝ⟶ℂ)
21827a1i 11 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0)))
219 eleq1 2671 . . . . . . . . 9 (𝑠 = (𝑥 + 𝑇) → (𝑠 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
220 fveq2 6084 . . . . . . . . 9 (𝑠 = (𝑥 + 𝑇) → (𝐺𝑠) = (𝐺‘(𝑥 + 𝑇)))
221219, 220ifbieq1d 4054 . . . . . . . 8 (𝑠 = (𝑥 + 𝑇) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
222178, 128, 187, 10fperdvper 38608 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺𝑥)))
223222simpld 473 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
224223iftrued 4039 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = (𝐺‘(𝑥 + 𝑇)))
225221, 224sylan9eqr 2661 . . . . . . 7 (((𝜑𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
226225adantllr 750 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺‘(𝑥 + 𝑇)))
227 simpr 475 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
228128adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229227, 228readdcld 9921 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℝ)
230229adantr 479 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
231212ad2antrr 757 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝐺:dom 𝐺⟶ℝ)
232223adantlr 746 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
233231, 232ffvelrnd 6249 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) ∈ ℝ)
234218, 226, 230, 233fvmptd 6178 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
235222simprd 477 . . . . . 6 ((𝜑𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺𝑥))
236235adantlr 746 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘(𝑥 + 𝑇)) = (𝐺𝑥))
237 eleq1 2671 . . . . . . . . 9 (𝑠 = 𝑥 → (𝑠 ∈ dom 𝐺𝑥 ∈ dom 𝐺))
238 fveq2 6084 . . . . . . . . 9 (𝑠 = 𝑥 → (𝐺𝑠) = (𝐺𝑥))
239237, 238ifbieq1d 4054 . . . . . . . 8 (𝑠 = 𝑥 → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0))
240239adantl 480 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0))
241 simplr 787 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
242 simpr 475 . . . . . . . . . 10 ((𝜑𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
243242iftrued 4039 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) = (𝐺𝑥))
244212ffvelrnda 6248 . . . . . . . . 9 ((𝜑𝑥 ∈ dom 𝐺) → (𝐺𝑥) ∈ ℝ)
245243, 244eqeltrd 2683 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) ∈ ℝ)
246245adantlr 746 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) ∈ ℝ)
247218, 240, 241, 246fvmptd 6178 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻𝑥) = if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0))
248 simpr 475 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
249248iftrued 4039 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) = (𝐺𝑥))
250247, 249eqtr2d 2640 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐺𝑥) = (𝐻𝑥))
251234, 236, 2503eqtrd 2643 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻𝑥))
252229recnd 9920 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → (𝑥 + 𝑇) ∈ ℂ)
253228recnd 9920 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
254252, 253negsubd 10245 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → ((𝑥 + 𝑇) + -𝑇) = ((𝑥 + 𝑇) − 𝑇))
255227recnd 9920 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
256255, 253pncand 10240 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
257254, 256eqtr2d 2640 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
258257adantr 479 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 = ((𝑥 + 𝑇) + -𝑇))
259 simpr 475 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ dom 𝐺)
260 simpll 785 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝜑)
261260, 259jca 552 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺))
262 eleq1 2671 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 𝑇) → (𝑦 ∈ dom 𝐺 ↔ (𝑥 + 𝑇) ∈ dom 𝐺))
263262anbi2d 735 . . . . . . . . . . . 12 (𝑦 = (𝑥 + 𝑇) → ((𝜑𝑦 ∈ dom 𝐺) ↔ (𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺)))
264 oveq1 6530 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 + 𝑇) → (𝑦 + -𝑇) = ((𝑥 + 𝑇) + -𝑇))
265264eleq1d 2667 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 𝑇) → ((𝑦 + -𝑇) ∈ dom 𝐺 ↔ ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺))
266264fveq2d 6088 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 + 𝑇) → (𝐺‘(𝑦 + -𝑇)) = (𝐺‘((𝑥 + 𝑇) + -𝑇)))
267 fveq2 6084 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 + 𝑇) → (𝐺𝑦) = (𝐺‘(𝑥 + 𝑇)))
268266, 267eqeq12d 2620 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + 𝑇) → ((𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦) ↔ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
269265, 268anbi12d 742 . . . . . . . . . . . 12 (𝑦 = (𝑥 + 𝑇) → (((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦)) ↔ (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
270263, 269imbi12d 332 . . . . . . . . . . 11 (𝑦 = (𝑥 + 𝑇) → (((𝜑𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦))) ↔ ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))))
271128renegcld 10304 . . . . . . . . . . . 12 (𝜑 → -𝑇 ∈ ℝ)
272160mulm1d 10328 . . . . . . . . . . . . . . . . 17 (𝜑 → (-1 · 𝑇) = -𝑇)
273272eqcomd 2611 . . . . . . . . . . . . . . . 16 (𝜑 → -𝑇 = (-1 · 𝑇))
274273adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → -𝑇 = (-1 · 𝑇))
275274oveq2d 6539 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝑦 + -𝑇) = (𝑦 + (-1 · 𝑇)))
276275fveq2d 6088 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹‘(𝑦 + (-1 · 𝑇))))
277178adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
278128adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
279 1zzd 11237 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 1 ∈ ℤ)
280279znegcld 11312 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → -1 ∈ ℤ)
281 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
282187adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
283277, 278, 280, 281, 282fperiodmul 38258 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + (-1 · 𝑇))) = (𝐹𝑦))
284276, 283eqtrd 2639 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + -𝑇)) = (𝐹𝑦))
285178, 271, 284, 10fperdvper 38608 . . . . . . . . . . 11 ((𝜑𝑦 ∈ dom 𝐺) → ((𝑦 + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑦 + -𝑇)) = (𝐺𝑦)))
286270, 285vtoclg 3234 . . . . . . . . . 10 ((𝑥 + 𝑇) ∈ dom 𝐺 → ((𝜑 ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇)))))
287259, 261, 286sylc 62 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → (((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺 ∧ (𝐺‘((𝑥 + 𝑇) + -𝑇)) = (𝐺‘(𝑥 + 𝑇))))
288287simpld 473 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → ((𝑥 + 𝑇) + -𝑇) ∈ dom 𝐺)
289258, 288eqeltrd 2683 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ (𝑥 + 𝑇) ∈ dom 𝐺) → 𝑥 ∈ dom 𝐺)
290289stoic1a 1687 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ (𝑥 + 𝑇) ∈ dom 𝐺)
291290iffalsed 4042 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) = 0)
29227a1i 11 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝐻 = (𝑠 ∈ ℝ ↦ if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0)))
293221adantl 480 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = (𝑥 + 𝑇)) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
294229adantr 479 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
295 0red 9893 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 0 ∈ ℝ)
296291, 295eqeltrd 2683 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0) ∈ ℝ)
297292, 293, 294, 296fvmptd 6178 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = if((𝑥 + 𝑇) ∈ dom 𝐺, (𝐺‘(𝑥 + 𝑇)), 0))
298 simpr 475 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → ¬ 𝑥 ∈ dom 𝐺)
299298iffalsed 4042 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → if(𝑥 ∈ dom 𝐺, (𝐺𝑥), 0) = 0)
300239, 299sylan9eqr 2661 . . . . . 6 ((((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) ∧ 𝑠 = 𝑥) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = 0)
301 simplr 787 . . . . . 6 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
302292, 300, 301, 295fvmptd 6178 . . . . 5 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻𝑥) = 0)
303291, 297, 3023eqtr4d 2649 . . . 4 (((𝜑𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ dom 𝐺) → (𝐻‘(𝑥 + 𝑇)) = (𝐻𝑥))
304251, 303pm2.61dan 827 . . 3 ((𝜑𝑥 ∈ ℝ) → (𝐻‘(𝑥 + 𝑇)) = (𝐻𝑥))
305 elioore 12028 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
306305adantl 480 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
307305, 25sylan2 489 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) ∈ ℝ)
308306, 307, 28syl2anc 690 . . . . . . . 8 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
309308adantlr 746 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0))
31091iftrued 4039 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 ∈ dom 𝐺, (𝐺𝑠), 0) = (𝐺𝑠))
311309, 310eqtrd 2639 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = (𝐺𝑠))
312311mpteq2dva 4662 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺𝑠)))
313214adantr 479 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻:ℝ⟶ℝ)
314 ioossre 12058 . . . . . . 7 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
315314a1i 11 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
316313, 315feqresmpt 6141 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)))
317212adantr 479 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐺:dom 𝐺⟶ℝ)
318317, 94feqresmpt 6141 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐺𝑠)))
319312, 316, 3183eqtr4d 2649 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
320319, 81eqeltrd 2683 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
321 eqid 2605 . . 3 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
322 oveq1 6530 . . . . . . . 8 (𝑧 = 𝑦 → (𝑧 + (𝑙 · 𝑇)) = (𝑦 + (𝑙 · 𝑇)))
323322eleq1d 2667 . . . . . . 7 (𝑧 = 𝑦 → ((𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
324323rexbidv 3029 . . . . . 6 (𝑧 = 𝑦 → (∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄))
325324cbvrabv 3167 . . . . 5 {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}
326325uneq2i 3721 . . . 4 ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})
327326eqcomi 2614 . . 3 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑧 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑧 + (𝑙 · 𝑇)) ∈ ran 𝑄})
32854fveq2i 6087 . . . 4 (#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))
329328oveq1i 6533 . . 3 ((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) − 1)
330 isoeq5 6445 . . . . . 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 5772 . . . 4 (℩𝑔𝑔 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃ ∈ ℤ (𝑦 + ( · 𝑇)) ∈ ran 𝑄})))
333 isoeq1 6441 . . . . 5 (𝑓 = 𝑔 → (𝑓 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))))
334333cbviotav 5756 . . . 4 (℩𝑓𝑓 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑔𝑔 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
335332, 334, 653eqtr4ri 2638 . . 3 𝑉 = (℩𝑓𝑓 Isom < , < ((0...((#‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑙 ∈ ℤ (𝑦 + (𝑙 · 𝑇)) ∈ ran 𝑄})))
336 id 22 . . . . 5 (𝑣 = 𝑥𝑣 = 𝑥)
337 oveq2 6531 . . . . . . . 8 (𝑣 = 𝑥 → (𝐵𝑣) = (𝐵𝑥))
338337oveq1d 6538 . . . . . . 7 (𝑣 = 𝑥 → ((𝐵𝑣) / 𝑇) = ((𝐵𝑥) / 𝑇))
339338fveq2d 6088 . . . . . 6 (𝑣 = 𝑥 → (⌊‘((𝐵𝑣) / 𝑇)) = (⌊‘((𝐵𝑥) / 𝑇)))
340339oveq1d 6538 . . . . 5 (𝑣 = 𝑥 → ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))
341336, 340oveq12d 6541 . . . 4 (𝑣 = 𝑥 → (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
342341cbvmptv 4668 . . 3 (𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
343 eqeq1 2609 . . . . 5 (𝑢 = 𝑧 → (𝑢 = 𝐵𝑧 = 𝐵))
344 id 22 . . . . 5 (𝑢 = 𝑧𝑢 = 𝑧)
345343, 344ifbieq2d 4056 . . . 4 (𝑢 = 𝑧 → if(𝑢 = 𝐵, 𝐴, 𝑢) = if(𝑧 = 𝐵, 𝐴, 𝑧))
346345cbvmptv 4668 . . 3 (𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢)) = (𝑧 ∈ (𝐴(,]𝐵) ↦ if(𝑧 = 𝐵, 𝐴, 𝑧))
347 eqid 2605 . . 3 ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))) = ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))
348 eqid 2605 . . 3 (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))) = (𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))
349 eqid 2605 . . 3 (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))))))) = (𝑧 ∈ ((((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))(,)(((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1))) + ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))) ↦ ((𝐻 ↾ (((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉𝐽)))(,)((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))‘(𝑧 − ((𝑉‘(𝐽 + 1)) − ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘(𝑉‘(𝐽 + 1)))))))
350 fveq2 6084 . . . . . . . 8 (𝑖 = 𝑡 → (𝑄𝑖) = (𝑄𝑡))
351350breq1d 4583 . . . . . . 7 (𝑖 = 𝑡 → ((𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))))
352351cbvrabv 3167 . . . . . 6 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))}
353 fveq2 6084 . . . . . . . . . 10 (𝑤 = 𝑥 → ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤) = ((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))
354353fveq2d 6088 . . . . . . . . 9 (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)))
355354eqcomd 2611 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)) = ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤)))
356355breq2d 4585 . . . . . . 7 (𝑤 = 𝑥 → ((𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))))
357356rabbidv 3159 . . . . . 6 (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))})
358352, 357syl5req 2652 . . . . 5 (𝑤 = 𝑥 → {𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))})
359358supeq1d 8208 . . . 4 (𝑤 = 𝑥 → sup({𝑡 ∈ (0..^𝑀) ∣ (𝑄𝑡) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑤))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ ((𝑢 ∈ (𝐴(,]𝐵) ↦ if(𝑢 = 𝐵, 𝐴, 𝑢))‘((𝑣 ∈ ℝ ↦ (𝑣 + ((⌊‘((𝐵𝑣) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < ))
360359cbvmptv 4668 . . 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 38889 . 2 (𝜑 → (𝐻 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
362216, 361eqeltrd 2683 1 (𝜑 → (𝐺 ↾ ((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))) ∈ (((𝑉𝐽)(,)(𝑉‘(𝐽 + 1)))–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1975  wral 2891  wrex 2892  {crab 2895  cun 3533  wss 3535  ifcif 4031  {cpr 4122   class class class wbr 4573  cmpt 4633  dom cdm 5024  ran crn 5025  cres 5026  cio 5748  Fun wfun 5780  wf 5782  cfv 5786   Isom wiso 5787  (class class class)co 6523  𝑚 cmap 7717  supcsup 8202  cc 9786  cr 9787  0cc0 9788  1c1 9789   + caddc 9791   · cmul 9793  +∞cpnf 9923  *cxr 9925   < clt 9926  cle 9927  cmin 10113  -cneg 10114   / cdiv 10529  cn 10863  cz 11206  (,)cioo 11998  (,]cioc 11999  [,]cicc 12001  ...cfz 12148  ..^cfzo 12285  cfl 12404  #chash 12930  cnccncf 22414   D cdv 23346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-iin 4448  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-fi 8173  df-sup 8204  df-inf 8205  df-oi 8271  df-card 8621  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-4 10924  df-5 10925  df-6 10926  df-7 10927  df-8 10928  df-9 10929  df-n0 11136  df-z 11207  df-dec 11322  df-uz 11516  df-q 11617  df-rp 11661  df-xneg 11774  df-xadd 11775  df-xmul 11776  df-ioo 12002  df-ioc 12003  df-ico 12004  df-icc 12005  df-fz 12149  df-fzo 12286  df-fl 12406  df-seq 12615  df-exp 12674  df-hash 12931  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-struct 15639  df-ndx 15640  df-slot 15641  df-base 15642  df-plusg 15723  df-mulr 15724  df-starv 15725  df-tset 15729  df-ple 15730  df-ds 15733  df-unif 15734  df-rest 15848  df-topn 15849  df-topgen 15869  df-psmet 19501  df-xmet 19502  df-met 19503  df-bl 19504  df-mopn 19505  df-fbas 19506  df-fg 19507  df-cnfld 19510  df-top 20459  df-bases 20460  df-topon 20461  df-topsp 20462  df-cld 20571  df-ntr 20572  df-cls 20573  df-nei 20650  df-lp 20688  df-perf 20689  df-cn 20779  df-cnp 20780  df-haus 20867  df-cmp 20938  df-fil 21398  df-fm 21490  df-flim 21491  df-flf 21492  df-xms 21872  df-ms 21873  df-cncf 22416  df-limc 23349  df-dv 23350
This theorem is referenced by:  fourierdlem112  38911
  Copyright terms: Public domain W3C validator