Theorem itgioocnicc 46515

Description: The integral of a piecewise continuous function 𝐹 on an open interval is equal to the integral of the continuous function 𝐺, in the corresponding closed interval. 𝐺 is equal to 𝐹 on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
itgioocnicc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
itgioocnicc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
itgioocnicc.f	⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
itgioocnicc.fcn	⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
itgioocnicc.fdom	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)
itgioocnicc.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴))
itgioocnicc.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵))
itgioocnicc.g	⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))

Assertion

Ref	Expression
itgioocnicc	⊢ (𝜑 → (𝐺 ∈ 𝐿1 ∧ ∫(𝐴[,]𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐿   𝑥,𝑅   𝜑,𝑥

Allowed substitution hint:   𝐺(𝑥)

Proof of Theorem itgioocnicc

Step	Hyp	Ref	Expression
1		itgioocnicc.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		itgioocnicc.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		itgioocnicc.g	. . . . 5 ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))
4		iftrue 4485	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅)
5		iftrue 4485	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = 𝑅)
6	4, 5	eqtr4d 2799	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
7	6	adantl 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
8		iftrue 4485	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = 𝐿)
9		iftrue 4485	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = 𝐿)
10	8, 9	eqtr4d 2799	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
11	10	adantl 485	. . . . . . . . . 10 ⊢ ((¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
12	11	ifeq2d 4500	. . . . . . . . 9 ⊢ ((¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
13	12	adantll 724	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
14		iffalse 4488	. . . . . . . . . 10 ⊢ (¬ 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))
15	14	ad2antlr 737	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))
16		iffalse 4488	. . . . . . . . . 10 ⊢ (¬ 𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥))
17	16	adantl 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥))
18		iffalse 4488	. . . . . . . . . . 11 ⊢ (¬ 𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
19	18	ad2antlr 737	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))) = if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))
20		iffalse 4488	. . . . . . . . . . 11 ⊢ (¬ 𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
21	20	adantl 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
22	1	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
23	22	rexrd 11229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
24	23	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈ ℝ*)
25	2	rexrd 11229	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
26	25	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ*)
27	2	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
28		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
29		eliccre 46045	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
30	22, 27, 28, 29	syl3anc 1389	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
31	30	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ)
32	1	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 ∈ ℝ)
33	30	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ ℝ)
34	25	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ*)
35		iccgelb 13403	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
36	23, 34, 28, 35	syl3anc 1389	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
37	36	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 ≤ 𝑥)
38		neqne 2964	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝐴 → 𝑥 ≠ 𝐴)
39	38	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ≠ 𝐴)
40	32, 33, 37, 39	leneltd 11334	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → 𝐴 < 𝑥)
41	40	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 < 𝑥)
42	30	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ)
43	2	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ)
44		iccleub 13402	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
45	23, 34, 28, 44	syl3anc 1389	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
46	45	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ≤ 𝐵)
47		eqcom 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝐵 ↔ 𝐵 = 𝑥)
48	47	notbii 322	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑥 = 𝐵 ↔ ¬ 𝐵 = 𝑥)
49	48	biimpi 218	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝐵 → ¬ 𝐵 = 𝑥)
50	49	neqned 2963	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝐵 → 𝐵 ≠ 𝑥)
51	50	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ≠ 𝑥)
52	42, 43, 46, 51	leneltd 11334	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐵)
53	52	adantlr 725	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐵)
54	24, 26, 31, 41, 53	eliood 46038	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵))
55		fvres 6882	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥))
56	54, 55	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥))
57	19, 21, 56	3eqtrrd 2801	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
58	15, 17, 57	3eqtrd 2800	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
59	13, 58	pm2.61dan 822	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
60	7, 59	pm2.61dan 822	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
61	60	mpteq2dva 5192	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))))
62	3, 61	eqtrid 2808	. . . 4 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))))
63		nfv 1933	. . . . 5 ⊢ Ⅎ𝑥𝜑
64		eqid 2761	. . . . 5 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))))
65		itgioocnicc.fcn	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
66		itgioocnicc.l	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵))
67		itgioocnicc.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴))
68	63, 64, 1, 2, 65, 66, 67	cncfiooicc 46432	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
69	62, 68	eqeltrd 2861	. . 3 ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
70		cniccibl 25883	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐺 ∈ 𝐿1)
71	1, 2, 69, 70	syl3anc 1389	. 2 ⊢ (𝜑 → 𝐺 ∈ 𝐿1)
72	4	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅)
73		limccl 25917	. . . . . . . . . . 11 ⊢ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐴) ⊆ ℂ
74	73, 67	sselid 3934	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ ℂ)
75	74	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → 𝑅 ∈ ℂ)
76	72, 75	eqeltrd 2861	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ)
77	14, 8	sylan9eq 2816	. . . . . . . . . . 11 ⊢ ((¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝐿)
78	77	adantll 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝐿)
79		limccl 25917	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) ⊆ ℂ
80	79, 66	sselid 3934	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ ℂ)
81	80	ad3antrrr 740	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ)
82	78, 81	eqeltrd 2861	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ)
83	14, 16	sylan9eq 2816	. . . . . . . . . . 11 ⊢ ((¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = (𝐹‘𝑥))
84	83	adantll 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = (𝐹‘𝑥))
85	56	eqcomd 2767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) = ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥))
86		cncff 24935	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝐹 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
87	65, 86	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
88	87	ad3antrrr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ)
89	88, 54	ffvelcdmd 7062	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐹 ↾ (𝐴(,)𝐵))‘𝑥) ∈ ℂ)
90	85, 89	eqeltrd 2861	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) ∈ ℂ)
91	84, 90	eqeltrd 2861	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ)
92	82, 91	pm2.61dan 822	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ)
93	76, 92	pm2.61dan 822	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ)
94	3	fvmpt2 6983	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))
95	28, 93, 94	syl2anc 593	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))
96	95, 93	eqeltrd 2861	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑥) ∈ ℂ)
97	1, 2, 96	itgioo 25858	. . . 4 ⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐺‘𝑥) d𝑥)
98	97	eqcomd 2767	. . 3 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)(𝐺‘𝑥) d𝑥)
99		ioossicc 13434	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
100	99	sseli 3932	. . . . . 6 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵))
101	100, 95	sylan2 602	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))))
102	1	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
103		eliooord 13406	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))
104	103	simpld 498	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑥)
105	104	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑥)
106	102, 105	gtned 11315	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 𝐴)
107	106	neneqd 2961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴)
108	107, 14	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))
109	100, 30	sylan2 602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ)
110	103	simprd 499	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 < 𝐵)
111	110	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 < 𝐵)
112	109, 111	ltned 11316	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 𝐵)
113	112	neneqd 2961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐵)
114	113, 16	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥))
115	101, 108, 114	3eqtrd 2800	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) = (𝐹‘𝑥))
116	115	itgeq2dv 25824	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴(,)𝐵)(𝐹‘𝑥) d𝑥)
117		itgioocnicc.f	. . . . . 6 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
118	117	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹:dom 𝐹⟶ℂ)
119		itgioocnicc.fdom	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom 𝐹)
120	119	sselda 3936	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ dom 𝐹)
121	118, 120	ffvelcdmd 7062	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
122	1, 2, 121	itgioo 25858	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
123	98, 116, 122	3eqtrd 2800	. 2 ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
124	71, 123	jca 519	1 ⊢ (𝜑 → (𝐺 ∈ 𝐿1 ∧ ∫(𝐴[,]𝐵)(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ≠ wne 2956   ⊆ wss 3904  ifcif 4479   class class class wbr 5099   ↦ cmpt 5180  dom cdm 5645   ↾ cres 5647  ⟶wf 6513  ‘cfv 6517  (class class class)co 7392  ℂcc 11068  ℝcr 11069  ℝ^*cxr 11212   < clt 11213   ≤ cle 11214  (,)cioo 13346  [,]cicc 13349  –cn→ccncf 24918  𝐿¹cibl 25659  ∫citg 25660   lim_ℂ climc 25904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-inf2 9593  ax-cc 10389  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147  ax-pre-sup 11148  ax-addf 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-symdif 4205  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-iin 4951  df-disj 5067  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-se 5599  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-isom 6526  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-of 7656  df-ofr 7657  df-om 7843  df-1st 7966  df-2nd 7967  df-supp 8136  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-2o 8433  df-oadd 8436  df-omul 8437  df-er 8673  df-map 8805  df-pm 8806  df-ixp 8876  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-fsupp 9305  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9455  df-dju 9856  df-card 9894  df-acn 9897  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-div 11842  df-nn 12208  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12479  df-z 12566  df-dec 12686  df-uz 12837  df-q 12947  df-rp 12991  df-xneg 13111  df-xadd 13112  df-xmul 13113  df-ioo 13350  df-ioc 13351  df-ico 13352  df-icc 13353  df-fz 13510  df-fzo 13657  df-fl 13799  df-mod 13877  df-seq 14012  df-exp 14072  df-hash 14341  df-cj 15109  df-re 15110  df-im 15111  df-sqrt 15245  df-abs 15246  df-limsup 15481  df-clim 15498  df-rlim 15499  df-sum 15697  df-struct 17166  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17250  df-plusg 17282  df-mulr 17283  df-starv 17284  df-sca 17285  df-vsca 17286  df-ip 17287  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-hom 17293  df-cco 17294  df-rest 17434  df-topn 17435  df-0g 17453  df-gsum 17454  df-topgen 17455  df-pt 17456  df-prds 17459  df-xrs 17515  df-qtop 17520  df-imas 17521  df-xps 17523  df-mre 17597  df-mrc 17598  df-acs 17600  df-mgm 18657  df-sgrp 18736  df-mnd 18752  df-submnd 18801  df-mulg 19093  df-cntz 19340  df-cmn 19805  df-psmet 21396  df-xmet 21397  df-met 21398  df-bl 21399  df-mopn 21400  df-cnfld 21405  df-top 22934  df-topon 22951  df-topsp 22973  df-bases 22986  df-cld 23059  df-ntr 23060  df-cls 23061  df-cn 23267  df-cnp 23268  df-cmp 23427  df-tx 23602  df-hmeo 23795  df-xms 24360  df-ms 24361  df-tms 24362  df-cncf 24920  df-ovol 25506  df-vol 25507  df-mbf 25661  df-itg1 25662  df-itg2 25663  df-ibl 25664  df-itg 25665  df-0p 25712  df-limc 25908

This theorem is referenced by:  fourierdlem81  46725