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 46218

Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 46203 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 7401	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝑋) + (𝐵 − 𝐴))
3		fourierdlem107.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4	3	recnd 11209	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		fourierdlem107.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
6	5	rpred 13002	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ℝ)
7	6	recnd 11209	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ ℂ)
8		fourierdlem107.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	8	recnd 11209	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10	4, 7, 9, 4	subadd4b 45288	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝑋) + (𝐵 − 𝐴)) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
11	2, 10	eqtrid 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
12	4	subidd 11528	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
13	12	oveq1d 7405	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝐴) + (𝐵 − 𝑋)) = (0 + (𝐵 − 𝑋)))
14	8, 6	resubcld 11613	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
15	14	recnd 11209	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
16	15	addlidd 11382	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0 + (𝐵 − 𝑋)) = (𝐵 − 𝑋))
17	11, 13, 16	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = (𝐵 − 𝑋))
18	1	oveq2i 7401	. . . . . . . . . . . . . . 15 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
19	4, 9	pncan3d 11543	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
20	18, 19	eqtrid 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
21	17, 20	oveq12d 7408	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵 − 𝑋)[,]𝐵))
22	21	eqcomd 2736	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) = (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)))
23	22	itgeq1d 45962	. . . . . . . . . . 11 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥)
24	3, 6	resubcld 11613	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ)
25		fourierdlem107.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		fveq2 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘𝑖) = (𝑝‘𝑗))
27		oveq1 7397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
28	27	fveq2d 6865	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
29	26, 28	breq12d 5123	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
30	29	cbvralvw 3216	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))
31	30	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
32	31	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → ((((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))))
33	32	rabbidv 3416	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
34	33	mpteq2ia 5205	. . . . . . . . . . . . 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 13034	. . . . . . . . . . . . . . 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 46165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
44	43	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
45	44	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46	8, 3	resubcld 11613	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
47	1, 46	eqeltrid 2833	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
48	44	simprd 495	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
49	24	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐴 − 𝑋) ∈ ℝ)
50	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴))
52		eliccre 45510	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
53	49, 50, 51, 52	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54		fourierdlem107.fper	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
55	53, 54	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
56		fveq2 6861	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑆‘𝑖) = (𝑆‘𝑗))
57	56	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑆‘𝑖) + 𝑇) = ((𝑆‘𝑗) + 𝑇))
58	57	cbvmptv 5214	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑁) ↦ ((𝑆‘𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆‘𝑗) + 𝑇))
59		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = ((𝐴 − 𝑋) + 𝑇) ∧ (𝑝‘𝑚) = (𝐴 + 𝑇)) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
60		fourierdlem107.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
61	37	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
62	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃‘𝑀))
63	60	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
64	54	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
65		fourierdlem107.fcn	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
66	65	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
67	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ)
68	67	rexrd 11231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ^*)
69		pnfxr 11235	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ^*)
71	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
72	39	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) < 𝐴)
73	3	ltpnfd 13088	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 < +∞)
74	73	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
75	68, 70, 71, 72, 74	eliood 45503	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
76		fourierdlem107.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
77		fourierdlem107.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
78		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
79		eqid 2730	. . . . . . . . . . . . 13 ⊢ ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
80		eqid 2730	. . . . . . . . . . . . 13 ⊢ (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
81		eqid 2730	. . . . . . . . . . . . 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 46201	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84		fourierdlem107.r	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
85	84	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
86		eqid 2730	. . . . . . . . . . . . 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 46200	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝑗))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
88		fourierdlem107.l	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
89	88	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
90		eqid 2730	. . . . . . . . . . . . 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 46202	. . . . . . . . . . . 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 46203	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
93	23, 92	eqtrd 2765	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
94	60	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
95	14	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ)
96	8	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵))
98		eliccre 45510	. . . . . . . . . . . . 13 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
99	95, 96, 97, 98	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
100	94, 99	ffvelcdmd 7060	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
101	14	rexrd 11231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ^*)
102	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → +∞ ∈ ℝ^*)
103	8, 5	ltsubrpd 13034	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) < 𝐵)
104	8	ltpnfd 13088	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 < +∞)
105	101, 102, 8, 103, 104	eliood 45503	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ((𝐵 − 𝑋)(,)+∞))
106	36, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105	fourierdlem105 46216	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
107	100, 106	itgcl 25692	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
108	93, 107	eqeltrrd 2830	. . . . . . . . 9 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
109	108	subidd 11528	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
110	109	eqcomd 2736	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
111	110	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
112	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ∈ ℝ)
113	3	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ℝ)
114	14	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ)
115	36, 37, 38	fourierdlem11 46123	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116	115	simp3d 1144	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
117	3, 8, 116	ltled 11329	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
118	117	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ≤ 𝐵)
119	3, 8, 6	lesub1d 11792	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
120	119	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝑋) ≤ (𝐵 − 𝑋)))
121	118, 120	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐴 − 𝑋) ≤ (𝐵 − 𝑋))
122	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐵 ∈ ℝ)
123	6	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑋 ∈ ℝ)
124		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑇 < 𝑋)
125	1, 124	eqbrtrrid 5146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝐴) < 𝑋)
126	122, 113, 123, 125	ltsub23d 11790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) < 𝐴)
127	114, 113, 126	ltled 11329	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ≤ 𝐴)
128	112, 113, 114, 121, 127	eliccd 45509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)[,]𝐴))
129	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130	129, 53	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
131	130	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
132	24	rexrd 11231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ^*)
133	3, 8, 6, 116	ltsub1dd 11797	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) < (𝐵 − 𝑋))
134	14	ltpnfd 13088	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 − 𝑋) < +∞)
135	132, 102, 14, 133, 134	eliood 45503	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)(,)+∞))
136	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135	fourierdlem105 46216	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
137	136	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
138	37	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑀 ∈ ℕ)
139	38	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝑄 ∈ (𝑃‘𝑀))
140	60	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐹:ℝ⟶ℂ)
141	54	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
142	65	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
143	84	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
144	88	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
145	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ℝ^*)
146	69	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → +∞ ∈ ℝ^*)
147	113	ltpnfd 13088	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 < +∞)
148	145, 146, 113, 126, 147	eliood 45503	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)(,)+∞))
149	36, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148	fourierdlem105 46216	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
150	112, 113, 128, 131, 137, 149	itgspliticc 25745	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
151	150	oveq1d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
152	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
153	24	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐴 − 𝑋) ∈ ℝ)
154	14	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
155		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
156		eliccre 45510	. . . . . . . . . . 11 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
157	153, 154, 155, 156	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
158	152, 157	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
159	158, 136	itgcl 25692	. . . . . . . 8 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
160	159	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
161	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
162	14	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐵 − 𝑋) ∈ ℝ)
163	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
164		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴))
165		eliccre 45510	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166	162, 163, 164, 165	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167	161, 166	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
168	167	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
169	168, 149	itgcl 25692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
170	108	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
171	160, 169, 170	addsubassd 11560	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
172	111, 151, 171	3eqtrd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
173	172	oveq2d 7406	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
174	160	subid1d 11529	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
175	159	subidd 11528	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = 0)
176	175	oveq1d 7405	. . . . . 6 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
177	176	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
178	169, 170	subcld 11540	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) ∈ ℂ)
179	160, 160, 178	subsub4d 11571	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
180		df-neg 11415	. . . . . 6 ⊢ -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
181	169, 170	negsubdi2d 11556	. . . . . 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 11528	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
186	185	eqcomd 2736	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
187	186	oveq2d 7406	. . . . . 6 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
188	187	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
189	169	addridd 11381	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
190	114, 122, 113, 127, 118	eliccd 45509	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)[,]𝐵))
191	100	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
192	3, 8	iccssred 13402	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
193	60, 192	feqresmpt 6933	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
194	60, 192	fssresd 6730	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195		ioossicc 13401	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
196	3	rexrd 11231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
197	196	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ^*)
198	8	rexrd 11231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
199	198	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ^*)
200	36, 37, 38	fourierdlem15 46127	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201	200	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203	197, 199, 201, 202	fourierdlem8 46120	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204	195, 203	sstrid 3961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205	204	resabs1d 5982	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
206	205, 65	eqeltrd 2829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207	205	eqcomd 2736	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
208	207	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
209	84, 208	eleqtrd 2831	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
210	207	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
211	88, 210	eleqtrd 2831	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
212	36, 37, 38, 194, 206, 209, 211	fourierdlem69 46180	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿¹)
213	193, 212	eqeltrrd 2830	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
214	213	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
215	114, 122, 190, 191, 149, 214	itgspliticc 25745	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
216	215	oveq2d 7406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
217	216	oveq2d 7406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
218	107	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
219	215, 218	eqeltrrd 2830	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) ∈ ℂ)
220	169, 218, 219	addsub12d 11563	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
221	60	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:ℝ⟶ℂ)
222	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
223	8	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
224		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
225		eliccre 45510	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226	222, 223, 224, 225	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227	221, 226	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
228	227, 213	itgcl 25692	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
229	228	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
230	169, 169, 229	subsub4d 11571	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
231	230	eqcomd 2736	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
232	231	oveq2d 7406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
233	169	subidd 11528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
234	233	oveq1d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
235		df-neg 11415	. . . . . . . . 9 ⊢ -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
236	234, 235	eqtr4di 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
237	236	oveq2d 7406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
238	218, 229	negsubd 11546	. . . . . . 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 7406	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
243	108, 107, 228	subsubd 11568	. . . . 5 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
244	93	oveq2d 7406	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
245	244, 109	eqtrd 2765	. . . . . 6 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
246	245	oveq1d 7405	. . . . 5 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
247	228	addlidd 11382	. . . . 5 ⊢ (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
248	243, 246, 247	3eqtrd 2769	. . . 4 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
249	248	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
250	184, 242, 249	3eqtrd 2769	. 2 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
251	24	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ∈ ℝ)
252	14	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ ℝ)
253	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ℝ)
254	24, 3, 39	ltled 11329	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑋) ≤ 𝐴)
255	254	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ≤ 𝐴)
256	6	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ∈ ℝ)
257	8	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ∈ ℝ)
258		id 22	. . . . . . . . 9 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ 𝑇)
259	258, 1	breqtrdi 5151	. . . . . . . 8 ⊢ (𝑋 ≤ 𝑇 → 𝑋 ≤ (𝐵 − 𝐴))
260	259	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝑋 ≤ (𝐵 − 𝐴))
261	256, 257, 253, 260	lesubd 11789	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ≤ (𝐵 − 𝑋))
262	251, 252, 253, 255, 261	eliccd 45509	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
263	158	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
264	132, 102, 3, 39, 73	eliood 45503	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
265	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264	fourierdlem105 46216	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
266	265	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
267	3	leidd 11751	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
268	5	rpge0d 13006	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑋)
269	8, 6	subge02d 11777	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
270	268, 269	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ≤ 𝐵)
271		iccss 13382	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐴 ∧ (𝐵 − 𝑋) ≤ 𝐵)) → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
272	3, 8, 267, 270, 271	syl22anc 838	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
273		iccmbl 25474	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
274	3, 14, 273	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
275	272, 274, 227, 213	iblss 25713	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
276	275	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
277	251, 252, 262, 263, 266, 276	itgspliticc 25745	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥))
278	268	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 0 ≤ 𝑋)
279	269	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
280	278, 279	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ≤ 𝐵)
281	253, 257, 252, 261, 280	eliccd 45509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ (𝐴[,]𝐵))
282	227	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
283	8	leidd 11751	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
284	283	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ≤ 𝐵)
285		iccss 13382	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵 − 𝑋) ∧ 𝐵 ≤ 𝐵)) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286	253, 257, 261, 284, 285	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287		iccmbl 25474	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
288	14, 8, 287	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
289	288	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ∈ dom vol)
290	213	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
291	286, 289, 282, 290	iblss 25713	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
292	253, 257, 281, 282, 276, 291	itgspliticc 25745	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
293	292	oveq1d 7405	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
294	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐹:ℝ⟶ℂ)
295	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝐴 ∈ ℝ)
296	14	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐵 − 𝑋) ∈ ℝ)
297		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ (𝐴[,](𝐵 − 𝑋)))
298		eliccre 45510	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
299	295, 296, 297, 298	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
300	294, 299	ffvelcdmd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
301	300, 275	itgcl 25692	. . . . . . . 8 ⊢ (𝜑 → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
302	301, 107, 107	addsubassd 11560	. . . . . . 7 ⊢ (𝜑 → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
303	302	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
304	185	oveq2d 7406	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0))
305	301	addridd 11381	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
306	304, 305	eqtrd 2765	. . . . . . 7 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
307	306	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
308	293, 303, 307	3eqtrrd 2770	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
309	308	oveq2d 7406	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
310	93	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
311	107	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
312	310, 311	eqeltrrd 2830	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
313	282, 290	itgcl 25692	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
314	312, 313, 311	addsub12d 11563	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
315	313, 312, 311	addsubassd 11560	. . . . 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 7406	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
319	313, 312	pncand 11541	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
320	317, 318, 319	3eqtrd 2769	. 2 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
321	250, 320, 47, 6	ltlecasei 11289	1 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 {crab 3408 ∪ cun 3915 ⊆ wss 3917 ifcif 4491 {cpr 4594 class class class wbr 5110 ↦ cmpt 5191 dom cdm 5641 ran crn 5642 ↾ cres 5643 ℩cio 6465 ⟶wf 6510 ‘cfv 6514 Isom wiso 6515 (class class class)co 7390 ↑_m cmap 8802 supcsup 9398 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 · cmul 11080 +∞cpnf 11212 ℝ^*cxr 11214 < clt 11215 ≤ cle 11216 − cmin 11412 -cneg 11413 / cdiv 11842 ℕcn 12193 ℤcz 12536 ℝ⁺crp 12958 (,)cioo 13313 (,]cioc 13314 [,]cicc 13316 ...cfz 13475 ..^cfzo 13622 ⌊cfl 13759 ♯chash 14302 –cn→ccncf 24776 volcvol 25371 𝐿¹cibl 25525 ∫citg 25526 lim_ℂ climc 25770

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cc 10395 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-symdif 4219 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-disj 5078 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-ofr 7657 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-omul 8442 df-er 8674 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9861 df-card 9899 df-acn 9902 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-xnn0 12523 df-z 12537 df-dec 12657 df-uz 12801 df-q 12915 df-rp 12959 df-xneg 13079 df-xadd 13080 df-xmul 13081 df-ioo 13317 df-ioc 13318 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-limsup 15444 df-clim 15461 df-rlim 15462 df-sum 15660 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-rest 17392 df-topn 17393 df-0g 17411 df-gsum 17412 df-topgen 17413 df-pt 17414 df-prds 17417 df-xrs 17472 df-qtop 17477 df-imas 17478 df-xps 17480 df-mre 17554 df-mrc 17555 df-acs 17557 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-submnd 18718 df-mulg 19007 df-cntz 19256 df-cmn 19719 df-psmet 21263 df-xmet 21264 df-met 21265 df-bl 21266 df-mopn 21267 df-fbas 21268 df-fg 21269 df-cnfld 21272 df-top 22788 df-topon 22805 df-topsp 22827 df-bases 22840 df-cld 22913 df-ntr 22914 df-cls 22915 df-nei 22992 df-lp 23030 df-perf 23031 df-cn 23121 df-cnp 23122 df-haus 23209 df-cmp 23281 df-tx 23456 df-hmeo 23649 df-fil 23740 df-fm 23832 df-flim 23833 df-flf 23834 df-xms 24215 df-ms 24216 df-tms 24217 df-cncf 24778 df-ovol 25372 df-vol 25373 df-mbf 25527 df-itg1 25528 df-itg2 25529 df-ibl 25530 df-itg 25531 df-0p 25578 df-ditg 25755 df-limc 25774 df-dv 25775

This theorem is referenced by: fourierdlem108 46219

W3C validator