ftc2

Description: The Fundamental Theorem of Calculus, part two. If F is a function continuous on [ A , B ] and continuously differentiable on ( A , B ) , then the integral of the derivative of F is equal to F ( B ) - F ( A ) . This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014)

	Ref	Expression
Hypotheses	ftc2.a	\|- ( ph -> A e. RR )
	ftc2.b	\|- ( ph -> B e. RR )
	ftc2.le	\|- ( ph -> A <_ B )
	ftc2.c	\|- ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
	ftc2.i	\|- ( ph -> ( RR _D F ) e. L^1 )
	ftc2.f	\|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
Assertion	ftc2	\|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ftc2.a	\|- ( ph -> A e. RR )
2		ftc2.b	\|- ( ph -> B e. RR )
3		ftc2.le	\|- ( ph -> A <_ B )
4		ftc2.c	\|- ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
5		ftc2.i	\|- ( ph -> ( RR _D F ) e. L^1 )
6		ftc2.f	\|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
7	1	rexrd	\|- ( ph -> A e. RR* )
8	2	rexrd	\|- ( ph -> B e. RR* )
9		ubicc2	\|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
10	7 8 3 9	syl3anc	\|- ( ph -> B e. ( A [,] B ) )
11		fvex	\|- ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) e. _V
12	11	fvconst2	\|- ( B e. ( A [,] B ) -> ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) = ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) )
13	10 12	syl	\|- ( ph -> ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) = ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) )
14		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
15	14	subcn	\|- - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
16	15	a1i	\|- ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
17		eqid	\|- ( x e. ( A [,] B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) = ( x e. ( A [,] B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t )
18		ssidd	\|- ( ph -> ( A (,) B ) C_ ( A (,) B ) )
19		ioossre	\|- ( A (,) B ) C_ RR
20	19	a1i	\|- ( ph -> ( A (,) B ) C_ RR )
21		cncff	\|- ( ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) -> ( RR _D F ) : ( A (,) B ) --> CC )
22	4 21	syl	\|- ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
23	17 1 2 3 18 20 5 22	ftc1a	\|- ( ph -> ( x e. ( A [,] B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) e. ( ( A [,] B ) -cn-> CC ) )
24		cncff	\|- ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
25	6 24	syl	\|- ( ph -> F : ( A [,] B ) --> CC )
26	25	feqmptd	\|- ( ph -> F = ( x e. ( A [,] B ) \|-> ( F ` x ) ) )
27	26 6	eqeltrrd	\|- ( ph -> ( x e. ( A [,] B ) \|-> ( F ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
28	14 16 23 27	cncfmpt2f	\|- ( ph -> ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
29		ax-resscn	\|- RR C_ CC
30	29	a1i	\|- ( ph -> RR C_ CC )
31		iccssre	\|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
32	1 2 31	syl2anc	\|- ( ph -> ( A [,] B ) C_ RR )
33		fvex	\|- ( ( RR _D F ) ` t ) e. _V
34	33	a1i	\|- ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) x ) ) -> ( ( RR _D F ) ` t ) e. _V )
35	2	adantr	\|- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
36	35	rexrd	\|- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
37		elicc2	\|- ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
38	1 2 37	syl2anc	\|- ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
39	38	biimpa	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
40	39	simp3d	\|- ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
41		iooss2	\|- ( ( B e. RR* /\ x <_ B ) -> ( A (,) x ) C_ ( A (,) B ) )
42	36 40 41	syl2anc	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) C_ ( A (,) B ) )
43		ioombl	\|- ( A (,) x ) e. dom vol
44	43	a1i	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) e. dom vol )
45	33	a1i	\|- ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
46	22	feqmptd	\|- ( ph -> ( RR _D F ) = ( t e. ( A (,) B ) \|-> ( ( RR _D F ) ` t ) ) )
47	46 5	eqeltrrd	\|- ( ph -> ( t e. ( A (,) B ) \|-> ( ( RR _D F ) ` t ) ) e. L^1 )
48	47	adantr	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) B ) \|-> ( ( RR _D F ) ` t ) ) e. L^1 )
49	42 44 45 48	iblss	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) x ) \|-> ( ( RR _D F ) ` t ) ) e. L^1 )
50	34 49	itgcl	\|- ( ( ph /\ x e. ( A [,] B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
51	25	ffvelcdmda	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
52	50 51	subcld	\|- ( ( ph /\ x e. ( A [,] B ) ) -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) e. CC )
53		tgioo4	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
54		iccntr	\|- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
55	1 2 54	syl2anc	\|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
56	30 32 52 53 14 55	dvmptntr	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( RR _D ( x e. ( A (,) B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) )
57		reelprrecn	\|- RR e. { RR , CC }
58	57	a1i	\|- ( ph -> RR e. { RR , CC } )
59		ioossicc	\|- ( A (,) B ) C_ ( A [,] B )
60	59	sseli	\|- ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
61	60 50	sylan2	\|- ( ( ph /\ x e. ( A (,) B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
62	22	ffvelcdmda	\|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
63	17 1 2 3 4 5	ftc1cn	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( RR _D F ) )
64	30 32 50 53 14 55	dvmptntr	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( RR _D ( x e. ( A (,) B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) )
65	22	feqmptd	\|- ( ph -> ( RR _D F ) = ( x e. ( A (,) B ) \|-> ( ( RR _D F ) ` x ) ) )
66	63 64 65	3eqtr3d	\|- ( ph -> ( RR _D ( x e. ( A (,) B ) \|-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( x e. ( A (,) B ) \|-> ( ( RR _D F ) ` x ) ) )
67	60 51	sylan2	\|- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
68	30 32 51 53 14 55	dvmptntr	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> ( F ` x ) ) ) = ( RR _D ( x e. ( A (,) B ) \|-> ( F ` x ) ) ) )
69	26	oveq2d	\|- ( ph -> ( RR _D F ) = ( RR _D ( x e. ( A [,] B ) \|-> ( F ` x ) ) ) )
70	69 65	eqtr3d	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> ( F ` x ) ) ) = ( x e. ( A (,) B ) \|-> ( ( RR _D F ) ` x ) ) )
71	68 70	eqtr3d	\|- ( ph -> ( RR _D ( x e. ( A (,) B ) \|-> ( F ` x ) ) ) = ( x e. ( A (,) B ) \|-> ( ( RR _D F ) ` x ) ) )
72	58 61 62 66 67 62 71	dvmptsub	\|- ( ph -> ( RR _D ( x e. ( A (,) B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( x e. ( A (,) B ) \|-> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) ) )
73	62	subidd	\|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) = 0 )
74	73	mpteq2dva	\|- ( ph -> ( x e. ( A (,) B ) \|-> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) \|-> 0 ) )
75	56 72 74	3eqtrd	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( x e. ( A (,) B ) \|-> 0 ) )
76		fconstmpt	\|- ( ( A (,) B ) X. { 0 } ) = ( x e. ( A (,) B ) \|-> 0 )
77	75 76	eqtr4di	\|- ( ph -> ( RR _D ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( ( A (,) B ) X. { 0 } ) )
78	1 2 28 77	dveq0	\|- ( ph -> ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) = ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) )
79	78	fveq1d	\|- ( ph -> ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` B ) = ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) )
80		oveq2	\|- ( x = B -> ( A (,) x ) = ( A (,) B ) )
81		itgeq1	\|- ( ( A (,) x ) = ( A (,) B ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
82	80 81	syl	\|- ( x = B -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
83		fveq2	\|- ( x = B -> ( F ` x ) = ( F ` B ) )
84	82 83	oveq12d	\|- ( x = B -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
85		eqid	\|- ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) = ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) )
86		ovex	\|- ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) e. _V
87	84 85 86	fvmpt	\|- ( B e. ( A [,] B ) -> ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` B ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
88	10 87	syl	\|- ( ph -> ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` B ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
89	79 88	eqtr3d	\|- ( ph -> ( ( ( A [,] B ) X. { ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) } ) ` B ) = ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) )
90		lbicc2	\|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
91	7 8 3 90	syl3anc	\|- ( ph -> A e. ( A [,] B ) )
92		oveq2	\|- ( x = A -> ( A (,) x ) = ( A (,) A ) )
93		iooid	\|- ( A (,) A ) = (/)
94	92 93	eqtrdi	\|- ( x = A -> ( A (,) x ) = (/) )
95		itgeq1	\|- ( ( A (,) x ) = (/) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
96	94 95	syl	\|- ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
97		itg0	\|- S. (/) ( ( RR _D F ) ` t ) _d t = 0
98	96 97	eqtrdi	\|- ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = 0 )
99		fveq2	\|- ( x = A -> ( F ` x ) = ( F ` A ) )
100	98 99	oveq12d	\|- ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = ( 0 - ( F ` A ) ) )
101		df-neg	\|- -u ( F ` A ) = ( 0 - ( F ` A ) )
102	100 101	eqtr4di	\|- ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = -u ( F ` A ) )
103		negex	\|- -u ( F ` A ) e. _V
104	102 85 103	fvmpt	\|- ( A e. ( A [,] B ) -> ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
105	91 104	syl	\|- ( ph -> ( ( x e. ( A [,] B ) \|-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
106	13 89 105	3eqtr3d	\|- ( ph -> ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) = -u ( F ` A ) )
107	106	oveq2d	\|- ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = ( ( F ` B ) + -u ( F ` A ) ) )
108	25 10	ffvelcdmd	\|- ( ph -> ( F ` B ) e. CC )
109	33	a1i	\|- ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
110	109 47	itgcl	\|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t e. CC )
111	108 110	pncan3d	\|- ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
112	25 91	ffvelcdmd	\|- ( ph -> ( F ` A ) e. CC )
113	108 112	negsubd	\|- ( ph -> ( ( F ` B ) + -u ( F ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
114	107 111 113	3eqtr3d	\|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )

Metamath Proof Explorer

Theorem ftc2

Proof