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 45524
Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 45509 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 7425 . . . . . . . . . . . . . . . 16 ((𝐴 βˆ’ 𝑋) + 𝑇) = ((𝐴 βˆ’ 𝑋) + (𝐡 βˆ’ 𝐴))
3 fourierdlem107.a . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐴 ∈ ℝ)
43recnd 11264 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐴 ∈ β„‚)
5 fourierdlem107.x . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 ∈ ℝ+)
65rpred 13040 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑋 ∈ ℝ)
76recnd 11264 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑋 ∈ β„‚)
8 fourierdlem107.b . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐡 ∈ ℝ)
98recnd 11264 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐡 ∈ β„‚)
104, 7, 9, 4subadd4b 44587 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝐴 βˆ’ 𝑋) + (𝐡 βˆ’ 𝐴)) = ((𝐴 βˆ’ 𝐴) + (𝐡 βˆ’ 𝑋)))
112, 10eqtrid 2779 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝐴 βˆ’ 𝑋) + 𝑇) = ((𝐴 βˆ’ 𝐴) + (𝐡 βˆ’ 𝑋)))
124subidd 11581 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐴 βˆ’ 𝐴) = 0)
1312oveq1d 7429 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝐴 βˆ’ 𝐴) + (𝐡 βˆ’ 𝑋)) = (0 + (𝐡 βˆ’ 𝑋)))
148, 6resubcld 11664 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
1514recnd 11264 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) ∈ β„‚)
1615addlidd 11437 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (0 + (𝐡 βˆ’ 𝑋)) = (𝐡 βˆ’ 𝑋))
1711, 13, 163eqtrd 2771 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐴 βˆ’ 𝑋) + 𝑇) = (𝐡 βˆ’ 𝑋))
181oveq2i 7425 . . . . . . . . . . . . . . 15 (𝐴 + 𝑇) = (𝐴 + (𝐡 βˆ’ 𝐴))
194, 9pncan3d 11596 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴 + (𝐡 βˆ’ 𝐴)) = 𝐡)
2018, 19eqtrid 2779 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐴 + 𝑇) = 𝐡)
2117, 20oveq12d 7432 . . . . . . . . . . . . 13 (πœ‘ β†’ (((𝐴 βˆ’ 𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐡 βˆ’ 𝑋)[,]𝐡))
2221eqcomd 2733 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐡 βˆ’ 𝑋)[,]𝐡) = (((𝐴 βˆ’ 𝑋) + 𝑇)[,](𝐴 + 𝑇)))
2322itgeq1d 45268 . . . . . . . . . . 11 (πœ‘ β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ = ∫(((𝐴 βˆ’ 𝑋) + 𝑇)[,](𝐴 + 𝑇))(πΉβ€˜π‘₯) dπ‘₯)
243, 6resubcld 11664 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ)
25 fourierdlem107.o . . . . . . . . . . . . 13 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
26 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 β†’ (π‘β€˜π‘–) = (π‘β€˜π‘—))
27 oveq1 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 β†’ (𝑖 + 1) = (𝑗 + 1))
2827fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 β†’ (π‘β€˜(𝑖 + 1)) = (π‘β€˜(𝑗 + 1)))
2926, 28breq12d 5155 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 β†’ ((π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)) ↔ (π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1))))
3029cbvralvw 3229 . . . . . . . . . . . . . . . . 17 (βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)) ↔ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1)))
3130a1i 11 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„• β†’ (βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)) ↔ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1))))
3231anbi2d 628 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ ((((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1))) ↔ (((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1)))))
3332rabbidv 3435 . . . . . . . . . . . . . 14 (π‘š ∈ β„• β†’ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1)))})
3433mpteq2ia 5245 . . . . . . . . . . . . 13 (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))}) = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = (𝐴 βˆ’ 𝑋) ∧ (π‘β€˜π‘š) = 𝐴) ∧ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1)))})
3525, 34eqtri 2755 . . . . . . . . . . . 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 13072 . . . . . . . . . . . . . . 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 45471 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
4443simpld 494 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)))
4544simpld 494 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„•)
468, 3resubcld 11664 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
471, 46eqeltrid 2832 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ ℝ)
4844simprd 495 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 ∈ (π‘‚β€˜π‘))
4924adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ)
503adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ 𝐴 ∈ ℝ)
51 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴))
52 eliccre 44813 . . . . . . . . . . . . . 14 (((𝐴 βˆ’ 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ π‘₯ ∈ ℝ)
5349, 50, 51, 52syl3anc 1369 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ π‘₯ ∈ ℝ)
54 fourierdlem107.fper . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
5553, 54syldan 590 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
56 fveq2 6891 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 β†’ (π‘†β€˜π‘–) = (π‘†β€˜π‘—))
5756oveq1d 7429 . . . . . . . . . . . . 13 (𝑖 = 𝑗 β†’ ((π‘†β€˜π‘–) + 𝑇) = ((π‘†β€˜π‘—) + 𝑇))
5857cbvmptv 5255 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑁) ↦ ((π‘†β€˜π‘–) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((π‘†β€˜π‘—) + 𝑇))
59 eqid 2727 . . . . . . . . . . . 12 (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = ((𝐴 βˆ’ 𝑋) + 𝑇) ∧ (π‘β€˜π‘š) = (𝐴 + 𝑇)) ∧ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1)))}) = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = ((𝐴 βˆ’ 𝑋) + 𝑇) ∧ (π‘β€˜π‘š) = (𝐴 + 𝑇)) ∧ βˆ€π‘— ∈ (0..^π‘š)(π‘β€˜π‘—) < (π‘β€˜(𝑗 + 1)))})
60 fourierdlem107.f . . . . . . . . . . . 12 (πœ‘ β†’ 𝐹:β„βŸΆβ„‚)
6137adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝑀 ∈ β„•)
6238adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝑄 ∈ (π‘ƒβ€˜π‘€))
6360adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝐹:β„βŸΆβ„‚)
6454adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
65 fourierdlem107.fcn . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
6665adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
6724adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ)
6867rexrd 11286 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ*)
69 pnfxr 11290 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
7069a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ +∞ ∈ ℝ*)
713adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝐴 ∈ ℝ)
7239adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ (𝐴 βˆ’ 𝑋) < 𝐴)
733ltpnfd 13125 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 < +∞)
7473adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝐴 < +∞)
7568, 70, 71, 72, 74eliood 44806 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝐴 ∈ ((𝐴 βˆ’ 𝑋)(,)+∞))
76 fourierdlem107.e . . . . . . . . . . . . 13 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)))
77 fourierdlem107.z . . . . . . . . . . . . 13 𝑍 = (𝑦 ∈ (𝐴(,]𝐡) ↦ if(𝑦 = 𝐡, 𝐴, 𝑦))
78 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ 𝑗 ∈ (0..^𝑁))
79 eqid 2727 . . . . . . . . . . . . 13 ((π‘†β€˜(𝑗 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝑗 + 1)))) = ((π‘†β€˜(𝑗 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝑗 + 1))))
80 eqid 2727 . . . . . . . . . . . . 13 (𝐹 β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))(,)(πΈβ€˜(π‘†β€˜(𝑗 + 1))))) = (𝐹 β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))(,)(πΈβ€˜(π‘†β€˜(𝑗 + 1)))))
81 eqid 2727 . . . . . . . . . . . . 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 45507 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ (𝐹 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) ∈ (((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))–cnβ†’β„‚))
84 fourierdlem107.r . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
8584adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
86 eqid 2727 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) ↦ 𝑅) = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
8736, 1, 61, 62, 63, 64, 66, 85, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 86fourierdlem89 45506 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ if((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—))) = (π‘„β€˜(πΌβ€˜(π‘†β€˜π‘—))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)β€˜(πΌβ€˜(π‘†β€˜π‘—))), (πΉβ€˜(π‘β€˜(πΈβ€˜(π‘†β€˜π‘—))))) ∈ ((𝐹 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜π‘—)))
88 fourierdlem107.l . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
8988adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
90 eqid 2727 . . . . . . . . . . . . 13 (𝑖 ∈ (0..^𝑀) ↦ 𝐿) = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
9136, 1, 61, 62, 63, 64, 66, 89, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 90fourierdlem91 45508 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ if((πΈβ€˜(π‘†β€˜(𝑗 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π‘—)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)β€˜(πΌβ€˜(π‘†β€˜π‘—))), (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝑗 + 1))))) ∈ ((𝐹 β†Ύ ((π‘†β€˜π‘—)(,)(π‘†β€˜(𝑗 + 1)))) limβ„‚ (π‘†β€˜(𝑗 + 1))))
9224, 3, 35, 45, 47, 48, 55, 58, 59, 60, 83, 87, 91fourierdlem92 45509 . . . . . . . . . . 11 (πœ‘ β†’ ∫(((𝐴 βˆ’ 𝑋) + 𝑇)[,](𝐴 + 𝑇))(πΉβ€˜π‘₯) dπ‘₯ = ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)
9323, 92eqtrd 2767 . . . . . . . . . 10 (πœ‘ β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ = ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)
9460adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ 𝐹:β„βŸΆβ„‚)
9514adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
968adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ 𝐡 ∈ ℝ)
97 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡))
98 eliccre 44813 . . . . . . . . . . . . 13 (((𝐡 βˆ’ 𝑋) ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ π‘₯ ∈ ℝ)
9995, 96, 97, 98syl3anc 1369 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ π‘₯ ∈ ℝ)
10094, 99ffvelcdmd 7089 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
10114rexrd 11286 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ*)
10269a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ +∞ ∈ ℝ*)
1038, 5ltsubrpd 13072 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) < 𝐡)
1048ltpnfd 13125 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 < +∞)
105101, 102, 8, 103, 104eliood 44806 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ((𝐡 βˆ’ 𝑋)(,)+∞))
10636, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105fourierdlem105 45522 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
107100, 106itgcl 25700 . . . . . . . . . 10 (πœ‘ β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
10893, 107eqeltrrd 2829 . . . . . . . . 9 (πœ‘ β†’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
109108subidd 11581 . . . . . . . 8 (πœ‘ β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = 0)
110109eqcomd 2733 . . . . . . 7 (πœ‘ β†’ 0 = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
111110adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 0 = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
11224adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ)
1133adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐴 ∈ ℝ)
11414adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
11536, 37, 38fourierdlem11 45429 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡))
116115simp3d 1142 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 < 𝐡)
1173, 8, 116ltled 11384 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ≀ 𝐡)
118117adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐴 ≀ 𝐡)
1193, 8, 6lesub1d 11843 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ≀ 𝐡 ↔ (𝐴 βˆ’ 𝑋) ≀ (𝐡 βˆ’ 𝑋)))
120119adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐴 ≀ 𝐡 ↔ (𝐴 βˆ’ 𝑋) ≀ (𝐡 βˆ’ 𝑋)))
121118, 120mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐴 βˆ’ 𝑋) ≀ (𝐡 βˆ’ 𝑋))
1228adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐡 ∈ ℝ)
1236adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝑋 ∈ ℝ)
124 simpr 484 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝑇 < 𝑋)
1251, 124eqbrtrrid 5178 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐡 βˆ’ 𝐴) < 𝑋)
126122, 113, 123, 125ltsub23d 11841 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐡 βˆ’ 𝑋) < 𝐴)
127114, 113, 126ltled 11384 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐡 βˆ’ 𝑋) ≀ 𝐴)
128112, 113, 114, 121, 127eliccd 44812 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐡 βˆ’ 𝑋) ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴))
12960adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ 𝐹:β„βŸΆβ„‚)
130129, 53ffvelcdmd 7089 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
131130adantlr 714 . . . . . . . 8 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
13224rexrd 11286 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ*)
1333, 8, 6, 116ltsub1dd 11848 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 βˆ’ 𝑋) < (𝐡 βˆ’ 𝑋))
13414ltpnfd 13125 . . . . . . . . . . 11 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) < +∞)
135132, 102, 14, 133, 134eliood 44806 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) ∈ ((𝐴 βˆ’ 𝑋)(,)+∞))
13636, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135fourierdlem105 45522 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋)) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
137136adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋)) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
13837adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝑀 ∈ β„•)
13938adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝑄 ∈ (π‘ƒβ€˜π‘€))
14060adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐹:β„βŸΆβ„‚)
14154adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
14265adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
14384adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
14488adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
145101adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ*)
14669a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ +∞ ∈ ℝ*)
147113ltpnfd 13125 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐴 < +∞)
148145, 146, 113, 126, 147eliood 44806 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐴 ∈ ((𝐡 βˆ’ 𝑋)(,)+∞))
14936, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148fourierdlem105 45522 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
150112, 113, 128, 131, 137, 149itgspliticc 25753 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ = (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
151150oveq1d 7429 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = ((∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
15260adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ 𝐹:β„βŸΆβ„‚)
15324adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ)
15414adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
155 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋)))
156 eliccre 44813 . . . . . . . . . . 11 (((𝐴 βˆ’ 𝑋) ∈ ℝ ∧ (𝐡 βˆ’ 𝑋) ∈ ℝ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ π‘₯ ∈ ℝ)
157153, 154, 155, 156syl3anc 1369 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ π‘₯ ∈ ℝ)
158152, 157ffvelcdmd 7089 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
159158, 136itgcl 25700 . . . . . . . 8 (πœ‘ β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
160159adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
16160adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ 𝐹:β„βŸΆβ„‚)
16214adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
1633adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ 𝐴 ∈ ℝ)
164 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴))
165 eliccre 44813 . . . . . . . . . . 11 (((𝐡 βˆ’ 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ π‘₯ ∈ ℝ)
166162, 163, 164, 165syl3anc 1369 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ π‘₯ ∈ ℝ)
167161, 166ffvelcdmd 7089 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
168167adantlr 714 . . . . . . . 8 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐴)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
169168, 149itgcl 25700 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
170108adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
171160, 169, 170addsubassd 11613 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ((∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)))
172111, 151, 1713eqtrd 2771 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 0 = (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)))
173172oveq2d 7430 . . . 4 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ 0) = (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))))
174160subid1d 11582 . . . 4 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ 0) = ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯)
175159subidd 11581 . . . . . . 7 (πœ‘ β†’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯) = 0)
176175oveq1d 7429 . . . . . 6 (πœ‘ β†’ ((∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯) βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)) = (0 βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)))
177176adantr 480 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ((∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯) βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)) = (0 βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)))
178169, 170subcld 11593 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) ∈ β„‚)
179160, 160, 178subsub4d 11624 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ((∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯) βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)) = (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))))
180 df-neg 11469 . . . . . 6 -(∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = (0 βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
181169, 170negsubdi2d 11609 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ -(∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
182180, 181eqtr3id 2781 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (0 βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)) = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
183177, 179, 1823eqtr3d 2775 . . . 4 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))) = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
184173, 174, 1833eqtr3d 2775 . . 3 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
185107subidd 11581 . . . . . . . 8 (πœ‘ β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = 0)
186185eqcomd 2733 . . . . . . 7 (πœ‘ β†’ 0 = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
187186oveq2d 7430 . . . . . 6 (πœ‘ β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + 0) = (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
188187adantr 480 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + 0) = (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
189169addridd 11436 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + 0) = ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)
190114, 122, 113, 127, 118eliccd 44812 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ 𝐴 ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡))
191100adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑇 < 𝑋) ∧ π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
1923, 8iccssred 13435 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
19360, 192feqresmpt 6962 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (𝐴[,]𝐡)) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘₯)))
19460, 192fssresd 6758 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 β†Ύ (𝐴[,]𝐡)):(𝐴[,]𝐡)βŸΆβ„‚)
195 ioossicc 13434 . . . . . . . . . . . . . . 15 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1)))
1963rexrd 11286 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐴 ∈ ℝ*)
197196adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐴 ∈ ℝ*)
1988rexrd 11286 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐡 ∈ ℝ*)
199198adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐡 ∈ ℝ*)
20036, 37, 38fourierdlem15 45433 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑄:(0...𝑀)⟢(𝐴[,]𝐡))
201200adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑄:(0...𝑀)⟢(𝐴[,]𝐡))
202 simpr 484 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑖 ∈ (0..^𝑀))
203197, 199, 201, 202fourierdlem8 45426 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1))) βŠ† (𝐴[,]𝐡))
204195, 203sstrid 3989 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† (𝐴[,]𝐡))
205204resabs1d 6010 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
206205, 65eqeltrd 2828 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
207205eqcomd 2733 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = ((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
208207oveq1d 7429 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)) = (((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
20984, 208eleqtrd 2830 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ (((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜π‘–)))
210207oveq1d 7429 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))) = (((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
21188, 210eleqtrd 2830 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ (((𝐹 β†Ύ (𝐴[,]𝐡)) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
21236, 37, 38, 194, 206, 209, 211fourierdlem69 45486 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (𝐴[,]𝐡)) ∈ 𝐿1)
213193, 212eqeltrrd 2829 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
214213adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
215114, 122, 190, 191, 149, 214itgspliticc 25753 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ = (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
216215oveq2d 7430 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
217216oveq2d 7430 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))))
218107adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
219215, 218eqeltrrd 2829 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) ∈ β„‚)
220169, 218, 219addsub12d 11616 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))))
22160adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐹:β„βŸΆβ„‚)
2223adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐴 ∈ ℝ)
2238adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐡 ∈ ℝ)
224 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘₯ ∈ (𝐴[,]𝐡))
225 eliccre 44813 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘₯ ∈ ℝ)
226222, 223, 224, 225syl3anc 1369 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘₯ ∈ ℝ)
227221, 226ffvelcdmd 7089 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
228227, 213itgcl 25700 . . . . . . . . . . 11 (πœ‘ β†’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
229228adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
230169, 169, 229subsub4d 11624 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ((∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
231230eqcomd 2733 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ((∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
232231oveq2d 7430 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ((∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
233169subidd 11581 . . . . . . . . . 10 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = 0)
234233oveq1d 7429 . . . . . . . . 9 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ((∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (0 βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
235 df-neg 11469 . . . . . . . . 9 -∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ = (0 βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
236234, 235eqtr4di 2785 . . . . . . . 8 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ((∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = -∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
237236oveq2d 7430 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ((∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + -∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
238218, 229negsubd 11599 . . . . . . 7 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + -∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
239232, 237, 2383eqtrd 2771 . . . . . 6 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
240217, 220, 2393eqtrd 2771 . . . . 5 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
241188, 189, 2403eqtr3d 2775 . . . 4 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ = (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
242241oveq2d 7430 . . 3 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
243108, 107, 228subsubd 11621 . . . . 5 (πœ‘ β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ((∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
24493oveq2d 7430 . . . . . . 7 (πœ‘ β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
245244, 109eqtrd 2767 . . . . . 6 (πœ‘ β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = 0)
246245oveq1d 7429 . . . . 5 (πœ‘ β†’ ((∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (0 + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
247228addlidd 11437 . . . . 5 (πœ‘ β†’ (0 + ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
248243, 246, 2473eqtrd 2771 . . . 4 (πœ‘ β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
249248adantr 480 . . 3 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
250184, 242, 2493eqtrd 2771 . 2 ((πœ‘ ∧ 𝑇 < 𝑋) β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
25124adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (𝐴 βˆ’ 𝑋) ∈ ℝ)
25214adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
2533adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝐴 ∈ ℝ)
25424, 3, 39ltled 11384 . . . . . . 7 (πœ‘ β†’ (𝐴 βˆ’ 𝑋) ≀ 𝐴)
255254adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (𝐴 βˆ’ 𝑋) ≀ 𝐴)
2566adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝑋 ∈ ℝ)
2578adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝐡 ∈ ℝ)
258 id 22 . . . . . . . . 9 (𝑋 ≀ 𝑇 β†’ 𝑋 ≀ 𝑇)
259258, 1breqtrdi 5183 . . . . . . . 8 (𝑋 ≀ 𝑇 β†’ 𝑋 ≀ (𝐡 βˆ’ 𝐴))
260259adantl 481 . . . . . . 7 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝑋 ≀ (𝐡 βˆ’ 𝐴))
261256, 257, 253, 260lesubd 11840 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝐴 ≀ (𝐡 βˆ’ 𝑋))
262251, 252, 253, 255, 261eliccd 44812 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝐴 ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋)))
263158adantlr 714 . . . . 5 (((πœ‘ ∧ 𝑋 ≀ 𝑇) ∧ π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
264132, 102, 3, 39, 73eliood 44806 . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ ((𝐴 βˆ’ 𝑋)(,)+∞))
26536, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264fourierdlem105 45522 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
266265adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (π‘₯ ∈ ((𝐴 βˆ’ 𝑋)[,]𝐴) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
2673leidd 11802 . . . . . . . 8 (πœ‘ β†’ 𝐴 ≀ 𝐴)
2685rpge0d 13044 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝑋)
2698, 6subge02d 11828 . . . . . . . . 9 (πœ‘ β†’ (0 ≀ 𝑋 ↔ (𝐡 βˆ’ 𝑋) ≀ 𝐡))
270268, 269mpbid 231 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ’ 𝑋) ≀ 𝐡)
271 iccss 13416 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ 𝐴 ∧ (𝐡 βˆ’ 𝑋) ≀ 𝐡)) β†’ (𝐴[,](𝐡 βˆ’ 𝑋)) βŠ† (𝐴[,]𝐡))
2723, 8, 267, 270, 271syl22anc 838 . . . . . . 7 (πœ‘ β†’ (𝐴[,](𝐡 βˆ’ 𝑋)) βŠ† (𝐴[,]𝐡))
273 iccmbl 25482 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ (𝐡 βˆ’ 𝑋) ∈ ℝ) β†’ (𝐴[,](𝐡 βˆ’ 𝑋)) ∈ dom vol)
2743, 14, 273syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴[,](𝐡 βˆ’ 𝑋)) ∈ dom vol)
275272, 274, 227, 213iblss 25721 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋)) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
276275adantr 480 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋)) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
277251, 252, 262, 263, 266, 276itgspliticc 25753 . . . 4 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯))
278268adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 0 ≀ 𝑋)
279269adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (0 ≀ 𝑋 ↔ (𝐡 βˆ’ 𝑋) ≀ 𝐡))
280278, 279mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (𝐡 βˆ’ 𝑋) ≀ 𝐡)
281253, 257, 252, 261, 280eliccd 44812 . . . . . . . 8 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (𝐡 βˆ’ 𝑋) ∈ (𝐴[,]𝐡))
282227adantlr 714 . . . . . . . 8 (((πœ‘ ∧ 𝑋 ≀ 𝑇) ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
2838leidd 11802 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ≀ 𝐡)
284283adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ 𝐡 ≀ 𝐡)
285 iccss 13416 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) ∧ (𝐴 ≀ (𝐡 βˆ’ 𝑋) ∧ 𝐡 ≀ 𝐡)) β†’ ((𝐡 βˆ’ 𝑋)[,]𝐡) βŠ† (𝐴[,]𝐡))
286253, 257, 261, 284, 285syl22anc 838 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ((𝐡 βˆ’ 𝑋)[,]𝐡) βŠ† (𝐴[,]𝐡))
287 iccmbl 25482 . . . . . . . . . . 11 (((𝐡 βˆ’ 𝑋) ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((𝐡 βˆ’ 𝑋)[,]𝐡) ∈ dom vol)
28814, 8, 287syl2anc 583 . . . . . . . . . 10 (πœ‘ β†’ ((𝐡 βˆ’ 𝑋)[,]𝐡) ∈ dom vol)
289288adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ((𝐡 βˆ’ 𝑋)[,]𝐡) ∈ dom vol)
290213adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
291286, 289, 282, 290iblss 25721 . . . . . . . 8 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (π‘₯ ∈ ((𝐡 βˆ’ 𝑋)[,]𝐡) ↦ (πΉβ€˜π‘₯)) ∈ 𝐿1)
292253, 257, 281, 282, 276, 291itgspliticc 25753 . . . . . . 7 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ = (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
293292oveq1d 7429 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = ((∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
29460adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ 𝐹:β„βŸΆβ„‚)
2953adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ 𝐴 ∈ ℝ)
29614adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ (𝐡 βˆ’ 𝑋) ∈ ℝ)
297 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋)))
298 eliccre 44813 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ (𝐡 βˆ’ 𝑋) ∈ ℝ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ π‘₯ ∈ ℝ)
299295, 296, 297, 298syl3anc 1369 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ π‘₯ ∈ ℝ)
300294, 299ffvelcdmd 7089 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,](𝐡 βˆ’ 𝑋))) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
301300, 275itgcl 25700 . . . . . . . 8 (πœ‘ β†’ ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
302301, 107, 107addsubassd 11613 . . . . . . 7 (πœ‘ β†’ ((∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
303302adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ((∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
304185oveq2d 7430 . . . . . . . 8 (πœ‘ β†’ (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + 0))
305301addridd 11436 . . . . . . . 8 (πœ‘ β†’ (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + 0) = ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯)
306304, 305eqtrd 2767 . . . . . . 7 (πœ‘ β†’ (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯)
307306adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯)
308293, 303, 3073eqtrrd 2772 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
309308oveq2d 7430 . . . 4 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + ∫(𝐴[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯) = (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
31093adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ = ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯)
311107adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
312310, 311eqeltrrd 2829 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
313282, 290itgcl 25700 . . . . . 6 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ ∈ β„‚)
314312, 313, 311addsub12d 11616 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
315313, 312, 311addsubassd 11613 . . . . 5 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ((∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)))
316314, 315eqtr4d 2770 . . . 4 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ (∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯ + (∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)) = ((∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
317277, 309, 3163eqtrd 2771 . . 3 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = ((∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯))
318310oveq2d 7430 . . 3 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ((∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐡 βˆ’ 𝑋)[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯) = ((∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯))
319313, 312pncand 11594 . . 3 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ((∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯ + ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) βˆ’ ∫((𝐴 βˆ’ 𝑋)[,]𝐴)(πΉβ€˜π‘₯) dπ‘₯) = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
320317, 318, 3193eqtrd 2771 . 2 ((πœ‘ ∧ 𝑋 ≀ 𝑇) β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
321250, 320, 47, 6ltlecasei 11344 1 (πœ‘ β†’ ∫((𝐴 βˆ’ 𝑋)[,](𝐡 βˆ’ 𝑋))(πΉβ€˜π‘₯) dπ‘₯ = ∫(𝐴[,]𝐡)(πΉβ€˜π‘₯) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427   βˆͺ cun 3942   βŠ† wss 3944  ifcif 4524  {cpr 4626   class class class wbr 5142   ↦ cmpt 5225  dom cdm 5672  ran crn 5673   β†Ύ cres 5674  β„©cio 6492  βŸΆwf 6538  β€˜cfv 6542   Isom wiso 6543  (class class class)co 7414   ↑m cmap 8836  supcsup 9455  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135  +∞cpnf 11267  β„*cxr 11269   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466  -cneg 11467   / cdiv 11893  β„•cn 12234  β„€cz 12580  β„+crp 12998  (,)cioo 13348  (,]cioc 13349  [,]cicc 13351  ...cfz 13508  ..^cfzo 13651  βŒŠcfl 13779  β™―chash 14313  β€“cnβ†’ccncf 24783  volcvol 25379  πΏ1cibl 25533  βˆ«citg 25534   limβ„‚ climc 25778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cc 10450  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-symdif 4238  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-ofr 7680  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-omul 8485  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-dju 9916  df-card 9954  df-acn 9957  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-xnn0 12567  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-sum 15657  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-ovol 25380  df-vol 25381  df-mbf 25535  df-itg1 25536  df-itg2 25537  df-ibl 25538  df-itg 25539  df-0p 25586  df-ditg 25763  df-limc 25782  df-dv 25783
This theorem is referenced by:  fourierdlem108  45525
  Copyright terms: Public domain W3C validator