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

Theorem fourierdlem107 44349
Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 44334 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem107.a (𝜑𝐴 ∈ ℝ)
fourierdlem107.b (𝜑𝐵 ∈ ℝ)
fourierdlem107.t 𝑇 = (𝐵𝐴)
fourierdlem107.x (𝜑𝑋 ∈ ℝ+)
fourierdlem107.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem107.m (𝜑𝑀 ∈ ℕ)
fourierdlem107.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem107.f (𝜑𝐹:ℝ⟶ℂ)
fourierdlem107.fper ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
fourierdlem107.fcn ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem107.r ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
fourierdlem107.l ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
fourierdlem107.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem107.h 𝐻 = ({(𝐴𝑋), 𝐴} ∪ {𝑦 ∈ ((𝐴𝑋)[,]𝐴) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem107.n 𝑁 = ((♯‘𝐻) − 1)
fourierdlem107.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem107.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
fourierdlem107.z 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem107.i 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝑍‘(𝐸𝑥))}, ℝ, < ))
Assertion
Ref Expression
fourierdlem107 (𝜑 → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Distinct variable groups:   𝐴,𝑓,𝑘,𝑦   𝐴,𝑖,𝑥,𝑘,𝑦   𝐴,𝑚,𝑝,𝑖   𝐵,𝑓,𝑘,𝑦   𝐵,𝑖,𝑥   𝐵,𝑚,𝑝   𝑓,𝐸,𝑘,𝑦   𝑖,𝐸,𝑥   𝑖,𝐹,𝑥,𝑦   𝑓,𝐻,𝑦   𝑥,𝐻   𝑓,𝐼,𝑘,𝑦   𝑖,𝐼,𝑥   𝑥,𝐿,𝑦   𝑖,𝑀,𝑥,𝑦   𝑚,𝑀,𝑝   𝑓,𝑁,𝑘,𝑦   𝑖,𝑁,𝑥   𝑚,𝑁,𝑝   𝑄,𝑓,𝑘,𝑦   𝑄,𝑖,𝑥   𝑄,𝑚,𝑝   𝑥,𝑅,𝑦   𝑆,𝑓,𝑘,𝑦   𝑆,𝑖,𝑥   𝑆,𝑝   𝑇,𝑓,𝑘,𝑦   𝑇,𝑖,𝑥   𝑇,𝑚,𝑝   𝑓,𝑋,𝑦   𝑖,𝑋,𝑚,𝑝   𝑥,𝑋   𝑖,𝑍,𝑥,𝑦   𝜑,𝑓,𝑘,𝑦   𝜑,𝑖,𝑥
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝑃(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝)   𝑅(𝑓,𝑖,𝑘,𝑚,𝑝)   𝑆(𝑚)   𝐸(𝑚,𝑝)   𝐹(𝑓,𝑘,𝑚,𝑝)   𝐻(𝑖,𝑘,𝑚,𝑝)   𝐼(𝑚,𝑝)   𝐿(𝑓,𝑖,𝑘,𝑚,𝑝)   𝑀(𝑓,𝑘)   𝑂(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝)   𝑋(𝑘)   𝑍(𝑓,𝑘,𝑚,𝑝)

Proof of Theorem fourierdlem107
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem107.t . . . . . . . . . . . . . . . . 17 𝑇 = (𝐵𝐴)
21oveq2i 7362 . . . . . . . . . . . . . . . 16 ((𝐴𝑋) + 𝑇) = ((𝐴𝑋) + (𝐵𝐴))
3 fourierdlem107.a . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ ℝ)
43recnd 11141 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℂ)
5 fourierdlem107.x . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℝ+)
65rpred 12911 . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ ℝ)
76recnd 11141 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
8 fourierdlem107.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℝ)
98recnd 11141 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℂ)
104, 7, 9, 4subadd4b 43415 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑋) + (𝐵𝐴)) = ((𝐴𝐴) + (𝐵𝑋)))
112, 10eqtrid 2788 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝑋) + 𝑇) = ((𝐴𝐴) + (𝐵𝑋)))
124subidd 11458 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐴) = 0)
1312oveq1d 7366 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝐴) + (𝐵𝑋)) = (0 + (𝐵𝑋)))
148, 6resubcld 11541 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑋) ∈ ℝ)
1514recnd 11141 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
1615addid2d 11314 . . . . . . . . . . . . . . 15 (𝜑 → (0 + (𝐵𝑋)) = (𝐵𝑋))
1711, 13, 163eqtrd 2780 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝑋) + 𝑇) = (𝐵𝑋))
181oveq2i 7362 . . . . . . . . . . . . . . 15 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
194, 9pncan3d 11473 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
2018, 19eqtrid 2788 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 + 𝑇) = 𝐵)
2117, 20oveq12d 7369 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵𝑋)[,]𝐵))
2221eqcomd 2742 . . . . . . . . . . . 12 (𝜑 → ((𝐵𝑋)[,]𝐵) = (((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇)))
2322itgeq1d 44093 . . . . . . . . . . 11 (𝜑 → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹𝑥) d𝑥)
243, 6resubcld 11541 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑋) ∈ ℝ)
25 fourierdlem107.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
26 fveq2 6839 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑝𝑖) = (𝑝𝑗))
27 oveq1 7358 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
2827fveq2d 6843 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
2926, 28breq12d 5116 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝𝑗) < (𝑝‘(𝑗 + 1))))
3029cbvralvw 3223 . . . . . . . . . . . . . . . . 17 (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))
3130a1i 11 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1))))
3231anbi2d 629 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → ((((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))))
3332rabbidv 3413 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
3433mpteq2ia 5206 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
3525, 34eqtri 2764 . . . . . . . . . . . 12 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
36 fourierdlem107.p . . . . . . . . . . . . . . 15 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
37 fourierdlem107.m . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ)
38 fourierdlem107.q . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (𝑃𝑀))
393, 5ltsubrpd 12943 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝑋) < 𝐴)
40 fourierdlem107.h . . . . . . . . . . . . . . 15 𝐻 = ({(𝐴𝑋), 𝐴} ∪ {𝑦 ∈ ((𝐴𝑋)[,]𝐴) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
41 fourierdlem107.n . . . . . . . . . . . . . . 15 𝑁 = ((♯‘𝐻) − 1)
42 fourierdlem107.s . . . . . . . . . . . . . . 15 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
431, 36, 37, 38, 24, 3, 39, 25, 40, 41, 42fourierdlem54 44296 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
4443simpld 495 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
4544simpld 495 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
468, 3resubcld 11541 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℝ)
471, 46eqeltrid 2842 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
4844simprd 496 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝑂𝑁))
4924adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐴𝑋) ∈ ℝ)
503adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴𝑋)[,]𝐴))
52 eliccre 43638 . . . . . . . . . . . . . 14 (((𝐴𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
5349, 50, 51, 52syl3anc 1371 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54 fourierdlem107.fper . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
5553, 54syldan 591 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
56 fveq2 6839 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑆𝑖) = (𝑆𝑗))
5756oveq1d 7366 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝑆𝑖) + 𝑇) = ((𝑆𝑗) + 𝑇))
5857cbvmptv 5216 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑁) ↦ ((𝑆𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆𝑗) + 𝑇))
59 eqid 2736 . . . . . . . . . . . 12 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴𝑋) + 𝑇) ∧ (𝑝𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴𝑋) + 𝑇) ∧ (𝑝𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
60 fourierdlem107.f . . . . . . . . . . . 12 (𝜑𝐹:ℝ⟶ℂ)
6137adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
6238adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃𝑀))
6360adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
6454adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
65 fourierdlem107.fcn . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
6665adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
6724adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴𝑋) ∈ ℝ)
6867rexrd 11163 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴𝑋) ∈ ℝ*)
69 pnfxr 11167 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
7069a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ*)
713adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
7239adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴𝑋) < 𝐴)
733ltpnfd 12996 . . . . . . . . . . . . . . 15 (𝜑𝐴 < +∞)
7473adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
7568, 70, 71, 72, 74eliood 43631 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ((𝐴𝑋)(,)+∞))
76 fourierdlem107.e . . . . . . . . . . . . 13 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
77 fourierdlem107.z . . . . . . . . . . . . 13 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
78 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
79 eqid 2736 . . . . . . . . . . . . 13 ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
80 eqid 2736 . . . . . . . . . . . . 13 (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
81 eqid 2736 . . . . . . . . . . . . 13 (𝑦 ∈ (((𝑍‘(𝐸‘(𝑆𝑗))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))(,)((𝐸‘(𝑆‘(𝑗 + 1))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))) ↦ ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))‘(𝑦 − ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))))) = (𝑦 ∈ (((𝑍‘(𝐸‘(𝑆𝑗))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))(,)((𝐸‘(𝑆‘(𝑗 + 1))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))) ↦ ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))‘(𝑦 − ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))))
82 fourierdlem107.i . . . . . . . . . . . . 13 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝑍‘(𝐸𝑥))}, ℝ, < ))
8336, 1, 61, 62, 63, 64, 66, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 80, 81, 82fourierdlem90 44332 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84 fourierdlem107.r . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
8584adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
86 eqid 2736 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) ↦ 𝑅) = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
8736, 1, 61, 62, 63, 64, 66, 85, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 86fourierdlem89 44331 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝑍‘(𝐸‘(𝑆𝑗))) = (𝑄‘(𝐼‘(𝑆𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝑍‘(𝐸‘(𝑆𝑗))))) ∈ ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
88 fourierdlem107.l . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
8988adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
90 eqid 2736 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) ↦ 𝐿) = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
9136, 1, 61, 62, 63, 64, 66, 89, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 90fourierdlem91 44333 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
9224, 3, 35, 45, 47, 48, 55, 58, 59, 60, 83, 87, 91fourierdlem92 44334 . . . . . . . . . . 11 (𝜑 → ∫(((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
9323, 92eqtrd 2776 . . . . . . . . . 10 (𝜑 → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
9460adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
9514adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → (𝐵𝑋) ∈ ℝ)
968adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵𝑋)[,]𝐵))
98 eliccre 43638 . . . . . . . . . . . . 13 (((𝐵𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
9995, 96, 97, 98syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
10094, 99ffvelcdmd 7032 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
10114rexrd 11163 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝑋) ∈ ℝ*)
10269a1i 11 . . . . . . . . . . . . 13 (𝜑 → +∞ ∈ ℝ*)
1038, 5ltsubrpd 12943 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝑋) < 𝐵)
1048ltpnfd 12996 . . . . . . . . . . . . 13 (𝜑𝐵 < +∞)
105101, 102, 8, 103, 104eliood 43631 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ((𝐵𝑋)(,)+∞))
10636, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105fourierdlem105 44347 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ((𝐵𝑋)[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
107100, 106itgcl 25094 . . . . . . . . . 10 (𝜑 → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
10893, 107eqeltrrd 2839 . . . . . . . . 9 (𝜑 → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
109108subidd 11458 . . . . . . . 8 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = 0)
110109eqcomd 2742 . . . . . . 7 (𝜑 → 0 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
111110adantr 481 . . . . . 6 ((𝜑𝑇 < 𝑋) → 0 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
11224adantr 481 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝐴𝑋) ∈ ℝ)
1133adantr 481 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → 𝐴 ∈ ℝ)
11414adantr 481 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ∈ ℝ)
11536, 37, 38fourierdlem11 44254 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116115simp3d 1144 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
1173, 8, 116ltled 11261 . . . . . . . . . . 11 (𝜑𝐴𝐵)
118117adantr 481 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → 𝐴𝐵)
1193, 8, 6lesub1d 11720 . . . . . . . . . . 11 (𝜑 → (𝐴𝐵 ↔ (𝐴𝑋) ≤ (𝐵𝑋)))
120119adantr 481 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (𝐴𝐵 ↔ (𝐴𝑋) ≤ (𝐵𝑋)))
121118, 120mpbid 231 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝐴𝑋) ≤ (𝐵𝑋))
1228adantr 481 . . . . . . . . . . 11 ((𝜑𝑇 < 𝑋) → 𝐵 ∈ ℝ)
1236adantr 481 . . . . . . . . . . 11 ((𝜑𝑇 < 𝑋) → 𝑋 ∈ ℝ)
124 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑇 < 𝑋) → 𝑇 < 𝑋)
1251, 124eqbrtrrid 5139 . . . . . . . . . . 11 ((𝜑𝑇 < 𝑋) → (𝐵𝐴) < 𝑋)
126122, 113, 123, 125ltsub23d 11718 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) < 𝐴)
127114, 113, 126ltled 11261 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ≤ 𝐴)
128112, 113, 114, 121, 127eliccd 43637 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ∈ ((𝐴𝑋)[,]𝐴))
12960adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130129, 53ffvelcdmd 7032 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
131130adantlr 713 . . . . . . . 8 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
13224rexrd 11163 . . . . . . . . . . 11 (𝜑 → (𝐴𝑋) ∈ ℝ*)
1333, 8, 6, 116ltsub1dd 11725 . . . . . . . . . . 11 (𝜑 → (𝐴𝑋) < (𝐵𝑋))
13414ltpnfd 12996 . . . . . . . . . . 11 (𝜑 → (𝐵𝑋) < +∞)
135132, 102, 14, 133, 134eliood 43631 . . . . . . . . . 10 (𝜑 → (𝐵𝑋) ∈ ((𝐴𝑋)(,)+∞))
13636, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135fourierdlem105 44347 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
137136adantr 481 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
13837adantr 481 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝑀 ∈ ℕ)
13938adantr 481 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝑄 ∈ (𝑃𝑀))
14060adantr 481 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝐹:ℝ⟶ℂ)
14154adantlr 713 . . . . . . . . 9 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
14265adantlr 713 . . . . . . . . 9 (((𝜑𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
14384adantlr 713 . . . . . . . . 9 (((𝜑𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
14488adantlr 713 . . . . . . . . 9 (((𝜑𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
145101adantr 481 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ∈ ℝ*)
14669a1i 11 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → +∞ ∈ ℝ*)
147113ltpnfd 12996 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → 𝐴 < +∞)
148145, 146, 113, 126, 147eliood 43631 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝐴 ∈ ((𝐵𝑋)(,)+∞))
14936, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148fourierdlem105 44347 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝑥 ∈ ((𝐵𝑋)[,]𝐴) ↦ (𝐹𝑥)) ∈ 𝐿1)
150112, 113, 128, 131, 137, 149itgspliticc 25147 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
151150oveq1d 7366 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
15260adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝐹:ℝ⟶ℂ)
15324adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐴𝑋) ∈ ℝ)
15414adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐵𝑋) ∈ ℝ)
155 simpr 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋)))
156 eliccre 43638 . . . . . . . . . . 11 (((𝐴𝑋) ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
157153, 154, 155, 156syl3anc 1371 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
158152, 157ffvelcdmd 7032 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐹𝑥) ∈ ℂ)
159158, 136itgcl 25094 . . . . . . . 8 (𝜑 → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 ∈ ℂ)
160159adantr 481 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 ∈ ℂ)
16160adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
16214adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → (𝐵𝑋) ∈ ℝ)
1633adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
164 simpr 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐵𝑋)[,]𝐴))
165 eliccre 43638 . . . . . . . . . . 11 (((𝐵𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166162, 163, 164, 165syl3anc 1371 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167161, 166ffvelcdmd 7032 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
168167adantlr 713 . . . . . . . 8 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
169168, 149itgcl 25094 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
170108adantr 481 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
171160, 169, 170addsubassd 11490 . . . . . 6 ((𝜑𝑇 < 𝑋) → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
172111, 151, 1713eqtrd 2780 . . . . 5 ((𝜑𝑇 < 𝑋) → 0 = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
173172oveq2d 7367 . . . 4 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − 0) = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))))
174160subid1d 11459 . . . 4 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − 0) = ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥)
175159subidd 11458 . . . . . . 7 (𝜑 → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) = 0)
176175oveq1d 7366 . . . . . 6 (𝜑 → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
177176adantr 481 . . . . 5 ((𝜑𝑇 < 𝑋) → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
178169, 170subcld 11470 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) ∈ ℂ)
179160, 160, 178subsub4d 11501 . . . . 5 ((𝜑𝑇 < 𝑋) → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))))
180 df-neg 11346 . . . . . 6 -(∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
181169, 170negsubdi2d 11486 . . . . . 6 ((𝜑𝑇 < 𝑋) → -(∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
182180, 181eqtr3id 2790 . . . . 5 ((𝜑𝑇 < 𝑋) → (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
183177, 179, 1823eqtr3d 2784 . . . 4 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
184173, 174, 1833eqtr3d 2784 . . 3 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
185107subidd 11458 . . . . . . . 8 (𝜑 → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = 0)
186185eqcomd 2742 . . . . . . 7 (𝜑 → 0 = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
187186oveq2d 7367 . . . . . 6 (𝜑 → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + 0) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
188187adantr 481 . . . . 5 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + 0) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
189169addid1d 11313 . . . . 5 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + 0) = ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
190114, 122, 113, 127, 118eliccd 43637 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝐴 ∈ ((𝐵𝑋)[,]𝐵))
191100adantlr 713 . . . . . . . . 9 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
1923, 8iccssred 13305 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
19360, 192feqresmpt 6908 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)))
19460, 192fssresd 6706 . . . . . . . . . . . 12 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195 ioossicc 13304 . . . . . . . . . . . . . . 15 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
1963rexrd 11163 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ*)
197196adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
1988rexrd 11163 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
199198adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
20036, 37, 38fourierdlem15 44258 . . . . . . . . . . . . . . . . 17 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201200adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203197, 199, 201, 202fourierdlem8 44251 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204195, 203sstrid 3953 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205204resabs1d 5966 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
206205, 65eqeltrd 2838 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207205eqcomd 2742 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
208207oveq1d 7366 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
20984, 208eleqtrd 2840 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
210207oveq1d 7366 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
21188, 210eleqtrd 2840 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
21236, 37, 38, 194, 206, 209, 211fourierdlem69 44311 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿1)
213193, 212eqeltrrd 2839 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
214213adantr 481 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
215114, 122, 190, 191, 149, 214itgspliticc 25147 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
216215oveq2d 7367 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
217216oveq2d 7367 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))))
218107adantr 481 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
219215, 218eqeltrrd 2839 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) ∈ ℂ)
220169, 218, 219addsub12d 11493 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))))
22160adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ)
2223adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
2238adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
224 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
225 eliccre 43638 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226222, 223, 224, 225syl3anc 1371 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227221, 226ffvelcdmd 7032 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
228227, 213itgcl 25094 . . . . . . . . . . 11 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
229228adantr 481 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
230169, 169, 229subsub4d 11501 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
231230eqcomd 2742 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
232231oveq2d 7367 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
233169subidd 11458 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = 0)
234233oveq1d 7366 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
235 df-neg 11346 . . . . . . . . 9 -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
236234, 235eqtr4di 2794 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
237236oveq2d 7367 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
238218, 229negsubd 11476 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
239232, 237, 2383eqtrd 2780 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
240217, 220, 2393eqtrd 2780 . . . . 5 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
241188, 189, 2403eqtr3d 2784 . . . 4 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
242241oveq2d 7367 . . 3 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
243108, 107, 228subsubd 11498 . . . . 5 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ((∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
24493oveq2d 7367 . . . . . . 7 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
245244, 109eqtrd 2776 . . . . . 6 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = 0)
246245oveq1d 7366 . . . . 5 (𝜑 → ((∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
247228addid2d 11314 . . . . 5 (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
248243, 246, 2473eqtrd 2780 . . . 4 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
249248adantr 481 . . 3 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
250184, 242, 2493eqtrd 2780 . 2 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
25124adantr 481 . . . . 5 ((𝜑𝑋𝑇) → (𝐴𝑋) ∈ ℝ)
25214adantr 481 . . . . 5 ((𝜑𝑋𝑇) → (𝐵𝑋) ∈ ℝ)
2533adantr 481 . . . . . 6 ((𝜑𝑋𝑇) → 𝐴 ∈ ℝ)
25424, 3, 39ltled 11261 . . . . . . 7 (𝜑 → (𝐴𝑋) ≤ 𝐴)
255254adantr 481 . . . . . 6 ((𝜑𝑋𝑇) → (𝐴𝑋) ≤ 𝐴)
2566adantr 481 . . . . . . 7 ((𝜑𝑋𝑇) → 𝑋 ∈ ℝ)
2578adantr 481 . . . . . . 7 ((𝜑𝑋𝑇) → 𝐵 ∈ ℝ)
258 id 22 . . . . . . . . 9 (𝑋𝑇𝑋𝑇)
259258, 1breqtrdi 5144 . . . . . . . 8 (𝑋𝑇𝑋 ≤ (𝐵𝐴))
260259adantl 482 . . . . . . 7 ((𝜑𝑋𝑇) → 𝑋 ≤ (𝐵𝐴))
261256, 257, 253, 260lesubd 11717 . . . . . 6 ((𝜑𝑋𝑇) → 𝐴 ≤ (𝐵𝑋))
262251, 252, 253, 255, 261eliccd 43637 . . . . 5 ((𝜑𝑋𝑇) → 𝐴 ∈ ((𝐴𝑋)[,](𝐵𝑋)))
263158adantlr 713 . . . . 5 (((𝜑𝑋𝑇) ∧ 𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐹𝑥) ∈ ℂ)
264132, 102, 3, 39, 73eliood 43631 . . . . . . 7 (𝜑𝐴 ∈ ((𝐴𝑋)(,)+∞))
26536, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264fourierdlem105 44347 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐴𝑋)[,]𝐴) ↦ (𝐹𝑥)) ∈ 𝐿1)
266265adantr 481 . . . . 5 ((𝜑𝑋𝑇) → (𝑥 ∈ ((𝐴𝑋)[,]𝐴) ↦ (𝐹𝑥)) ∈ 𝐿1)
2673leidd 11679 . . . . . . . 8 (𝜑𝐴𝐴)
2685rpge0d 12915 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑋)
2698, 6subge02d 11705 . . . . . . . . 9 (𝜑 → (0 ≤ 𝑋 ↔ (𝐵𝑋) ≤ 𝐵))
270268, 269mpbid 231 . . . . . . . 8 (𝜑 → (𝐵𝑋) ≤ 𝐵)
271 iccss 13286 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴𝐴 ∧ (𝐵𝑋) ≤ 𝐵)) → (𝐴[,](𝐵𝑋)) ⊆ (𝐴[,]𝐵))
2723, 8, 267, 270, 271syl22anc 837 . . . . . . 7 (𝜑 → (𝐴[,](𝐵𝑋)) ⊆ (𝐴[,]𝐵))
273 iccmbl 24876 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ) → (𝐴[,](𝐵𝑋)) ∈ dom vol)
2743, 14, 273syl2anc 584 . . . . . . 7 (𝜑 → (𝐴[,](𝐵𝑋)) ∈ dom vol)
275272, 274, 227, 213iblss 25115 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
276275adantr 481 . . . . 5 ((𝜑𝑋𝑇) → (𝑥 ∈ (𝐴[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
277251, 252, 262, 263, 266, 276itgspliticc 25147 . . . 4 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥))
278268adantr 481 . . . . . . . . . 10 ((𝜑𝑋𝑇) → 0 ≤ 𝑋)
279269adantr 481 . . . . . . . . . 10 ((𝜑𝑋𝑇) → (0 ≤ 𝑋 ↔ (𝐵𝑋) ≤ 𝐵))
280278, 279mpbid 231 . . . . . . . . 9 ((𝜑𝑋𝑇) → (𝐵𝑋) ≤ 𝐵)
281253, 257, 252, 261, 280eliccd 43637 . . . . . . . 8 ((𝜑𝑋𝑇) → (𝐵𝑋) ∈ (𝐴[,]𝐵))
282227adantlr 713 . . . . . . . 8 (((𝜑𝑋𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
2838leidd 11679 . . . . . . . . . . 11 (𝜑𝐵𝐵)
284283adantr 481 . . . . . . . . . 10 ((𝜑𝑋𝑇) → 𝐵𝐵)
285 iccss 13286 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵𝑋) ∧ 𝐵𝐵)) → ((𝐵𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286253, 257, 261, 284, 285syl22anc 837 . . . . . . . . 9 ((𝜑𝑋𝑇) → ((𝐵𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287 iccmbl 24876 . . . . . . . . . . 11 (((𝐵𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵𝑋)[,]𝐵) ∈ dom vol)
28814, 8, 287syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝐵𝑋)[,]𝐵) ∈ dom vol)
289288adantr 481 . . . . . . . . 9 ((𝜑𝑋𝑇) → ((𝐵𝑋)[,]𝐵) ∈ dom vol)
290213adantr 481 . . . . . . . . 9 ((𝜑𝑋𝑇) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
291286, 289, 282, 290iblss 25115 . . . . . . . 8 ((𝜑𝑋𝑇) → (𝑥 ∈ ((𝐵𝑋)[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
292253, 257, 281, 282, 276, 291itgspliticc 25147 . . . . . . 7 ((𝜑𝑋𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
293292oveq1d 7366 . . . . . 6 ((𝜑𝑋𝑇) → (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = ((∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
29460adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝐹:ℝ⟶ℂ)
2953adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝐴 ∈ ℝ)
29614adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → (𝐵𝑋) ∈ ℝ)
297 simpr 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝑥 ∈ (𝐴[,](𝐵𝑋)))
298 eliccre 43638 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
299295, 296, 297, 298syl3anc 1371 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
300294, 299ffvelcdmd 7032 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → (𝐹𝑥) ∈ ℂ)
301300, 275itgcl 25094 . . . . . . . 8 (𝜑 → ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 ∈ ℂ)
302301, 107, 107addsubassd 11490 . . . . . . 7 (𝜑 → ((∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
303302adantr 481 . . . . . 6 ((𝜑𝑋𝑇) → ((∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
304185oveq2d 7367 . . . . . . . 8 (𝜑 → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + 0))
305301addid1d 11313 . . . . . . . 8 (𝜑 → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥)
306304, 305eqtrd 2776 . . . . . . 7 (𝜑 → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥)
307306adantr 481 . . . . . 6 ((𝜑𝑋𝑇) → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥)
308293, 303, 3073eqtrrd 2781 . . . . 5 ((𝜑𝑋𝑇) → ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
309308oveq2d 7367 . . . 4 ((𝜑𝑋𝑇) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
31093adantr 481 . . . . . . 7 ((𝜑𝑋𝑇) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
311107adantr 481 . . . . . . 7 ((𝜑𝑋𝑇) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
312310, 311eqeltrrd 2839 . . . . . 6 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
313282, 290itgcl 25094 . . . . . 6 ((𝜑𝑋𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
314312, 313, 311addsub12d 11493 . . . . 5 ((𝜑𝑋𝑇) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
315313, 312, 311addsubassd 11490 . . . . 5 ((𝜑𝑋𝑇) → ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
316314, 315eqtr4d 2779 . . . 4 ((𝜑𝑋𝑇) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
317277, 309, 3163eqtrd 2780 . . 3 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
318310oveq2d 7367 . . 3 ((𝜑𝑋𝑇) → ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
319313, 312pncand 11471 . . 3 ((𝜑𝑋𝑇) → ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
320317, 318, 3193eqtrd 2780 . 2 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
321250, 320, 47, 6ltlecasei 11221 1 (𝜑 → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3062  wrex 3071  {crab 3405  cun 3906  wss 3908  ifcif 4484  {cpr 4586   class class class wbr 5103  cmpt 5186  dom cdm 5631  ran crn 5632  cres 5633  cio 6443  wf 6489  cfv 6493   Isom wiso 6494  (class class class)co 7351  m cmap 8723  supcsup 9334  cc 11007  cr 11008  0cc0 11009  1c1 11010   + caddc 11012   · cmul 11014  +∞cpnf 11144  *cxr 11146   < clt 11147  cle 11148  cmin 11343  -cneg 11344   / cdiv 11770  cn 12111  cz 12457  +crp 12869  (,)cioo 13218  (,]cioc 13219  [,]cicc 13221  ...cfz 13378  ..^cfzo 13521  cfl 13649  chash 14184  cnccncf 24185  volcvol 24773  𝐿1cibl 24927  citg 24928   lim climc 25172
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664  ax-inf2 9535  ax-cc 10329  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087  ax-addf 11088  ax-mulf 11089
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-symdif 4200  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-iin 4955  df-disj 5069  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7307  df-ov 7354  df-oprab 7355  df-mpo 7356  df-of 7609  df-ofr 7610  df-om 7795  df-1st 7913  df-2nd 7914  df-supp 8085  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-1o 8404  df-2o 8405  df-oadd 8408  df-omul 8409  df-er 8606  df-map 8725  df-pm 8726  df-ixp 8794  df-en 8842  df-dom 8843  df-sdom 8844  df-fin 8845  df-fsupp 9264  df-fi 9305  df-sup 9336  df-inf 9337  df-oi 9404  df-dju 9795  df-card 9833  df-acn 9836  df-pnf 11149  df-mnf 11150  df-xr 11151  df-ltxr 11152  df-le 11153  df-sub 11345  df-neg 11346  df-div 11771  df-nn 12112  df-2 12174  df-3 12175  df-4 12176  df-5 12177  df-6 12178  df-7 12179  df-8 12180  df-9 12181  df-n0 12372  df-xnn0 12444  df-z 12458  df-dec 12577  df-uz 12722  df-q 12828  df-rp 12870  df-xneg 12987  df-xadd 12988  df-xmul 12989  df-ioo 13222  df-ioc 13223  df-ico 13224  df-icc 13225  df-fz 13379  df-fzo 13522  df-fl 13651  df-mod 13729  df-seq 13861  df-exp 13922  df-hash 14185  df-cj 14938  df-re 14939  df-im 14940  df-sqrt 15074  df-abs 15075  df-limsup 15307  df-clim 15324  df-rlim 15325  df-sum 15525  df-struct 16973  df-sets 16990  df-slot 17008  df-ndx 17020  df-base 17038  df-ress 17067  df-plusg 17100  df-mulr 17101  df-starv 17102  df-sca 17103  df-vsca 17104  df-ip 17105  df-tset 17106  df-ple 17107  df-ds 17109  df-unif 17110  df-hom 17111  df-cco 17112  df-rest 17258  df-topn 17259  df-0g 17277  df-gsum 17278  df-topgen 17279  df-pt 17280  df-prds 17283  df-xrs 17338  df-qtop 17343  df-imas 17344  df-xps 17346  df-mre 17420  df-mrc 17421  df-acs 17423  df-mgm 18451  df-sgrp 18500  df-mnd 18511  df-submnd 18556  df-mulg 18826  df-cntz 19050  df-cmn 19517  df-psmet 20735  df-xmet 20736  df-met 20737  df-bl 20738  df-mopn 20739  df-fbas 20740  df-fg 20741  df-cnfld 20744  df-top 22189  df-topon 22206  df-topsp 22228  df-bases 22242  df-cld 22316  df-ntr 22317  df-cls 22318  df-nei 22395  df-lp 22433  df-perf 22434  df-cn 22524  df-cnp 22525  df-haus 22612  df-cmp 22684  df-tx 22859  df-hmeo 23052  df-fil 23143  df-fm 23235  df-flim 23236  df-flf 23237  df-xms 23619  df-ms 23620  df-tms 23621  df-cncf 24187  df-ovol 24774  df-vol 24775  df-mbf 24929  df-itg1 24930  df-itg2 24931  df-ibl 24932  df-itg 24933  df-0p 24980  df-ditg 25157  df-limc 25176  df-dv 25177
This theorem is referenced by:  fourierdlem108  44350
  Copyright terms: Public domain W3C validator