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 47192

Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 47177 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 7429	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝑋) + (𝐵 − 𝐴))
3		fourierdlem107.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4	3	recnd 11330	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		fourierdlem107.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
6	5	rpred 13157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ℝ)
7	6	recnd 11330	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ ℂ)
8		fourierdlem107.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	8	recnd 11330	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10	4, 7, 9, 4	subadd4b 46268	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝑋) + (𝐵 − 𝐴)) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
11	2, 10	eqtrid 2808	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
12	4	subidd 11650	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
13	12	oveq1d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝐴) + (𝐵 − 𝑋)) = (0 + (𝐵 − 𝑋)))
14	8, 6	resubcld 11737	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
15	14	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
16	15	addlidd 11504	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0 + (𝐵 − 𝑋)) = (𝐵 − 𝑋))
17	11, 13, 16	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = (𝐵 − 𝑋))
18	1	oveq2i 7429	. . . . . . . . . . . . . . 15 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
19	4, 9	pncan3d 11665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
20	18, 19	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
21	17, 20	oveq12d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵 − 𝑋)[,]𝐵))
22	21	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) = (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)))
23	22	itgeq1d 46936	. . . . . . . . . . 11 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥)
24	3, 6	resubcld 11737	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ)
25		fourierdlem107.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		fveq2 6883	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘𝑖) = (𝑝‘𝑗))
27		oveq1 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
28	27	fveq2d 6887	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
29	26, 28	breq12d 5116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
30	29	cbvralvw 3241	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
32	31	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → ((((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))))
33	32	rabbidv 3420	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
34	33	mpteq2ia 5200	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
35	25, 34	eqtri 2784	. . . . . . . . . . . 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 13189	. . . . . . . . . . . . . . 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 47139	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
44	43	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
45	44	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46	8, 3	resubcld 11737	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
47	1, 46	eqeltrid 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
48	44	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
49	24	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐴 − 𝑋) ∈ ℝ)
50	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴))
52		eliccre 46486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
53	49, 50, 51, 52	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54		fourierdlem107.fper	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
55	53, 54	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
56		fveq2 6883	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑆‘𝑖) = (𝑆‘𝑗))
57	56	oveq1d 7433	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑆‘𝑖) + 𝑇) = ((𝑆‘𝑗) + 𝑇))
58	57	cbvmptv 5209	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑁) ↦ ((𝑆‘𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆‘𝑗) + 𝑇))
59		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
60		fourierdlem107.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
61	37	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
62	38	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃‘𝑀))
63	60	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
64	54	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
65		fourierdlem107.fcn	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66	65	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
67	24	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ)
68	67	rexrd 11352	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ^*)
69		pnfxr 11356	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ^*)
71	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
72	39	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) < 𝐴)
73	3	ltpnfd 13243	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 < +∞)
74	73	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
75	68, 70, 71, 72, 74	eliood 46479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
76		fourierdlem107.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
77		fourierdlem107.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
78		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
79		eqid 2761	. . . . . . . . . . . . 13 ⊢ ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
80		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
81		eqid 2761	. . . . . . . . . . . . 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 47175	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84		fourierdlem107.r	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
85	84	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
86		eqid 2761	. . . . . . . . . . . . 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 47174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝑗))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
88		fourierdlem107.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	88	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90		eqid 2761	. . . . . . . . . . . . 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 47176	. . . . . . . . . . . 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 47177	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
93	23, 92	eqtrd 2796	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
94	60	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
95	14	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ)
96	8	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵))
98		eliccre 46486	. . . . . . . . . . . . 13 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
99	95, 96, 97, 98	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
100	94, 99	ffvelcdmd 7083	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
101	14	rexrd 11352	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ^*)
102	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → +∞ ∈ ℝ^*)
103	8, 5	ltsubrpd 13189	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) < 𝐵)
104	8	ltpnfd 13243	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 < +∞)
105	101, 102, 8, 103, 104	eliood 46479	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ((𝐵 − 𝑋)(,)+∞))
106	36, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105	fourierdlem105 47190	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
107	100, 106	itgcl 26097	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
108	93, 107	eqeltrrd 2862	. . . . . . . . 9 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
109	108	subidd 11650	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
110	109	eqcomd 2767	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
111	110	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
112	24	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ∈ ℝ)
113	3	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ℝ)
114	14	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ)
115	36, 37, 38	fourierdlem11 47097	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116	115	simp3d 1162	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
117	3, 8, 116	ltled 11451	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
118	117	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ≤ 𝐵)
119	3, 8, 6	lesub1d 11916	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
120	119	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
121	118, 120	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ≤ (𝐵 − 𝑋))
122	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐵 ∈ ℝ)
123	6	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑋 ∈ ℝ)
124		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑇 < 𝑋)
125	1, 124	eqbrtrrid 5141	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝐴) < 𝑋)
126	122, 113, 123, 125	ltsub23d 11914	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) < 𝐴)
127	114, 113, 126	ltled 11451	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ≤ 𝐴)
128	112, 113, 114, 121, 127	eliccd 46485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)[,]𝐴))
129	60	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130	129, 53	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
131	130	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
132	24	rexrd 11352	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ^*)
133	3, 8, 6, 116	ltsub1dd 11921	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) < (𝐵 − 𝑋))
134	14	ltpnfd 13243	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 − 𝑋) < +∞)
135	132, 102, 14, 133, 134	eliood 46479	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)(,)+∞))
136	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135	fourierdlem105 47190	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
137	136	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
138	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑀 ∈ ℕ)
139	38	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑄 ∈ (𝑃‘𝑀))
140	60	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐹:ℝ⟶ℂ)
141	54	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
142	65	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
143	84	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
144	88	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
145	101	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ^*)
146	69	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → +∞ ∈ ℝ^*)
147	113	ltpnfd 13243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 < +∞)
148	145, 146, 113, 126, 147	eliood 46479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)(,)+∞))
149	36, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148	fourierdlem105 47190	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
150	112, 113, 128, 131, 137, 149	itgspliticc 26150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
151	150	oveq1d 7433	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
152	60	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
153	24	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ)
154	14	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
155		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
156		eliccre 46486	. . . . . . . . . . 11 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
157	153, 154, 155, 156	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
158	152, 157	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
159	158, 136	itgcl 26097	. . . . . . . 8 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
160	159	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
161	60	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
162	14	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐵 − 𝑋) ∈ ℝ)
163	3	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
164		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴))
165		eliccre 46486	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166	162, 163, 164, 165	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167	161, 166	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
168	167	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
169	168, 149	itgcl 26097	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
170	108	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
171	160, 169, 170	addsubassd 11682	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
172	111, 151, 171	3eqtrd 2800	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
173	172	oveq2d 7434	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
174	160	subid1d 11651	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
175	159	subidd 11650	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = 0)
176	175	oveq1d 7433	. . . . . 6 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
177	176	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
178	169, 170	subcld 11662	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) ∈ ℂ)
179	160, 160, 178	subsub4d 11693	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
180		df-neg 11537	. . . . . 6 ⊢ -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
181	169, 170	negsubdi2d 11678	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
182	180, 181	eqtr3id 2810	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
183	177, 179, 182	3eqtr3d 2804	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
184	173, 174, 183	3eqtr3d 2804	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
185	107	subidd 11650	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
186	185	eqcomd 2767	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
187	186	oveq2d 7434	. . . . . 6 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
188	187	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
189	169	addridd 11503	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
190	114, 122, 113, 127, 118	eliccd 46485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)[,]𝐵))
191	100	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
192	3, 8	iccssred 13558	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
193	60, 192	feqresmpt 6952	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
194	60, 192	fssresd 6747	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195		ioossicc 13557	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
196	3	rexrd 11352	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
197	196	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ^*)
198	8	rexrd 11352	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
199	198	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ^*)
200	36, 37, 38	fourierdlem15 47101	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201	200	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203	197, 199, 201, 202	fourierdlem8 47094	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204	195, 203	sstrid 3942	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205	204	resabs1d 5999	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
206	205, 65	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207	205	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
208	207	oveq1d 7433	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
209	84, 208	eleqtrd 2863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
210	207	oveq1d 7433	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
211	88, 210	eleqtrd 2863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
212	36, 37, 38, 194, 206, 209, 211	fourierdlem69 47154	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿¹)
213	193, 212	eqeltrrd 2862	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
214	213	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
215	114, 122, 190, 191, 149, 214	itgspliticc 26150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
216	215	oveq2d 7434	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
217	216	oveq2d 7434	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
218	107	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
219	215, 218	eqeltrrd 2862	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) ∈ ℂ)
220	169, 218, 219	addsub12d 11685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
221	60	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ)
222	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
223	8	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
224		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
225		eliccre 46486	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226	222, 223, 224, 225	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227	221, 226	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
228	227, 213	itgcl 26097	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
229	228	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
230	169, 169, 229	subsub4d 11693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
231	230	eqcomd 2767	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
232	231	oveq2d 7434	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
233	169	subidd 11650	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
234	233	oveq1d 7433	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
235		df-neg 11537	. . . . . . . . 9 ⊢ -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
236	234, 235	eqtr4di 2814	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
237	236	oveq2d 7434	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
238	218, 229	negsubd 11668	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
239	232, 237, 238	3eqtrd 2800	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
240	217, 220, 239	3eqtrd 2800	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
241	188, 189, 240	3eqtr3d 2804	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
242	241	oveq2d 7434	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
243	108, 107, 228	subsubd 11690	. . . . 5 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
244	93	oveq2d 7434	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
245	244, 109	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
246	245	oveq1d 7433	. . . . 5 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
247	228	addlidd 11504	. . . . 5 ⊢ (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
248	243, 246, 247	3eqtrd 2800	. . . 4 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
249	248	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
250	184, 242, 249	3eqtrd 2800	. 2 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
251	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ∈ ℝ)
252	14	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ ℝ)
253	3	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ℝ)
254	24, 3, 39	ltled 11451	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑋) ≤ 𝐴)
255	254	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ≤ 𝐴)
256	6	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ∈ ℝ)
257	8	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ∈ ℝ)
258		id 23	. . . . . . . . 9 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ 𝑇)
259	258, 1	breqtrdi 5146	. . . . . . . 8 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ (𝐵 − 𝐴))
260	259	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ≤ (𝐵 − 𝐴))
261	256, 257, 253, 260	lesubd 11913	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ≤ (𝐵 − 𝑋))
262	251, 252, 253, 255, 261	eliccd 46485	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
263	158	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
264	132, 102, 3, 39, 73	eliood 46479	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
265	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264	fourierdlem105 47190	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
266	265	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
267	3	leidd 11875	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
268	5	rpge0d 13161	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑋)
269	8, 6	subge02d 11901	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
270	268, 269	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ≤ 𝐵)
271		iccss 13538	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐴 ∧ (𝐵 − 𝑋) ≤ 𝐵)) → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
272	3, 8, 267, 270, 271	syl22anc 852	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
273		iccmbl 25880	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
274	3, 14, 273	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
275	272, 274, 227, 213	iblss 26118	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
276	275	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
277	251, 252, 262, 263, 266, 276	itgspliticc 26150	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥))
278	268	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 0 ≤ 𝑋)
279	269	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
280	278, 279	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ≤ 𝐵)
281	253, 257, 252, 261, 280	eliccd 46485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ (𝐴[,]𝐵))
282	227	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
283	8	leidd 11875	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
284	283	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ≤ 𝐵)
285		iccss 13538	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵 − 𝑋) ∧ 𝐵 ≤ 𝐵)) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286	253, 257, 261, 284, 285	syl22anc 852	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287		iccmbl 25880	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
288	14, 8, 287	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
289	288	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
290	213	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
291	286, 289, 282, 290	iblss 26118	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
292	253, 257, 281, 282, 276, 291	itgspliticc 26150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
293	292	oveq1d 7433	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
294	60	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
295	3	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ)
296	14	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
297		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ (𝐴[,](𝐵 − 𝑋)))
298		eliccre 46486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
299	295, 296, 297, 298	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
300	294, 299	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
301	300, 275	itgcl 26097	. . . . . . . 8 ⊢ (𝜑 → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
302	301, 107, 107	addsubassd 11682	. . . . . . 7 ⊢ (𝜑 → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
303	302	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
304	185	oveq2d 7434	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0))
305	301	addridd 11503	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
306	304, 305	eqtrd 2796	. . . . . . 7 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
307	306	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
308	293, 303, 307	3eqtrrd 2801	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
309	308	oveq2d 7434	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
310	93	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
311	107	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
312	310, 311	eqeltrrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
313	282, 290	itgcl 26097	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
314	312, 313, 311	addsub12d 11685	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
315	313, 312, 311	addsubassd 11682	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
316	314, 315	eqtr4d 2799	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
317	277, 309, 316	3eqtrd 2800	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
318	310	oveq2d 7434	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
319	313, 312	pncand 11663	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
320	317, 318, 319	3eqtrd 2800	. 2 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
321	250, 320, 47, 6	ltlecasei 11411	1 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ∃wrex 3087 {crab 3413 ∪ cun 3897 ⊆ wss 3899 ifcif 4482 {cpr 4586 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ran crn 5652 ↾ cres 5653 ℩cio 6491 ⟶wf 6533 ‘cfv 6537 Isom wiso 6538 (class class class)co 7418 ↑_m cmap 8840 supcsup 9425 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 · cmul 11198 +∞cpnf 11333 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 − cmin 11534 -cneg 11535 / cdiv 11966 ℕcn 12328 ℤcz 12686 ℝ⁺crp 13113 (,)cioo 13469 (,]cioc 13470 [,]cicc 13472 ...cfz 13632 ..^cfzo 13781 ⌊cfl 13923 ♯chash 14467 –cn→ccncf 25190 volcvol 25777 𝐿¹cibl 25931 ∫citg 25932 lim_ℂ climc 26175

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cc 10506 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-symdif 4199 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-ofr 7692 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-oadd 8473 df-omul 8474 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-acn 10016 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-xnn0 12673 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ioc 13474 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-mod 14003 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-limsup 15631 df-clim 15648 df-rlim 15649 df-sum 15847 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-submnd 18972 df-mulg 19271 df-cntz 19524 df-cmn 19989 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-cmp 23698 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-xms 24632 df-ms 24633 df-tms 24634 df-cncf 25192 df-ovol 25778 df-vol 25779 df-mbf 25933 df-itg1 25934 df-itg2 25935 df-ibl 25936 df-itg 25937 df-0p 25984 df-ditg 26160 df-limc 26179 df-dv 26180

This theorem is used by: fourierdlem108 47193

W3C validator