fourierdlem107 - Mathbox for Glauco Siliprandi

	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.

Step	Hyp	Ref	Expression
1		fourierdlem107.t	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 = (𝐵 − 𝐴)
2	1	oveq2i 7430	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝑋) + (𝐵 − 𝐴))
3		fourierdlem107.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4	3	recnd 11279	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		fourierdlem107.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
6	5	rpred 13056	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ℝ)
7	6	recnd 11279	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ ℂ)
8		fourierdlem107.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	8	recnd 11279	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10	4, 7, 9, 4	subadd4b 44807	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝑋) + (𝐵 − 𝐴)) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
11	2, 10	eqtrid 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
12	4	subidd 11596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
13	12	oveq1d 7434	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝐴) + (𝐵 − 𝑋)) = (0 + (𝐵 − 𝑋)))
14	8, 6	resubcld 11679	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
15	14	recnd 11279	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
16	15	addlidd 11452	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0 + (𝐵 − 𝑋)) = (𝐵 − 𝑋))
17	11, 13, 16	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = (𝐵 − 𝑋))
18	1	oveq2i 7430	. . . . . . . . . . . . . . 15 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
19	4, 9	pncan3d 11611	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
20	18, 19	eqtrid 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
21	17, 20	oveq12d 7437	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵 − 𝑋)[,]𝐵))
22	21	eqcomd 2731	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) = (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)))
23	22	itgeq1d 45488	. . . . . . . . . . 11 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥)
24	3, 6	resubcld 11679	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ)
25		fourierdlem107.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		fveq2 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘𝑖) = (𝑝‘𝑗))
27		oveq1 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
28	27	fveq2d 6900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
29	26, 28	breq12d 5162	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
30	29	cbvralvw 3224	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
32	31	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → ((((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))))
33	32	rabbidv 3426	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
34	33	mpteq2ia 5252	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
35	25, 34	eqtri 2753	. . . . . . . . . . . 12 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
36		fourierdlem107.p	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
37		fourierdlem107.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℕ)
38		fourierdlem107.q	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
39	3, 5	ltsubrpd 13088	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 − 𝑋) < 𝐴)
40		fourierdlem107.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = ({(𝐴 − 𝑋), 𝐴} ∪ {𝑦 ∈ ((𝐴 − 𝑋)[,]𝐴) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
41		fourierdlem107.n	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = ((♯‘𝐻) − 1)
42		fourierdlem107.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
43	1, 36, 37, 38, 24, 3, 39, 25, 40, 41, 42	fourierdlem54 45691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
44	43	simpld 493	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
45	44	simpld 493	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46	8, 3	resubcld 11679	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
47	1, 46	eqeltrid 2829	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
48	44	simprd 494	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
49	24	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐴 − 𝑋) ∈ ℝ)
50	3	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51		simpr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴))
52		eliccre 45033	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
53	49, 50, 51, 52	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54		fourierdlem107.fper	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
55	53, 54	syldan 589	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
56		fveq2 6896	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑆‘𝑖) = (𝑆‘𝑗))
57	56	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑆‘𝑖) + 𝑇) = ((𝑆‘𝑗) + 𝑇))
58	57	cbvmptv 5262	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑁) ↦ ((𝑆‘𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆‘𝑗) + 𝑇))
59		eqid 2725	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
60		fourierdlem107.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
61	37	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
62	38	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃‘𝑀))
63	60	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
64	54	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
65		fourierdlem107.fcn	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66	65	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
67	24	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ)
68	67	rexrd 11301	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ^*)
69		pnfxr 11305	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ^*)
71	3	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
72	39	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) < 𝐴)
73	3	ltpnfd 13141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 < +∞)
74	73	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
75	68, 70, 71, 72, 74	eliood 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..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ))
83	36, 1, 61, 62, 63, 64, 66, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 80, 81, 82	fourierdlem90 45727	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84		fourierdlem107.r	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
85	84	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
86		eqid 2725	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) ↦ 𝑅) = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
87	36, 1, 61, 62, 63, 64, 66, 85, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 86	fourierdlem89 45726	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝑗))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
88		fourierdlem107.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	88	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90		eqid 2725	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0..^𝑀) ↦ 𝐿) = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
91	36, 1, 61, 62, 63, 64, 66, 89, 67, 75, 25, 40, 41, 42, 76, 77, 78, 79, 82, 90	fourierdlem91 45728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
92	24, 3, 35, 45, 47, 48, 55, 58, 59, 60, 83, 87, 91	fourierdlem92 45729	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
93	23, 92	eqtrd 2765	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
94	60	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
95	14	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ)
96	8	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97		simpr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵))
98		eliccre 45033	. . . . . . . . . . . . 13 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
99	95, 96, 97, 98	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
100	94, 99	ffvelcdmd 7094	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
101	14	rexrd 11301	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ^*)
102	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → +∞ ∈ ℝ^*)
103	8, 5	ltsubrpd 13088	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) < 𝐵)
104	8	ltpnfd 13141	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 < +∞)
105	101, 102, 8, 103, 104	eliood 45026	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ((𝐵 − 𝑋)(,)+∞))
106	36, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105	fourierdlem105 45742	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
107	100, 106	itgcl 25774	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
108	93, 107	eqeltrrd 2826	. . . . . . . . 9 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
109	108	subidd 11596	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
110	109	eqcomd 2731	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
111	110	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
112	24	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ∈ ℝ)
113	3	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ℝ)
114	14	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ)
115	36, 37, 38	fourierdlem11 45649	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116	115	simp3d 1141	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
117	3, 8, 116	ltled 11399	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
118	117	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ≤ 𝐵)
119	3, 8, 6	lesub1d 11858	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
120	119	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
121	118, 120	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ≤ (𝐵 − 𝑋))
122	8	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐵 ∈ ℝ)
123	6	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑋 ∈ ℝ)
124		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑇 < 𝑋)
125	1, 124	eqbrtrrid 5185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝐴) < 𝑋)
126	122, 113, 123, 125	ltsub23d 11856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) < 𝐴)
127	114, 113, 126	ltled 11399	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ≤ 𝐴)
128	112, 113, 114, 121, 127	eliccd 45032	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)[,]𝐴))
129	60	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130	129, 53	ffvelcdmd 7094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
131	130	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
132	24	rexrd 11301	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ^*)
133	3, 8, 6, 116	ltsub1dd 11863	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) < (𝐵 − 𝑋))
134	14	ltpnfd 13141	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 − 𝑋) < +∞)
135	132, 102, 14, 133, 134	eliood 45026	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)(,)+∞))
136	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135	fourierdlem105 45742	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
137	136	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
138	37	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑀 ∈ ℕ)
139	38	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑄 ∈ (𝑃‘𝑀))
140	60	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐹:ℝ⟶ℂ)
141	54	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
142	65	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
143	84	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
144	88	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
145	101	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ^*)
146	69	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → +∞ ∈ ℝ^*)
147	113	ltpnfd 13141	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 < +∞)
148	145, 146, 113, 126, 147	eliood 45026	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)(,)+∞))
149	36, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148	fourierdlem105 45742	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
150	112, 113, 128, 131, 137, 149	itgspliticc 25827	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
151	150	oveq1d 7434	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
152	60	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
153	24	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ)
154	14	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
155		simpr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
156		eliccre 45033	. . . . . . . . . . 11 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
157	153, 154, 155, 156	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
158	152, 157	ffvelcdmd 7094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
159	158, 136	itgcl 25774	. . . . . . . 8 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
160	159	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
161	60	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
162	14	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐵 − 𝑋) ∈ ℝ)
163	3	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
164		simpr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴))
165		eliccre 45033	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166	162, 163, 164, 165	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167	161, 166	ffvelcdmd 7094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
168	167	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
169	168, 149	itgcl 25774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
170	108	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
171	160, 169, 170	addsubassd 11628	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
172	111, 151, 171	3eqtrd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
173	172	oveq2d 7435	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
174	160	subid1d 11597	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
175	159	subidd 11596	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = 0)
176	175	oveq1d 7434	. . . . . 6 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
177	176	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
178	169, 170	subcld 11608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) ∈ ℂ)
179	160, 160, 178	subsub4d 11639	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
180		df-neg 11484	. . . . . 6 ⊢ -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
181	169, 170	negsubdi2d 11624	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
182	180, 181	eqtr3id 2779	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
183	177, 179, 182	3eqtr3d 2773	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
184	173, 174, 183	3eqtr3d 2773	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
185	107	subidd 11596	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
186	185	eqcomd 2731	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
187	186	oveq2d 7435	. . . . . 6 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
188	187	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
189	169	addridd 11451	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
190	114, 122, 113, 127, 118	eliccd 45032	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)[,]𝐵))
191	100	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
192	3, 8	iccssred 13451	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
193	60, 192	feqresmpt 6967	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
194	60, 192	fssresd 6764	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195		ioossicc 13450	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
196	3	rexrd 11301	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
197	196	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ^*)
198	8	rexrd 11301	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
199	198	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ^*)
200	36, 37, 38	fourierdlem15 45653	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201	200	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203	197, 199, 201, 202	fourierdlem8 45646	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204	195, 203	sstrid 3988	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205	204	resabs1d 6013	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
206	205, 65	eqeltrd 2825	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207	205	eqcomd 2731	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
208	207	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
209	84, 208	eleqtrd 2827	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
210	207	oveq1d 7434	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
211	88, 210	eleqtrd 2827	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
212	36, 37, 38, 194, 206, 209, 211	fourierdlem69 45706	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿¹)
213	193, 212	eqeltrrd 2826	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
214	213	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
215	114, 122, 190, 191, 149, 214	itgspliticc 25827	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
216	215	oveq2d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
217	216	oveq2d 7435	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
218	107	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
219	215, 218	eqeltrrd 2826	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) ∈ ℂ)
220	169, 218, 219	addsub12d 11631	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
221	60	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ)
222	3	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
223	8	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
224		simpr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
225		eliccre 45033	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226	222, 223, 224, 225	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227	221, 226	ffvelcdmd 7094	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
228	227, 213	itgcl 25774	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
229	228	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
230	169, 169, 229	subsub4d 11639	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
231	230	eqcomd 2731	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
232	231	oveq2d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
233	169	subidd 11596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
234	233	oveq1d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
235		df-neg 11484	. . . . . . . . 9 ⊢ -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
236	234, 235	eqtr4di 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
237	236	oveq2d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
238	218, 229	negsubd 11614	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
239	232, 237, 238	3eqtrd 2769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
240	217, 220, 239	3eqtrd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
241	188, 189, 240	3eqtr3d 2773	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
242	241	oveq2d 7435	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
243	108, 107, 228	subsubd 11636	. . . . 5 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
244	93	oveq2d 7435	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
245	244, 109	eqtrd 2765	. . . . . 6 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
246	245	oveq1d 7434	. . . . 5 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
247	228	addlidd 11452	. . . . 5 ⊢ (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
248	243, 246, 247	3eqtrd 2769	. . . 4 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
249	248	adantr 479	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
250	184, 242, 249	3eqtrd 2769	. 2 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
251	24	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ∈ ℝ)
252	14	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ ℝ)
253	3	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ℝ)
254	24, 3, 39	ltled 11399	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑋) ≤ 𝐴)
255	254	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ≤ 𝐴)
256	6	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ∈ ℝ)
257	8	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ∈ ℝ)
258		id 22	. . . . . . . . 9 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ 𝑇)
259	258, 1	breqtrdi 5190	. . . . . . . 8 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ (𝐵 − 𝐴))
260	259	adantl 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ≤ (𝐵 − 𝐴))
261	256, 257, 253, 260	lesubd 11855	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ≤ (𝐵 − 𝑋))
262	251, 252, 253, 255, 261	eliccd 45032	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
263	158	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
264	132, 102, 3, 39, 73	eliood 45026	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
265	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264	fourierdlem105 45742	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
266	265	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
267	3	leidd 11817	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
268	5	rpge0d 13060	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑋)
269	8, 6	subge02d 11843	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
270	268, 269	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ≤ 𝐵)
271		iccss 13432	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐴 ∧ (𝐵 − 𝑋) ≤ 𝐵)) → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
272	3, 8, 267, 270, 271	syl22anc 837	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
273		iccmbl 25556	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
274	3, 14, 273	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
275	272, 274, 227, 213	iblss 25795	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
276	275	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
277	251, 252, 262, 263, 266, 276	itgspliticc 25827	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥))
278	268	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 0 ≤ 𝑋)
279	269	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
280	278, 279	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ≤ 𝐵)
281	253, 257, 252, 261, 280	eliccd 45032	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ (𝐴[,]𝐵))
282	227	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
283	8	leidd 11817	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
284	283	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ≤ 𝐵)
285		iccss 13432	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵 − 𝑋) ∧ 𝐵 ≤ 𝐵)) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286	253, 257, 261, 284, 285	syl22anc 837	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287		iccmbl 25556	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
288	14, 8, 287	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
289	288	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
290	213	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
291	286, 289, 282, 290	iblss 25795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
292	253, 257, 281, 282, 276, 291	itgspliticc 25827	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
293	292	oveq1d 7434	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
294	60	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
295	3	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ)
296	14	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
297		simpr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ (𝐴[,](𝐵 − 𝑋)))
298		eliccre 45033	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
299	295, 296, 297, 298	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
300	294, 299	ffvelcdmd 7094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
301	300, 275	itgcl 25774	. . . . . . . 8 ⊢ (𝜑 → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
302	301, 107, 107	addsubassd 11628	. . . . . . 7 ⊢ (𝜑 → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
303	302	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
304	185	oveq2d 7435	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0))
305	301	addridd 11451	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
306	304, 305	eqtrd 2765	. . . . . . 7 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
307	306	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
308	293, 303, 307	3eqtrrd 2770	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
309	308	oveq2d 7435	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
310	93	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
311	107	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
312	310, 311	eqeltrrd 2826	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
313	282, 290	itgcl 25774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
314	312, 313, 311	addsub12d 11631	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
315	313, 312, 311	addsubassd 11628	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
316	314, 315	eqtr4d 2768	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
317	277, 309, 316	3eqtrd 2769	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
318	310	oveq2d 7435	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
319	313, 312	pncand 11609	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
320	317, 318, 319	3eqtrd 2769	. 2 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
321	250, 320, 47, 6	ltlecasei 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 –cn→ccncf 24857 volcvol 25453 𝐿¹cibl 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

W3C validator