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 47041

Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by any positive value 𝑋. This lemma generalizes fourierdlem92 47026 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 7424	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝑋) + (𝐵 − 𝐴))
3		fourierdlem107.a	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4	3	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		fourierdlem107.x	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
6	5	rpred 13086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑋 ∈ ℝ)
7	6	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ ℂ)
8		fourierdlem107.b	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	8	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10	4, 7, 9, 4	subadd4b 46116	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 − 𝑋) + (𝐵 − 𝐴)) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
11	2, 10	eqtrid 2807	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = ((𝐴 − 𝐴) + (𝐵 − 𝑋)))
12	4	subidd 11581	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
13	12	oveq1d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 − 𝐴) + (𝐵 − 𝑋)) = (0 + (𝐵 − 𝑋)))
14	8, 6	resubcld 11666	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ)
15	14	recnd 11261	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℂ)
16	15	addlidd 11435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0 + (𝐵 − 𝑋)) = (𝐵 − 𝑋))
17	11, 13, 16	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 − 𝑋) + 𝑇) = (𝐵 − 𝑋))
18	1	oveq2i 7424	. . . . . . . . . . . . . . 15 ⊢ (𝐴 + 𝑇) = (𝐴 + (𝐵 − 𝐴))
19	4, 9	pncan3d 11596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = 𝐵)
20	18, 19	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵)
21	17, 20	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)) = ((𝐵 − 𝑋)[,]𝐵))
22	21	eqcomd 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 − 𝑋)[,]𝐵) = (((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇)))
23	22	itgeq1d 46785	. . . . . . . . . . 11 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥)
24	3, 6	resubcld 11666	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ)
25		fourierdlem107.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 − 𝑋) ∧ (𝑝‘𝑚) = 𝐴) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		fveq2 6878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘𝑖) = (𝑝‘𝑗))
27		oveq1 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
28	27	fveq2d 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
29	26, 28	breq12d 5116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
30	29	cbvralvw 3240	. . . . . . . . . . . . . . . . 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 3419	. . . . . . . . . . . . . 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 2783	. . . . . . . . . . . 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 13118	. . . . . . . . . . . . . . 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 46988	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
44	43	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
45	44	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
46	8, 3	resubcld 11666	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
47	1, 46	eqeltrid 2864	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
48	44	simprd 501	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
49	24	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐴 − 𝑋) ∈ ℝ)
50	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐴 ∈ ℝ)
51		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴))
52		eliccre 46335	. . . . . . . . . . . . . 14 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
53	49, 50, 51, 52	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
54		fourierdlem107.fper	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
55	53, 54	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
56		fveq2 6878	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑆‘𝑖) = (𝑆‘𝑗))
57	56	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → ((𝑆‘𝑖) + 𝑇) = ((𝑆‘𝑗) + 𝑇))
58	57	cbvmptv 5209	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑁) ↦ ((𝑆‘𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑁) ↦ ((𝑆‘𝑗) + 𝑇))
59		eqid 2760	. . . . . . . . . . . 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 11283	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) ∈ ℝ^*)
69		pnfxr 11287	. . . . . . . . . . . . . . 15 ⊢ +∞ ∈ ℝ^*
70	69	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → +∞ ∈ ℝ^*)
71	3	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
72	39	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 − 𝑋) < 𝐴)
73	3	ltpnfd 13172	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 < +∞)
74	73	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < +∞)
75	68, 70, 71, 72, 74	eliood 46328	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
76		fourierdlem107.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
77		fourierdlem107.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
78		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
79		eqid 2760	. . . . . . . . . . . . 13 ⊢ ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
80		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
81		eqid 2760	. . . . . . . . . . . . 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 47024	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
84		fourierdlem107.r	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
85	84	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
86		eqid 2760	. . . . . . . . . . . . 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 47023	. . . . . . . . . . . 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 2760	. . . . . . . . . . . . 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 47025	. . . . . . . . . . . 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 47026	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(((𝐴 − 𝑋) + 𝑇)[,](𝐴 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
93	23, 92	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
94	60	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐹:ℝ⟶ℂ)
95	14	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐵 − 𝑋) ∈ ℝ)
96	8	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝐵 ∈ ℝ)
97		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵))
98		eliccre 46335	. . . . . . . . . . . . 13 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
99	95, 96, 97, 98	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → 𝑥 ∈ ℝ)
100	94, 99	ffvelcdmd 7078	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
101	14	rexrd 11283	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ℝ^*)
102	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → +∞ ∈ ℝ^*)
103	8, 5	ltsubrpd 13118	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝑋) < 𝐵)
104	8	ltpnfd 13172	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 < +∞)
105	101, 102, 8, 103, 104	eliood 46328	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ((𝐵 − 𝑋)(,)+∞))
106	36, 1, 37, 38, 60, 54, 65, 84, 88, 14, 105	fourierdlem105 47039	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
107	100, 106	itgcl 26011	. . . . . . . . . 10 ⊢ (𝜑 → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
108	93, 107	eqeltrrd 2861	. . . . . . . . 9 ⊢ (𝜑 → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
109	108	subidd 11581	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
110	109	eqcomd 2766	. . . . . . 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 46946	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
116	115	simp3d 1162	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
117	3, 8, 116	ltled 11382	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
118	117	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ≤ 𝐵)
119	3, 8, 6	lesub1d 11845	. . . . . . . . . . 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 11843	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) < 𝐴)
127	114, 113, 126	ltled 11382	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ≤ 𝐴)
128	112, 113, 114, 121, 127	eliccd 46334	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)[,]𝐴))
129	60	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → 𝐹:ℝ⟶ℂ)
130	129, 53	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
131	130	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
132	24	rexrd 11283	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) ∈ ℝ^*)
133	3, 8, 6, 116	ltsub1dd 11850	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝑋) < (𝐵 − 𝑋))
134	14	ltpnfd 13172	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 − 𝑋) < +∞)
135	132, 102, 14, 133, 134	eliood 46328	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝑋) ∈ ((𝐴 − 𝑋)(,)+∞))
136	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 135	fourierdlem105 47039	. . . . . . . . 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 13172	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 < +∞)
148	145, 146, 113, 126, 147	eliood 46328	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)(,)+∞))
149	36, 1, 138, 139, 140, 141, 142, 143, 144, 114, 148	fourierdlem105 47039	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
150	112, 113, 128, 131, 137, 149	itgspliticc 26064	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
151	150	oveq1d 7428	. . . . . 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 46335	. . . . . . . . . . 11 ⊢ (((𝐴 − 𝑋) ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
157	153, 154, 155, 156	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
158	152, 157	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
159	158, 136	itgcl 26011	. . . . . . . 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 46335	. . . . . . . . . . 11 ⊢ (((𝐵 − 𝑋) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
166	162, 163, 164, 165	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → 𝑥 ∈ ℝ)
167	161, 166	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
168	167	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐴)) → (𝐹‘𝑥) ∈ ℂ)
169	168, 149	itgcl 26011	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
170	108	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
171	160, 169, 170	addsubassd 11613	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
172	111, 151, 171	3eqtrd 2799	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 0 = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
173	172	oveq2d 7429	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
174	160	subid1d 11582	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − 0) = ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
175	159	subidd 11581	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = 0)
176	175	oveq1d 7428	. . . . . 6 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
177	176	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)))
178	169, 170	subcld 11593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) ∈ ℂ)
179	160, 160, 178	subsub4d 11624	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))))
180		df-neg 11468	. . . . . 6 ⊢ -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
181	169, 170	negsubdi2d 11609	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → -(∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
182	180, 181	eqtr3id 2809	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (0 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
183	177, 179, 182	3eqtr3d 2803	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 − (∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
184	173, 174, 183	3eqtr3d 2803	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
185	107	subidd 11581	. . . . . . . 8 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
186	185	eqcomd 2766	. . . . . . 7 ⊢ (𝜑 → 0 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
187	186	oveq2d 7429	. . . . . 6 ⊢ (𝜑 → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
188	187	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
189	169	addridd 11434	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + 0) = ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
190	114, 122, 113, 127, 118	eliccd 46334	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → 𝐴 ∈ ((𝐵 − 𝑋)[,]𝐵))
191	100	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑇 < 𝑋) ∧ 𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
192	3, 8	iccssred 13487	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
193	60, 192	feqresmpt 6947	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))
194	60, 192	fssresd 6742	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℂ)
195		ioossicc 13486	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
196	3	rexrd 11283	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
197	196	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ^*)
198	8	rexrd 11283	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
199	198	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ^*)
200	36, 37, 38	fourierdlem15 46950	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
201	200	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
202		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
203	197, 199, 201, 202	fourierdlem8 46943	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
204	195, 203	sstrid 3942	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
205	204	resabs1d 6001	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
206	205, 65	eqeltrd 2860	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
207	205	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
208	207	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
209	84, 208	eleqtrd 2862	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
210	207	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
211	88, 210	eleqtrd 2862	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ (𝐴[,]𝐵)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
212	36, 37, 38, 194, 206, 209, 211	fourierdlem69 47003	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ 𝐿¹)
213	193, 212	eqeltrrd 2861	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
214	213	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
215	114, 122, 190, 191, 149, 214	itgspliticc 26064	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
216	215	oveq2d 7429	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
217	216	oveq2d 7429	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))))
218	107	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
219	215, 218	eqeltrrd 2861	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) ∈ ℂ)
220	169, 218, 219	addsub12d 11616	. . . . . 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 46335	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
226	222, 223, 224, 225	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
227	221, 226	ffvelcdmd 7078	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
228	227, 213	itgcl 26011	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
229	228	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
230	169, 169, 229	subsub4d 11624	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
231	230	eqcomd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
232	231	oveq2d 7429	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
233	169	subidd 11581	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = 0)
234	233	oveq1d 7428	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
235		df-neg 11468	. . . . . . . . 9 ⊢ -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (0 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
236	234, 235	eqtr4di 2813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
237	236	oveq2d 7429	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + ((∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
238	218, 229	negsubd 11599	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + -∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
239	232, 237, 238	3eqtrd 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
240	217, 220, 239	3eqtrd 2799	. . . . 5 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
241	188, 189, 240	3eqtr3d 2803	. . . 4 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 = (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
242	241	oveq2d 7429	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)))
243	108, 107, 228	subsubd 11621	. . . . 5 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
244	93	oveq2d 7429	. . . . . . 7 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
245	244, 109	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = 0)
246	245	oveq1d 7428	. . . . 5 ⊢ (𝜑 → ((∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))
247	228	addlidd 11435	. . . . 5 ⊢ (𝜑 → (0 + ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
248	243, 246, 247	3eqtrd 2799	. . . 4 ⊢ (𝜑 → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
249	248	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
250	184, 242, 249	3eqtrd 2799	. 2 ⊢ ((𝜑 ∧ 𝑇 < 𝑋) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
251	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐴 − 𝑋) ∈ ℝ)
252	14	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ ℝ)
253	3	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ℝ)
254	24, 3, 39	ltled 11382	. . . . . . 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 11842	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ≤ (𝐵 − 𝑋))
262	251, 252, 253, 255, 261	eliccd 46334	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐴 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋)))
263	158	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ ((𝐴 − 𝑋)[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
264	132, 102, 3, 39, 73	eliood 46328	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((𝐴 − 𝑋)(,)+∞))
265	36, 1, 37, 38, 60, 54, 65, 84, 88, 24, 264	fourierdlem105 47039	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
266	265	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐴 − 𝑋)[,]𝐴) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
267	3	leidd 11804	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ 𝐴)
268	5	rpge0d 13090	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑋)
269	8, 6	subge02d 11830	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ 𝑋 ↔ (𝐵 − 𝑋) ≤ 𝐵))
270	268, 269	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝑋) ≤ 𝐵)
271		iccss 13467	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ 𝐴 ∧ (𝐵 − 𝑋) ≤ 𝐵)) → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
272	3, 8, 267, 270, 271	syl22anc 852	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ⊆ (𝐴[,]𝐵))
273		iccmbl 25794	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ) → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
274	3, 14, 273	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐴[,](𝐵 − 𝑋)) ∈ dom vol)
275	272, 274, 227, 213	iblss 26032	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
276	275	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ (𝐴[,](𝐵 − 𝑋)) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
277	251, 252, 262, 263, 266, 276	itgspliticc 26064	. . . 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 46334	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝐵 − 𝑋) ∈ (𝐴[,]𝐵))
282	227	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑋 ≤ 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
283	8	leidd 11804	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
284	283	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → 𝐵 ≤ 𝐵)
285		iccss 13467	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≤ (𝐵 − 𝑋) ∧ 𝐵 ≤ 𝐵)) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
286	253, 257, 261, 284, 285	syl22anc 852	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((𝐵 − 𝑋)[,]𝐵) ⊆ (𝐴[,]𝐵))
287		iccmbl 25794	. . . . . . . . . . 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 26032	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (𝑥 ∈ ((𝐵 − 𝑋)[,]𝐵) ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
292	253, 257, 281, 282, 276, 291	itgspliticc 26064	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
293	292	oveq1d 7428	. . . . . 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 46335	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 − 𝑋) ∈ ℝ ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
299	295, 296, 297, 298	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → 𝑥 ∈ ℝ)
300	294, 299	ffvelcdmd 7078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,](𝐵 − 𝑋))) → (𝐹‘𝑥) ∈ ℂ)
301	300, 275	itgcl 26011	. . . . . . . 8 ⊢ (𝜑 → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 ∈ ℂ)
302	301, 107, 107	addsubassd 11613	. . . . . . 7 ⊢ (𝜑 → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
303	302	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
304	185	oveq2d 7429	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0))
305	301	addridd 11434	. . . . . . . 8 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + 0) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
306	304, 305	eqtrd 2795	. . . . . . 7 ⊢ (𝜑 → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
307	306	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 + (∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥)
308	293, 303, 307	3eqtrrd 2800	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
309	308	oveq2d 7429	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + ∫(𝐴[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥) = (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
310	93	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥)
311	107	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
312	310, 311	eqeltrrd 2861	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 ∈ ℂ)
313	282, 290	itgcl 26011	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 ∈ ℂ)
314	312, 313, 311	addsub12d 11616	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
315	313, 312, 311	addsubassd 11613	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)))
316	314, 315	eqtr4d 2798	. . . 4 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → (∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥 + (∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥)) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
317	277, 309, 316	3eqtrd 2799	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥))
318	310	oveq2d 7429	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐵 − 𝑋)[,]𝐵)(𝐹‘𝑥) d𝑥) = ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥))
319	313, 312	pncand 11594	. . 3 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ((∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 + ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) − ∫((𝐴 − 𝑋)[,]𝐴)(𝐹‘𝑥) d𝑥) = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
320	317, 318, 319	3eqtrd 2799	. 2 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑇) → ∫((𝐴 − 𝑋)[,](𝐵 − 𝑋))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
321	250, 320, 47, 6	ltlecasei 11342	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 3076 ∃wrex 3086 {crab 3412 ∪ cun 3897 ⊆ wss 3899 ifcif 4482 {cpr 4586 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5655 ran crn 5656 ↾ cres 5657 ℩cio 6487 ⟶wf 6529 ‘cfv 6533 Isom wiso 6534 (class class class)co 7413 ↑_m cmap 8826 supcsup 9410 ℂcc 11122 ℝcr 11123 0cc0 11124 1c1 11125 + caddc 11127 · cmul 11129 +∞cpnf 11264 ℝ^*cxr 11266 < clt 11267 ≤ cle 11268 − cmin 11465 -cneg 11466 / cdiv 11895 ℕcn 12257 ℤcz 12615 ℝ⁺crp 13042 (,)cioo 13398 (,]cioc 13399 [,]cicc 13401 ...cfz 13561 ..^cfzo 13709 ⌊cfl 13851 ♯chash 14394 –cn→ccncf 25104 volcvol 25691 𝐿¹cibl 25845 ∫citg 25846 lim_ℂ climc 26089

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 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-inf2 9620 ax-cc 10437 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202 ax-addf 11203

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 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 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7678 df-ofr 7679 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-oadd 8459 df-omul 8460 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-acn 9947 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-div 11896 df-nn 12258 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12529 df-xnn0 12602 df-z 12616 df-dec 12737 df-uz 12888 df-q 12998 df-rp 13043 df-xneg 13163 df-xadd 13164 df-xmul 13165 df-ioo 13402 df-ioc 13403 df-ico 13404 df-icc 13405 df-fz 13562 df-fzo 13710 df-fl 13853 df-mod 13931 df-seq 14066 df-exp 14126 df-hash 14395 df-cj 15186 df-re 15187 df-im 15188 df-sqrt 15322 df-abs 15323 df-limsup 15558 df-clim 15575 df-rlim 15576 df-sum 15774 df-struct 17239 df-sets 17256 df-slot 17274 df-ndx 17286 df-base 17302 df-ress 17323 df-plusg 17355 df-mulr 17356 df-starv 17357 df-sca 17358 df-vsca 17359 df-ip 17360 df-tset 17361 df-ple 17362 df-ds 17364 df-unif 17365 df-hom 17366 df-cco 17367 df-rest 17507 df-topn 17508 df-0g 17526 df-gsum 17527 df-topgen 17528 df-pt 17529 df-prds 17532 df-xrs 17588 df-qtop 17593 df-imas 17594 df-xps 17596 df-mre 17670 df-mrc 17671 df-acs 17673 df-mgm 18730 df-sgrp 18821 df-mnd 18837 df-submnd 18892 df-mulg 19191 df-cntz 19444 df-cmn 19909 df-psmet 21577 df-xmet 21578 df-met 21579 df-bl 21580 df-mopn 21581 df-fbas 21582 df-fg 21583 df-cnfld 21586 df-top 23119 df-topon 23136 df-topsp 23158 df-bases 23171 df-cld 23244 df-ntr 23245 df-cls 23246 df-nei 23323 df-lp 23361 df-perf 23362 df-cn 23452 df-cnp 23453 df-haus 23540 df-cmp 23612 df-tx 23788 df-hmeo 23981 df-fil 24072 df-fm 24164 df-flim 24165 df-flf 24166 df-xms 24546 df-ms 24547 df-tms 24548 df-cncf 25106 df-ovol 25692 df-vol 25693 df-mbf 25847 df-itg1 25848 df-itg2 25849 df-ibl 25850 df-itg 25851 df-0p 25898 df-ditg 26074 df-limc 26093 df-dv 26094

This theorem is used by: fourierdlem108 47042

W3C validator