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 45744
Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 45729 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 7430 . . . . . . . . . . . . . . . 16 ((𝐴𝑋) + 𝑇) = ((𝐴𝑋) + (𝐵𝐴))
3 fourierdlem107.a . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ ℝ)
43recnd 11279 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℂ)
5 fourierdlem107.x . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 ∈ ℝ+)
65rpred 13056 . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ ℝ)
76recnd 11279 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ ℂ)
8 fourierdlem107.b . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℝ)
98recnd 11279 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℂ)
104, 7, 9, 4subadd4b 44807 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴𝑋) + (𝐵𝐴)) = ((𝐴𝐴) + (𝐵𝑋)))
112, 10eqtrid 2777 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝑋) + 𝑇) = ((𝐴𝐴) + (𝐵𝑋)))
124subidd 11596 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐴) = 0)
1312oveq1d 7434 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴𝐴) + (𝐵𝑋)) = (0 + (𝐵𝑋)))
148, 6resubcld 11679 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑋) ∈ ℝ)
1514recnd 11279 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑋) ∈ ℂ)
1615addlidd 11452 . . . . . . . . . . . . . . 15 (𝜑 → (0 + (𝐵𝑋)) = (𝐵𝑋))
1711, 13, 163eqtrd 2769 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝑋) + 𝑇) = (𝐵𝑋))
181oveq2i 7430 . . . . . . . . . . . . . . 15 (𝐴 + 𝑇) = (𝐴 + (𝐵𝐴))
194, 9pncan3d 11611 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 + (𝐵𝐴)) = 𝐵)
2018, 19eqtrid 2777 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 + 𝑇) = 𝐵)
2117, 20oveq12d 7437 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵𝑋)[,]𝐵))
2221eqcomd 2731 . . . . . . . . . . . 12 (𝜑 → ((𝐵𝑋)[,]𝐵) = (((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇)))
2322itgeq1d 45488 . . . . . . . . . . 11 (𝜑 → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹𝑥) d𝑥)
243, 6resubcld 11679 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑋) ∈ ℝ)
25 fourierdlem107.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
26 fveq2 6896 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑝𝑖) = (𝑝𝑗))
27 oveq1 7426 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
2827fveq2d 6900 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
2926, 28breq12d 5162 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝𝑗) < (𝑝‘(𝑗 + 1))))
3029cbvralvw 3224 . . . . . . . . . . . . . . . . 17 (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))
3130a1i 11 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1))))
3231anbi2d 628 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → ((((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))))
3332rabbidv 3426 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
3433mpteq2ia 5252 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴𝑋) ∧ (𝑝𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
3525, 34eqtri 2753 . . . . . . . . . . . 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 13088 . . . . . . . . . . . . . . 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 45691 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
4443simpld 493 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
4544simpld 493 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
468, 3resubcld 11679 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴) ∈ ℝ)
471, 46eqeltrid 2829 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
4844simprd 494 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝑂𝑁))
4924adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐴𝑋) ∈ ℝ)
503adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51 simpr 483 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴𝑋)[,]𝐴))
52 eliccre 45033 . . . . . . . . . . . . . 14 (((𝐴𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
5349, 50, 51, 52syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54 fourierdlem107.fper . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
5553, 54syldan 589 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
56 fveq2 6896 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑆𝑖) = (𝑆𝑗))
5756oveq1d 7434 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝑆𝑖) + 𝑇) = ((𝑆𝑗) + 𝑇))
5857cbvmptv 5262 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑁) ↦ ((𝑆𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆𝑗) + 𝑇))
59 eqid 2725 . . . . . . . . . . . 12 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴𝑋) + 𝑇) ∧ (𝑝𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴𝑋) + 𝑇) ∧ (𝑝𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
60 fourierdlem107.f . . . . . . . . . . . 12 (𝜑𝐹:ℝ⟶ℂ)
6137adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
6238adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃𝑀))
6360adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
6454adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
65 fourierdlem107.fcn . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
6665adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
6724adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴𝑋) ∈ ℝ)
6867rexrd 11301 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴𝑋) ∈ ℝ*)
69 pnfxr 11305 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
7069a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ*)
713adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
7239adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴𝑋) < 𝐴)
733ltpnfd 13141 . . . . . . . . . . . . . . 15 (𝜑𝐴 < +∞)
7473adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
7568, 70, 71, 72, 74eliood 45026 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ((𝐴𝑋)(,)+∞))
76 fourierdlem107.e . . . . . . . . . . . . 13 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
77 fourierdlem107.z . . . . . . . . . . . . 13 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
78 simpr 483 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
79 eqid 2725 . . . . . . . . . . . . 13 ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
80 eqid 2725 . . . . . . . . . . . . 13 (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
81 eqid 2725 . . . . . . . . . . . . 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 45727 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84 fourierdlem107.r . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
8584adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
86 eqid 2725 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) ↦ 𝑅) = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
8736, 1, 61, 62, 63, 64, 66, 85, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 86fourierdlem89 45726 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝑍‘(𝐸‘(𝑆𝑗))) = (𝑄‘(𝐼‘(𝑆𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝑍‘(𝐸‘(𝑆𝑗))))) ∈ ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
88 fourierdlem107.l . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
8988adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
90 eqid 2725 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) ↦ 𝐿) = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
9136, 1, 61, 62, 63, 64, 66, 89, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 90fourierdlem91 45728 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
9224, 3, 35, 45, 47, 48, 55, 58, 59, 60, 83, 87, 91fourierdlem92 45729 . . . . . . . . . . 11 (𝜑 → ∫(((𝐴𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
9323, 92eqtrd 2765 . . . . . . . . . 10 (𝜑 → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
9460adantr 479 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
9514adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → (𝐵𝑋) ∈ ℝ)
968adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97 simpr 483 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵𝑋)[,]𝐵))
98 eliccre 45033 . . . . . . . . . . . . 13 (((𝐵𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
9995, 96, 97, 98syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
10094, 99ffvelcdmd 7094 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
10114rexrd 11301 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝑋) ∈ ℝ*)
10269a1i 11 . . . . . . . . . . . . 13 (𝜑 → +∞ ∈ ℝ*)
1038, 5ltsubrpd 13088 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝑋) < 𝐵)
1048ltpnfd 13141 . . . . . . . . . . . . 13 (𝜑𝐵 < +∞)
105101, 102, 8, 103, 104eliood 45026 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ((𝐵𝑋)(,)+∞))
10636, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105fourierdlem105 45742 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ((𝐵𝑋)[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
107100, 106itgcl 25774 . . . . . . . . . 10 (𝜑 → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
10893, 107eqeltrrd 2826 . . . . . . . . 9 (𝜑 → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
109108subidd 11596 . . . . . . . 8 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = 0)
110109eqcomd 2731 . . . . . . 7 (𝜑 → 0 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
111110adantr 479 . . . . . 6 ((𝜑𝑇 < 𝑋) → 0 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
11224adantr 479 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝐴𝑋) ∈ ℝ)
1133adantr 479 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → 𝐴 ∈ ℝ)
11414adantr 479 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ∈ ℝ)
11536, 37, 38fourierdlem11 45649 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116115simp3d 1141 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
1173, 8, 116ltled 11399 . . . . . . . . . . 11 (𝜑𝐴𝐵)
118117adantr 479 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → 𝐴𝐵)
1193, 8, 6lesub1d 11858 . . . . . . . . . . 11 (𝜑 → (𝐴𝐵 ↔ (𝐴𝑋) ≤ (𝐵𝑋)))
120119adantr 479 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (𝐴𝐵 ↔ (𝐴𝑋) ≤ (𝐵𝑋)))
121118, 120mpbid 231 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝐴𝑋) ≤ (𝐵𝑋))
1228adantr 479 . . . . . . . . . . 11 ((𝜑𝑇 < 𝑋) → 𝐵 ∈ ℝ)
1236adantr 479 . . . . . . . . . . 11 ((𝜑𝑇 < 𝑋) → 𝑋 ∈ ℝ)
124 simpr 483 . . . . . . . . . . . 12 ((𝜑𝑇 < 𝑋) → 𝑇 < 𝑋)
1251, 124eqbrtrrid 5185 . . . . . . . . . . 11 ((𝜑𝑇 < 𝑋) → (𝐵𝐴) < 𝑋)
126122, 113, 123, 125ltsub23d 11856 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) < 𝐴)
127114, 113, 126ltled 11399 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ≤ 𝐴)
128112, 113, 114, 121, 127eliccd 45032 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ∈ ((𝐴𝑋)[,]𝐴))
12960adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130129, 53ffvelcdmd 7094 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
131130adantlr 713 . . . . . . . 8 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
13224rexrd 11301 . . . . . . . . . . 11 (𝜑 → (𝐴𝑋) ∈ ℝ*)
1333, 8, 6, 116ltsub1dd 11863 . . . . . . . . . . 11 (𝜑 → (𝐴𝑋) < (𝐵𝑋))
13414ltpnfd 13141 . . . . . . . . . . 11 (𝜑 → (𝐵𝑋) < +∞)
135132, 102, 14, 133, 134eliood 45026 . . . . . . . . . 10 (𝜑 → (𝐵𝑋) ∈ ((𝐴𝑋)(,)+∞))
13636, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135fourierdlem105 45742 . . . . . . . . 9 (𝜑 → (𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
137136adantr 479 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
13837adantr 479 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝑀 ∈ ℕ)
13938adantr 479 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝑄 ∈ (𝑃𝑀))
14060adantr 479 . . . . . . . . 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 479 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (𝐵𝑋) ∈ ℝ*)
14669a1i 11 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → +∞ ∈ ℝ*)
147113ltpnfd 13141 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → 𝐴 < +∞)
148145, 146, 113, 126, 147eliood 45026 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝐴 ∈ ((𝐵𝑋)(,)+∞))
14936, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148fourierdlem105 45742 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (𝑥 ∈ ((𝐵𝑋)[,]𝐴) ↦ (𝐹𝑥)) ∈ 𝐿1)
150112, 113, 128, 131, 137, 149itgspliticc 25827 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
151150oveq1d 7434 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
15260adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝐹:ℝ⟶ℂ)
15324adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐴𝑋) ∈ ℝ)
15414adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐵𝑋) ∈ ℝ)
155 simpr 483 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋)))
156 eliccre 45033 . . . . . . . . . . 11 (((𝐴𝑋) ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
157153, 154, 155, 156syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
158152, 157ffvelcdmd 7094 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐹𝑥) ∈ ℂ)
159158, 136itgcl 25774 . . . . . . . 8 (𝜑 → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 ∈ ℂ)
160159adantr 479 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 ∈ ℂ)
16160adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
16214adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → (𝐵𝑋) ∈ ℝ)
1633adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
164 simpr 483 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐵𝑋)[,]𝐴))
165 eliccre 45033 . . . . . . . . . . 11 (((𝐵𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166162, 163, 164, 165syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167161, 166ffvelcdmd 7094 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
168167adantlr 713 . . . . . . . 8 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐴)) → (𝐹𝑥) ∈ ℂ)
169168, 149itgcl 25774 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
170108adantr 479 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
171160, 169, 170addsubassd 11628 . . . . . 6 ((𝜑𝑇 < 𝑋) → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
172111, 151, 1713eqtrd 2769 . . . . 5 ((𝜑𝑇 < 𝑋) → 0 = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
173172oveq2d 7435 . . . 4 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − 0) = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))))
174160subid1d 11597 . . . 4 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − 0) = ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥)
175159subidd 11596 . . . . . . 7 (𝜑 → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) = 0)
176175oveq1d 7434 . . . . . 6 (𝜑 → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
177176adantr 479 . . . . 5 ((𝜑𝑇 < 𝑋) → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)))
178169, 170subcld 11608 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) ∈ ℂ)
179160, 160, 178subsub4d 11639 . . . . 5 ((𝜑𝑇 < 𝑋) → ((∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥) − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))))
180 df-neg 11484 . . . . . 6 -(∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
181169, 170negsubdi2d 11624 . . . . . 6 ((𝜑𝑇 < 𝑋) → -(∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
182180, 181eqtr3id 2779 . . . . 5 ((𝜑𝑇 < 𝑋) → (0 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
183177, 179, 1823eqtr3d 2773 . . . 4 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 − (∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
184173, 174, 1833eqtr3d 2773 . . 3 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
185107subidd 11596 . . . . . . . 8 (𝜑 → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = 0)
186185eqcomd 2731 . . . . . . 7 (𝜑 → 0 = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
187186oveq2d 7435 . . . . . 6 (𝜑 → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + 0) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
188187adantr 479 . . . . 5 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + 0) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
189169addridd 11451 . . . . 5 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + 0) = ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
190114, 122, 113, 127, 118eliccd 45032 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → 𝐴 ∈ ((𝐵𝑋)[,]𝐵))
191100adantlr 713 . . . . . . . . 9 (((𝜑𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵𝑋)[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
1923, 8iccssred 13451 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
19360, 192feqresmpt 6967 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)))
19460, 192fssresd 6764 . . . . . . . . . . . 12 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195 ioossicc 13450 . . . . . . . . . . . . . . 15 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
1963rexrd 11301 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ*)
197196adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
1988rexrd 11301 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
199198adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
20036, 37, 38fourierdlem15 45653 . . . . . . . . . . . . . . . . 17 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201200adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202 simpr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203197, 199, 201, 202fourierdlem8 45646 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204195, 203sstrid 3988 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205204resabs1d 6013 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
206205, 65eqeltrd 2825 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207205eqcomd 2731 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
208207oveq1d 7434 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
20984, 208eleqtrd 2827 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
210207oveq1d 7434 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
21188, 210eleqtrd 2827 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
21236, 37, 38, 194, 206, 209, 211fourierdlem69 45706 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿1)
213193, 212eqeltrrd 2826 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
214213adantr 479 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
215114, 122, 190, 191, 149, 214itgspliticc 25827 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
216215oveq2d 7435 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
217216oveq2d 7435 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))))
218107adantr 479 . . . . . . 7 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
219215, 218eqeltrrd 2826 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) ∈ ℂ)
220169, 218, 219addsub12d 11631 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))))
22160adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ)
2223adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
2238adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
224 simpr 483 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
225 eliccre 45033 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226222, 223, 224, 225syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227221, 226ffvelcdmd 7094 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
228227, 213itgcl 25774 . . . . . . . . . . 11 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
229228adantr 479 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
230169, 169, 229subsub4d 11639 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
231230eqcomd 2731 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
232231oveq2d 7435 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
233169subidd 11596 . . . . . . . . . 10 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = 0)
234233oveq1d 7434 . . . . . . . . 9 ((𝜑𝑇 < 𝑋) → ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
235 df-neg 11484 . . . . . . . . 9 -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
236234, 235eqtr4di 2783 . . . . . . . 8 ((𝜑𝑇 < 𝑋) → ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
237236oveq2d 7435 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + ((∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
238218, 229negsubd 11614 . . . . . . 7 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
239232, 237, 2383eqtrd 2769 . . . . . 6 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
240217, 220, 2393eqtrd 2769 . . . . 5 ((𝜑𝑇 < 𝑋) → (∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
241188, 189, 2403eqtr3d 2773 . . . 4 ((𝜑𝑇 < 𝑋) → ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥 = (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
242241oveq2d 7435 . . 3 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)))
243108, 107, 228subsubd 11636 . . . . 5 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ((∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
24493oveq2d 7435 . . . . . . 7 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
245244, 109eqtrd 2765 . . . . . 6 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = 0)
246245oveq1d 7434 . . . . 5 (𝜑 → ((∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥))
247228addlidd 11452 . . . . 5 (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
248243, 246, 2473eqtrd 2769 . . . 4 (𝜑 → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
249248adantr 479 . . 3 ((𝜑𝑇 < 𝑋) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
250184, 242, 2493eqtrd 2769 . 2 ((𝜑𝑇 < 𝑋) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
25124adantr 479 . . . . 5 ((𝜑𝑋𝑇) → (𝐴𝑋) ∈ ℝ)
25214adantr 479 . . . . 5 ((𝜑𝑋𝑇) → (𝐵𝑋) ∈ ℝ)
2533adantr 479 . . . . . 6 ((𝜑𝑋𝑇) → 𝐴 ∈ ℝ)
25424, 3, 39ltled 11399 . . . . . . 7 (𝜑 → (𝐴𝑋) ≤ 𝐴)
255254adantr 479 . . . . . 6 ((𝜑𝑋𝑇) → (𝐴𝑋) ≤ 𝐴)
2566adantr 479 . . . . . . 7 ((𝜑𝑋𝑇) → 𝑋 ∈ ℝ)
2578adantr 479 . . . . . . 7 ((𝜑𝑋𝑇) → 𝐵 ∈ ℝ)
258 id 22 . . . . . . . . 9 (𝑋𝑇𝑋𝑇)
259258, 1breqtrdi 5190 . . . . . . . 8 (𝑋𝑇𝑋 ≤ (𝐵𝐴))
260259adantl 480 . . . . . . 7 ((𝜑𝑋𝑇) → 𝑋 ≤ (𝐵𝐴))
261256, 257, 253, 260lesubd 11855 . . . . . 6 ((𝜑𝑋𝑇) → 𝐴 ≤ (𝐵𝑋))
262251, 252, 253, 255, 261eliccd 45032 . . . . 5 ((𝜑𝑋𝑇) → 𝐴 ∈ ((𝐴𝑋)[,](𝐵𝑋)))
263158adantlr 713 . . . . 5 (((𝜑𝑋𝑇) ∧ 𝑥 ∈ ((𝐴𝑋)[,](𝐵𝑋))) → (𝐹𝑥) ∈ ℂ)
264132, 102, 3, 39, 73eliood 45026 . . . . . . 7 (𝜑𝐴 ∈ ((𝐴𝑋)(,)+∞))
26536, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264fourierdlem105 45742 . . . . . 6 (𝜑 → (𝑥 ∈ ((𝐴𝑋)[,]𝐴) ↦ (𝐹𝑥)) ∈ 𝐿1)
266265adantr 479 . . . . 5 ((𝜑𝑋𝑇) → (𝑥 ∈ ((𝐴𝑋)[,]𝐴) ↦ (𝐹𝑥)) ∈ 𝐿1)
2673leidd 11817 . . . . . . . 8 (𝜑𝐴𝐴)
2685rpge0d 13060 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑋)
2698, 6subge02d 11843 . . . . . . . . 9 (𝜑 → (0 ≤ 𝑋 ↔ (𝐵𝑋) ≤ 𝐵))
270268, 269mpbid 231 . . . . . . . 8 (𝜑 → (𝐵𝑋) ≤ 𝐵)
271 iccss 13432 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴𝐴 ∧ (𝐵𝑋) ≤ 𝐵)) → (𝐴[,](𝐵𝑋)) ⊆ (𝐴[,]𝐵))
2723, 8, 267, 270, 271syl22anc 837 . . . . . . 7 (𝜑 → (𝐴[,](𝐵𝑋)) ⊆ (𝐴[,]𝐵))
273 iccmbl 25556 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ) → (𝐴[,](𝐵𝑋)) ∈ dom vol)
2743, 14, 273syl2anc 582 . . . . . . 7 (𝜑 → (𝐴[,](𝐵𝑋)) ∈ dom vol)
275272, 274, 227, 213iblss 25795 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐴[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
276275adantr 479 . . . . 5 ((𝜑𝑋𝑇) → (𝑥 ∈ (𝐴[,](𝐵𝑋)) ↦ (𝐹𝑥)) ∈ 𝐿1)
277251, 252, 262, 263, 266, 276itgspliticc 25827 . . . 4 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥))
278268adantr 479 . . . . . . . . . 10 ((𝜑𝑋𝑇) → 0 ≤ 𝑋)
279269adantr 479 . . . . . . . . . 10 ((𝜑𝑋𝑇) → (0 ≤ 𝑋 ↔ (𝐵𝑋) ≤ 𝐵))
280278, 279mpbid 231 . . . . . . . . 9 ((𝜑𝑋𝑇) → (𝐵𝑋) ≤ 𝐵)
281253, 257, 252, 261, 280eliccd 45032 . . . . . . . 8 ((𝜑𝑋𝑇) → (𝐵𝑋) ∈ (𝐴[,]𝐵))
282227adantlr 713 . . . . . . . 8 (((𝜑𝑋𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝑥) ∈ ℂ)
2838leidd 11817 . . . . . . . . . . 11 (𝜑𝐵𝐵)
284283adantr 479 . . . . . . . . . 10 ((𝜑𝑋𝑇) → 𝐵𝐵)
285 iccss 13432 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵𝑋) ∧ 𝐵𝐵)) → ((𝐵𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286253, 257, 261, 284, 285syl22anc 837 . . . . . . . . 9 ((𝜑𝑋𝑇) → ((𝐵𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287 iccmbl 25556 . . . . . . . . . . 11 (((𝐵𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵𝑋)[,]𝐵) ∈ dom vol)
28814, 8, 287syl2anc 582 . . . . . . . . . 10 (𝜑 → ((𝐵𝑋)[,]𝐵) ∈ dom vol)
289288adantr 479 . . . . . . . . 9 ((𝜑𝑋𝑇) → ((𝐵𝑋)[,]𝐵) ∈ dom vol)
290213adantr 479 . . . . . . . . 9 ((𝜑𝑋𝑇) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
291286, 289, 282, 290iblss 25795 . . . . . . . 8 ((𝜑𝑋𝑇) → (𝑥 ∈ ((𝐵𝑋)[,]𝐵) ↦ (𝐹𝑥)) ∈ 𝐿1)
292253, 257, 281, 282, 276, 291itgspliticc 25827 . . . . . . 7 ((𝜑𝑋𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
293292oveq1d 7434 . . . . . 6 ((𝜑𝑋𝑇) → (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = ((∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
29460adantr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝐹:ℝ⟶ℂ)
2953adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝐴 ∈ ℝ)
29614adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → (𝐵𝑋) ∈ ℝ)
297 simpr 483 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝑥 ∈ (𝐴[,](𝐵𝑋)))
298 eliccre 45033 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐵𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
299295, 296, 297, 298syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → 𝑥 ∈ ℝ)
300294, 299ffvelcdmd 7094 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐴[,](𝐵𝑋))) → (𝐹𝑥) ∈ ℂ)
301300, 275itgcl 25774 . . . . . . . 8 (𝜑 → ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 ∈ ℂ)
302301, 107, 107addsubassd 11628 . . . . . . 7 (𝜑 → ((∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
303302adantr 479 . . . . . 6 ((𝜑𝑋𝑇) → ((∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
304185oveq2d 7435 . . . . . . . 8 (𝜑 → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + 0))
305301addridd 11451 . . . . . . . 8 (𝜑 → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥)
306304, 305eqtrd 2765 . . . . . . 7 (𝜑 → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥)
307306adantr 479 . . . . . 6 ((𝜑𝑋𝑇) → (∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 + (∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥)
308293, 303, 3073eqtrrd 2770 . . . . 5 ((𝜑𝑋𝑇) → ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
309308oveq2d 7435 . . . 4 ((𝜑𝑋𝑇) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + ∫(𝐴[,](𝐵𝑋))(𝐹𝑥) d𝑥) = (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
31093adantr 479 . . . . . . 7 ((𝜑𝑋𝑇) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 = ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥)
311107adantr 479 . . . . . . 7 ((𝜑𝑋𝑇) → ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
312310, 311eqeltrrd 2826 . . . . . 6 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 ∈ ℂ)
313282, 290itgcl 25774 . . . . . 6 ((𝜑𝑋𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 ∈ ℂ)
314312, 313, 311addsub12d 11631 . . . . 5 ((𝜑𝑋𝑇) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
315313, 312, 311addsubassd 11628 . . . . 5 ((𝜑𝑋𝑇) → ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)))
316314, 315eqtr4d 2768 . . . 4 ((𝜑𝑋𝑇) → (∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥)) = ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
317277, 309, 3163eqtrd 2769 . . 3 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥))
318310oveq2d 7435 . . 3 ((𝜑𝑋𝑇) → ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐵𝑋)[,]𝐵)(𝐹𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥))
319313, 312pncand 11609 . . 3 ((𝜑𝑋𝑇) → ((∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 + ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) − ∫((𝐴𝑋)[,]𝐴)(𝐹𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
320317, 318, 3193eqtrd 2769 . 2 ((𝜑𝑋𝑇) → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
321250, 320, 47, 6ltlecasei 11359 1 (𝜑 → ∫((𝐴𝑋)[,](𝐵𝑋))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wral 3050  wrex 3059  {crab 3418  cun 3942  wss 3944  ifcif 4530  {cpr 4632   class class class wbr 5149  cmpt 5232  dom cdm 5678  ran crn 5679  cres 5680  cio 6499  wf 6545  cfv 6549   Isom wiso 6550  (class class class)co 7419  m cmap 8845  supcsup 9470  cc 11143  cr 11144  0cc0 11145  1c1 11146   + caddc 11148   · cmul 11150  +∞cpnf 11282  *cxr 11284   < clt 11285  cle 11286  cmin 11481  -cneg 11482   / cdiv 11908  cn 12250  cz 12596  +crp 13014  (,)cioo 13364  (,]cioc 13365  [,]cicc 13367  ...cfz 13524  ..^cfzo 13667  cfl 13796  chash 14333  cnccncf 24857  volcvol 25453  𝐿1cibl 25607  citg 25608   lim climc 25852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9671  ax-cc 10465  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223  ax-addf 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-symdif 4241  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-ofr 7686  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-omul 8492  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9393  df-fi 9441  df-sup 9472  df-inf 9473  df-oi 9540  df-dju 9931  df-card 9969  df-acn 9972  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-xnn0 12583  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ioc 13369  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13798  df-mod 13876  df-seq 14008  df-exp 14068  df-hash 14334  df-cj 15090  df-re 15091  df-im 15092  df-sqrt 15226  df-abs 15227  df-limsup 15459  df-clim 15476  df-rlim 15477  df-sum 15677  df-struct 17135  df-sets 17152  df-slot 17170  df-ndx 17182  df-base 17200  df-ress 17229  df-plusg 17265  df-mulr 17266  df-starv 17267  df-sca 17268  df-vsca 17269  df-ip 17270  df-tset 17271  df-ple 17272  df-ds 17274  df-unif 17275  df-hom 17276  df-cco 17277  df-rest 17423  df-topn 17424  df-0g 17442  df-gsum 17443  df-topgen 17444  df-pt 17445  df-prds 17448  df-xrs 17503  df-qtop 17508  df-imas 17509  df-xps 17511  df-mre 17585  df-mrc 17586  df-acs 17588  df-mgm 18619  df-sgrp 18698  df-mnd 18714  df-submnd 18760  df-mulg 19048  df-cntz 19297  df-cmn 19766  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-fbas 21310  df-fg 21311  df-cnfld 21314  df-top 22857  df-topon 22874  df-topsp 22896  df-bases 22910  df-cld 22984  df-ntr 22985  df-cls 22986  df-nei 23063  df-lp 23101  df-perf 23102  df-cn 23192  df-cnp 23193  df-haus 23280  df-cmp 23352  df-tx 23527  df-hmeo 23720  df-fil 23811  df-fm 23903  df-flim 23904  df-flf 23905  df-xms 24287  df-ms 24288  df-tms 24289  df-cncf 24859  df-ovol 25454  df-vol 25455  df-mbf 25609  df-itg1 25610  df-itg2 25611  df-ibl 25612  df-itg 25613  df-0p 25660  df-ditg 25837  df-limc 25856  df-dv 25857
This theorem is referenced by:  fourierdlem108  45745
  Copyright terms: Public domain W3C validator