Theorem ftc1lem1

Description: Lemma for ftc1a and ftc1 . (Contributed by Mario Carneiro, 31-Aug-2014)

	Ref	Expression
Hypotheses	ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
	ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1a.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
	ftc1lem1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
	ftc1lem1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
Assertion	ftc1lem1	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2		ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6		ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7		ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8		ftc1a.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
9		ftc1lem1.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
10		ftc1lem1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
11		oveq2	⊢ ( 𝑥 = 𝑌 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑌 ) )
12		itgeq1	⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑌 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
13	11 12	syl	⊢ ( 𝑥 = 𝑌 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
14		itgex	⊢ ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ V
15	13 1 14	fvmpt	⊢ ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺 ‘ 𝑌 ) = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
16	10 15	syl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐺 ‘ 𝑌 ) = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
18	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝐴 ∈ ℝ )
19		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20	2 3 19	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
21	20 10	sseldd	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ℝ )
23	20 9	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ℝ )
25		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
26	2 3 25	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
27	9 26	mpbid	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
28	27	simp2d	⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝐴 ≤ 𝑋 )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
31		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝑌 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) )
32	2 21 31	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝑌 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∈ ( 𝐴 [,] 𝑌 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) )
34	24 29 30 33	mpbir3and	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝐴 [,] 𝑌 ) )
35	3	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
36		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
37	2 3 36	syl2anc	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
38	10 37	mpbid	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) )
39	38	simp3d	⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
40		iooss2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑌 ≤ 𝐵 ) → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
41	35 39 40	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
42	41 5	sstrd	⊢ ( 𝜑 → ( 𝐴 (,) 𝑌 ) ⊆ 𝐷 )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐴 (,) 𝑌 ) ⊆ 𝐷 )
44	43	sselda	⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑌 ) ) → 𝑡 ∈ 𝐷 )
45	8	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
46	45	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
47	44 46	syldan	⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
48	27	simp3d	⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
49		iooss2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
50	35 48 49	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
51	50 5	sstrd	⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ⊆ 𝐷 )
52		ioombl	⊢ ( 𝐴 (,) 𝑋 ) ∈ dom vol
53	52	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ∈ dom vol )
54		fvexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
55	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
56	55 7	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
57	51 53 54 56	iblss	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
58	57	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
59	2	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
60		iooss1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
61	59 28 60	syl2anc	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
62	61 41	sstrd	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
63	62 5	sstrd	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ 𝐷 )
64		ioombl	⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
65	64	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
66	63 65 54 56	iblss	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
67	66	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
68	18 22 34 47 58 67	itgsplitioo	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
69	17 68	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐺 ‘ 𝑌 ) = ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
70		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑋 ) )
71		itgeq1	⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑋 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
72	70 71	syl	⊢ ( 𝑥 = 𝑋 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
73		itgex	⊢ ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ V
74	72 1 73	fvmpt	⊢ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺 ‘ 𝑋 ) = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
75	9 74	syl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐺 ‘ 𝑋 ) = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
77	69 76	oveq12d	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
78		fvexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
79	78 57	itgcl	⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ )
80	63	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ 𝐷 )
81	80 45	syldan	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
82	81 66	itgcl	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ )
83	79 82	pncan2d	⊢ ( 𝜑 → ( ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
84	83	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
85	77 84	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )