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 46785

Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 46770 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 7411	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝑋) + (𝐵 − 𝐴))
3		fourierdlem107.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4	3	recnd 11225	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		fourierdlem107.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
6	5	rpred 13051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ℝ)
7	6	recnd 11225	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ ℂ)
8		fourierdlem107.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	8	recnd 11225	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10	4, 7, 9, 4	subadd4b 45860	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝑋) + (𝐵 − 𝐴)) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
11	2, 10	eqtrid 2812	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
12	4	subidd 11545	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
13	12	oveq1d 7415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝐴) + (𝐵 − 𝑋)) = (0 + (𝐵 − 𝑋)))
14	8, 6	resubcld 11630	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
15	14	recnd 11225	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
16	15	addlidd 11399	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0 + (𝐵 − 𝑋)) = (𝐵 − 𝑋))
17	11, 13, 16	3eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = (𝐵 − 𝑋))
18	1	oveq2i 7411	. . . . . . . . . . . . . . 15 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
19	4, 9	pncan3d 11560	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
20	18, 19	eqtrid 2812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
21	17, 20	oveq12d 7418	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵 − 𝑋)[,]𝐵))
22	21	eqcomd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) = (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)))
23	22	itgeq1d 46529	. . . . . . . . . . 11 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥)
24	3, 6	resubcld 11630	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ)
25		fourierdlem107.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		fveq2 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘𝑖) = (𝑝‘𝑗))
27		oveq1 7407	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
28	27	fveq2d 6875	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
29	26, 28	breq12d 5118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
30	29	cbvralvw 3243	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
32	31	anbi2d 641	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → ((((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))))
33	32	rabbidv 3424	. . . . . . . . . . . . . 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 2788	. . . . . . . . . . . 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 13083	. . . . . . . . . . . . . . 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 46732	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
44	43	simpld 499	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
45	44	simpld 499	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46	8, 3	resubcld 11630	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
47	1, 46	eqeltrid 2869	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
48	44	simprd 500	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
49	24	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐴 − 𝑋) ∈ ℝ)
50	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴))
52		eliccre 46079	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
53	49, 50, 51, 52	syl3anc 1394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54		fourierdlem107.fper	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
55	53, 54	syldan 602	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
56		fveq2 6871	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑆‘𝑖) = (𝑆‘𝑗))
57	56	oveq1d 7415	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑆‘𝑖) + 𝑇) = ((𝑆‘𝑗) + 𝑇))
58	57	cbvmptv 5209	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑁) ↦ ((𝑆‘𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆‘𝑗) + 𝑇))
59		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
60		fourierdlem107.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
61	37	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
62	38	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃‘𝑀))
63	60	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
64	54	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
65		fourierdlem107.fcn	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66	65	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
67	24	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ)
68	67	rexrd 11247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ^*)
69		pnfxr 11251	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ^*)
71	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
72	39	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) < 𝐴)
73	3	ltpnfd 13137	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 < +∞)
74	73	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
75	68, 70, 71, 72, 74	eliood 46072	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
76		fourierdlem107.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
77		fourierdlem107.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
78		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
79		eqid 2765	. . . . . . . . . . . . 13 ⊢ ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
80		eqid 2765	. . . . . . . . . . . . 13 ⊢ (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
81		eqid 2765	. . . . . . . . . . . . 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 46768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84		fourierdlem107.r	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
85	84	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
86		eqid 2765	. . . . . . . . . . . . 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 46767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝑗))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
88		fourierdlem107.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	88	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90		eqid 2765	. . . . . . . . . . . . 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 46769	. . . . . . . . . . . 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 46770	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
93	23, 92	eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
94	60	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
95	14	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ)
96	8	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵))
98		eliccre 46079	. . . . . . . . . . . . 13 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
99	95, 96, 97, 98	syl3anc 1394	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
100	94, 99	ffvelcdmd 7070	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
101	14	rexrd 11247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ^*)
102	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → +∞ ∈ ℝ^*)
103	8, 5	ltsubrpd 13083	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) < 𝐵)
104	8	ltpnfd 13137	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 < +∞)
105	101, 102, 8, 103, 104	eliood 46072	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ((𝐵 − 𝑋)(,)+∞))
106	36, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105	fourierdlem105 46783	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
107	100, 106	itgcl 25904	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
108	93, 107	eqeltrrd 2866	. . . . . . . . 9 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
109	108	subidd 11545	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
110	109	eqcomd 2771	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
111	110	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
112	24	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ∈ ℝ)
113	3	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ℝ)
114	14	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ)
115	36, 37, 38	fourierdlem11 46690	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116	115	simp3d 1160	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
117	3, 8, 116	ltled 11346	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
118	117	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ≤ 𝐵)
119	3, 8, 6	lesub1d 11809	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
120	119	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
121	118, 120	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ≤ (𝐵 − 𝑋))
122	8	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐵 ∈ ℝ)
123	6	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑋 ∈ ℝ)
124		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑇 < 𝑋)
125	1, 124	eqbrtrrid 5141	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝐴) < 𝑋)
126	122, 113, 123, 125	ltsub23d 11807	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) < 𝐴)
127	114, 113, 126	ltled 11346	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ≤ 𝐴)
128	112, 113, 114, 121, 127	eliccd 46078	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)[,]𝐴))
129	60	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130	129, 53	ffvelcdmd 7070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
131	130	adantlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
132	24	rexrd 11247	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ^*)
133	3, 8, 6, 116	ltsub1dd 11814	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) < (𝐵 − 𝑋))
134	14	ltpnfd 13137	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 − 𝑋) < +∞)
135	132, 102, 14, 133, 134	eliood 46072	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)(,)+∞))
136	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135	fourierdlem105 46783	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
137	136	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
138	37	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑀 ∈ ℕ)
139	38	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑄 ∈ (𝑃‘𝑀))
140	60	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐹:ℝ⟶ℂ)
141	54	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
142	65	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
143	84	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
144	88	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
145	101	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ^*)
146	69	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → +∞ ∈ ℝ^*)
147	113	ltpnfd 13137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 < +∞)
148	145, 146, 113, 126, 147	eliood 46072	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)(,)+∞))
149	36, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148	fourierdlem105 46783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
150	112, 113, 128, 131, 137, 149	itgspliticc 25957	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
151	150	oveq1d 7415	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
152	60	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
153	24	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ)
154	14	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
155		simpr 489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
156		eliccre 46079	. . . . . . . . . . 11 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
157	153, 154, 155, 156	syl3anc 1394	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
158	152, 157	ffvelcdmd 7070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
159	158, 136	itgcl 25904	. . . . . . . 8 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
160	159	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
161	60	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
162	14	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐵 − 𝑋) ∈ ℝ)
163	3	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
164		simpr 489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴))
165		eliccre 46079	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166	162, 163, 164, 165	syl3anc 1394	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167	161, 166	ffvelcdmd 7070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
168	167	adantlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
169	168, 149	itgcl 25904	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
170	108	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
171	160, 169, 170	addsubassd 11577	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
172	111, 151, 171	3eqtrd 2804	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
173	172	oveq2d 7416	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
174	160	subid1d 11546	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
175	159	subidd 11545	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = 0)
176	175	oveq1d 7415	. . . . . 6 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
177	176	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
178	169, 170	subcld 11557	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) ∈ ℂ)
179	160, 160, 178	subsub4d 11588	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
180		df-neg 11432	. . . . . 6 ⊢ -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
181	169, 170	negsubdi2d 11573	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
182	180, 181	eqtr3id 2814	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
183	177, 179, 182	3eqtr3d 2808	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
184	173, 174, 183	3eqtr3d 2808	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
185	107	subidd 11545	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
186	185	eqcomd 2771	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
187	186	oveq2d 7416	. . . . . 6 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
188	187	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
189	169	addridd 11398	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
190	114, 122, 113, 127, 118	eliccd 46078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)[,]𝐵))
191	100	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
192	3, 8	iccssred 13452	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
193	60, 192	feqresmpt 6940	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
194	60, 192	fssresd 6735	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195		ioossicc 13451	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
196	3	rexrd 11247	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
197	196	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ^*)
198	8	rexrd 11247	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
199	198	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ^*)
200	36, 37, 38	fourierdlem15 46694	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201	200	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203	197, 199, 201, 202	fourierdlem8 46687	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204	195, 203	sstrid 3950	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205	204	resabs1d 5998	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
206	205, 65	eqeltrd 2865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207	205	eqcomd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
208	207	oveq1d 7415	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
209	84, 208	eleqtrd 2867	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
210	207	oveq1d 7415	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
211	88, 210	eleqtrd 2867	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
212	36, 37, 38, 194, 206, 209, 211	fourierdlem69 46747	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿¹)
213	193, 212	eqeltrrd 2866	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
214	213	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
215	114, 122, 190, 191, 149, 214	itgspliticc 25957	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
216	215	oveq2d 7416	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
217	216	oveq2d 7416	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
218	107	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
219	215, 218	eqeltrrd 2866	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) ∈ ℂ)
220	169, 218, 219	addsub12d 11580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
221	60	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ)
222	3	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
223	8	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
224		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
225		eliccre 46079	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226	222, 223, 224, 225	syl3anc 1394	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227	221, 226	ffvelcdmd 7070	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
228	227, 213	itgcl 25904	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
229	228	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
230	169, 169, 229	subsub4d 11588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
231	230	eqcomd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
232	231	oveq2d 7416	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
233	169	subidd 11545	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
234	233	oveq1d 7415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
235		df-neg 11432	. . . . . . . . 9 ⊢ -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
236	234, 235	eqtr4di 2818	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
237	236	oveq2d 7416	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
238	218, 229	negsubd 11563	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
239	232, 237, 238	3eqtrd 2804	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
240	217, 220, 239	3eqtrd 2804	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
241	188, 189, 240	3eqtr3d 2808	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
242	241	oveq2d 7416	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
243	108, 107, 228	subsubd 11585	. . . . 5 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
244	93	oveq2d 7416	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
245	244, 109	eqtrd 2800	. . . . . 6 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
246	245	oveq1d 7415	. . . . 5 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
247	228	addlidd 11399	. . . . 5 ⊢ (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
248	243, 246, 247	3eqtrd 2804	. . . 4 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
249	248	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
250	184, 242, 249	3eqtrd 2804	. 2 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
251	24	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ∈ ℝ)
252	14	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ ℝ)
253	3	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ℝ)
254	24, 3, 39	ltled 11346	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑋) ≤ 𝐴)
255	254	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ≤ 𝐴)
256	6	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ∈ ℝ)
257	8	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ∈ ℝ)
258		id 23	. . . . . . . . 9 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ 𝑇)
259	258, 1	breqtrdi 5146	. . . . . . . 8 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ (𝐵 − 𝐴))
260	259	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ≤ (𝐵 − 𝐴))
261	256, 257, 253, 260	lesubd 11806	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ≤ (𝐵 − 𝑋))
262	251, 252, 253, 255, 261	eliccd 46078	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
263	158	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
264	132, 102, 3, 39, 73	eliood 46072	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
265	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264	fourierdlem105 46783	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
266	265	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
267	3	leidd 11768	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
268	5	rpge0d 13055	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑋)
269	8, 6	subge02d 11794	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
270	268, 269	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ≤ 𝐵)
271		iccss 13432	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐴 ∧ (𝐵 − 𝑋) ≤ 𝐵)) → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
272	3, 8, 267, 270, 271	syl22anc 851	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
273		iccmbl 25686	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
274	3, 14, 273	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
275	272, 274, 227, 213	iblss 25925	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
276	275	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
277	251, 252, 262, 263, 266, 276	itgspliticc 25957	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥))
278	268	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 0 ≤ 𝑋)
279	269	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
280	278, 279	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ≤ 𝐵)
281	253, 257, 252, 261, 280	eliccd 46078	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ (𝐴[,]𝐵))
282	227	adantlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
283	8	leidd 11768	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
284	283	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ≤ 𝐵)
285		iccss 13432	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵 − 𝑋) ∧ 𝐵 ≤ 𝐵)) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286	253, 257, 261, 284, 285	syl22anc 851	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287		iccmbl 25686	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
288	14, 8, 287	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
289	288	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
290	213	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
291	286, 289, 282, 290	iblss 25925	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
292	253, 257, 281, 282, 276, 291	itgspliticc 25957	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
293	292	oveq1d 7415	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
294	60	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
295	3	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ)
296	14	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
297		simpr 489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ (𝐴[,](𝐵 − 𝑋)))
298		eliccre 46079	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
299	295, 296, 297, 298	syl3anc 1394	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
300	294, 299	ffvelcdmd 7070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
301	300, 275	itgcl 25904	. . . . . . . 8 ⊢ (𝜑 → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
302	301, 107, 107	addsubassd 11577	. . . . . . 7 ⊢ (𝜑 → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
303	302	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
304	185	oveq2d 7416	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0))
305	301	addridd 11398	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
306	304, 305	eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
307	306	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
308	293, 303, 307	3eqtrrd 2805	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
309	308	oveq2d 7416	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
310	93	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
311	107	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
312	310, 311	eqeltrrd 2866	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
313	282, 290	itgcl 25904	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
314	312, 313, 311	addsub12d 11580	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
315	313, 312, 311	addsubassd 11577	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
316	314, 315	eqtr4d 2803	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
317	277, 309, 316	3eqtrd 2804	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
318	310	oveq2d 7416	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
319	313, 312	pncand 11558	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
320	317, 318, 319	3eqtrd 2804	. 2 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
321	250, 320, 47, 6	ltlecasei 11306	1 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ∃wrex 3089 {crab 3417 ∪ cun 3905 ⊆ wss 3907 ifcif 4483 {cpr 4587 class class class wbr 5105 ↦ cmpt 5186 dom cdm 5652 ran crn 5653 ↾ cres 5654 ℩cio 6479 ⟶wf 6521 ‘cfv 6525 Isom wiso 6526 (class class class)co 7400 ↑_m cmap 8812 supcsup 9388 ℂcc 11086 ℝcr 11087 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 +∞cpnf 11228 ℝ^*cxr 11230 < clt 11231 ≤ cle 11232 − cmin 11429 -cneg 11430 / cdiv 11859 ℕcn 12224 ℤcz 12582 ℝ⁺crp 13007 (,)cioo 13363 (,]cioc 13364 [,]cicc 13366 ...cfz 13526 ..^cfzo 13673 ⌊cfl 13814 ♯chash 14357 –cn→ccncf 24996 volcvol 25583 𝐿¹cibl 25737 ∫citg 25738 lim_ℂ climc 25982

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598 ax-cc 10407 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-addf 11167

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-symdif 4208 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-iin 4955 df-disj 5073 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-ofr 7665 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-oadd 8445 df-omul 8446 df-er 8682 df-map 8814 df-pm 8815 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-fi 9359 df-sup 9390 df-inf 9391 df-oi 9460 df-dju 9875 df-card 9913 df-acn 9916 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-xnn0 12569 df-z 12583 df-dec 12703 df-uz 12854 df-q 12964 df-rp 13008 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13367 df-ioc 13368 df-ico 13369 df-icc 13370 df-fz 13527 df-fzo 13674 df-fl 13816 df-mod 13894 df-seq 14029 df-exp 14089 df-hash 14358 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-limsup 15512 df-clim 15529 df-rlim 15530 df-sum 15728 df-struct 17197 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-ress 17281 df-plusg 17313 df-mulr 17314 df-starv 17315 df-sca 17316 df-vsca 17317 df-ip 17318 df-tset 17319 df-ple 17320 df-ds 17322 df-unif 17323 df-hom 17324 df-cco 17325 df-rest 17465 df-topn 17466 df-0g 17484 df-gsum 17485 df-topgen 17486 df-pt 17487 df-prds 17490 df-xrs 17546 df-qtop 17551 df-imas 17552 df-xps 17554 df-mre 17628 df-mrc 17629 df-acs 17631 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-submnd 18832 df-mulg 19125 df-cntz 19378 df-cmn 19843 df-psmet 21474 df-xmet 21475 df-met 21476 df-bl 21477 df-mopn 21478 df-fbas 21479 df-fg 21480 df-cnfld 21483 df-top 23012 df-topon 23029 df-topsp 23051 df-bases 23064 df-cld 23137 df-ntr 23138 df-cls 23139 df-nei 23216 df-lp 23254 df-perf 23255 df-cn 23345 df-cnp 23346 df-haus 23433 df-cmp 23505 df-tx 23680 df-hmeo 23873 df-fil 23964 df-fm 24056 df-flim 24057 df-flf 24058 df-xms 24438 df-ms 24439 df-tms 24440 df-cncf 24998 df-ovol 25584 df-vol 25585 df-mbf 25739 df-itg1 25740 df-itg2 25741 df-ibl 25742 df-itg 25743 df-0p 25790 df-ditg 25967 df-limc 25986 df-dv 25987

This theorem is referenced by: fourierdlem108 46786

W3C validator