Theorem ftc2nc

Description: Choice-free proof of ftc2 . (Contributed by Brendan Leahy, 19-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		ftc2nc.a	|- ( ph -> A e. RR )
2		ftc2nc.b	|- ( ph -> B e. RR )
3		ftc2nc.le	|- ( ph -> A <_ B )
4		ftc2nc.c	|- ( ph -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
5		ftc2nc.i	|- ( ph -> ( RR _D F ) e. L^1 )
6		ftc2nc.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		ioof	|- (,) : ( RR* X. RR* ) --> ~P RR
24		ffun	|- ( (,) : ( RR* X. RR* ) --> ~P RR -> Fun (,) )
25	23 24	ax-mp	|- Fun (,)
26		fvelima	|- ( ( Fun (,) /\ s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ) -> E. x e. ( ( A [,] B ) X. ( A [,] B ) ) ( (,) ` x ) = s )
27	25 26	mpan	|- ( s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) -> E. x e. ( ( A [,] B ) X. ( A [,] B ) ) ( (,) ` x ) = s )
28		1st2nd2	|- ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
29	28	fveq2d	|- ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( (,) ` x ) = ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
30		df-ov	|- ( ( 1st ` x ) (,) ( 2nd ` x ) ) = ( (,) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
31	29 30	eqtr4di	|- ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( (,) ` x ) = ( ( 1st ` x ) (,) ( 2nd ` x ) ) )
32	31	eqeq1d	|- ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( ( (,) ` x ) = s <-> ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s ) )
33	32	adantl	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( (,) ` x ) = s <-> ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s ) )
34	7 8	jca	|- ( ph -> ( A e. RR* /\ B e. RR* ) )
35	34	adantr	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( A e. RR* /\ B e. RR* ) )
36		xp1st	|- ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( 1st ` x ) e. ( A [,] B ) )
37		elicc1	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( 1st ` x ) e. ( A [,] B ) <-> ( ( 1st ` x ) e. RR* /\ A <_ ( 1st ` x ) /\ ( 1st ` x ) <_ B ) ) )
38	7 8 37	syl2anc	|- ( ph -> ( ( 1st ` x ) e. ( A [,] B ) <-> ( ( 1st ` x ) e. RR* /\ A <_ ( 1st ` x ) /\ ( 1st ` x ) <_ B ) ) )
39	38	biimpa	|- ( ( ph /\ ( 1st ` x ) e. ( A [,] B ) ) -> ( ( 1st ` x ) e. RR* /\ A <_ ( 1st ` x ) /\ ( 1st ` x ) <_ B ) )
40	39	simp2d	|- ( ( ph /\ ( 1st ` x ) e. ( A [,] B ) ) -> A <_ ( 1st ` x ) )
41	36 40	sylan2	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> A <_ ( 1st ` x ) )
42		xp2nd	|- ( x e. ( ( A [,] B ) X. ( A [,] B ) ) -> ( 2nd ` x ) e. ( A [,] B ) )
43		iccleub	|- ( ( A e. RR* /\ B e. RR* /\ ( 2nd ` x ) e. ( A [,] B ) ) -> ( 2nd ` x ) <_ B )
44	43	3expa	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( 2nd ` x ) e. ( A [,] B ) ) -> ( 2nd ` x ) <_ B )
45	34 42 44	syl2an	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( 2nd ` x ) <_ B )
46		ioossioo	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ ( 1st ` x ) /\ ( 2nd ` x ) <_ B ) ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ ( A (,) B ) )
47	35 41 45 46	syl12anc	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ ( A (,) B ) )
48	47	sselda	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> t e. ( A (,) B ) )
49	22	ffvelcdmda	|- ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. CC )
50	49	adantlr	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. CC )
51	48 50	syldan	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> ( ( RR _D F ) ` t ) e. CC )
52		ioombl	|- ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol
53	52	a1i	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol )
54		fvexd	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
55	22	feqmptd	|- ( ph -> ( RR _D F ) = ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) )
56	55 5	eqeltrrd	|- ( ph -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
57	56	adantr	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
58	47 53 54 57	iblss	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
59		ax-resscn	|- RR C_ CC
60		ssid	|- CC C_ CC
61		cncfss	|- ( ( RR C_ CC /\ CC C_ CC ) -> ( CC -cn-> RR ) C_ ( CC -cn-> CC ) )
62	59 60 61	mp2an	|- ( CC -cn-> RR ) C_ ( CC -cn-> CC )
63		abscncf	|- abs e. ( CC -cn-> RR )
64	62 63	sselii	|- abs e. ( CC -cn-> CC )
65	64	a1i	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> abs e. ( CC -cn-> CC ) )
66	55	reseq1d	|- ( ph -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) )
67	66	adantr	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) )
68	47	resmptd	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) )
69	67 68	eqtrd	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) = ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) )
70	4	adantr	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) )
71		rescncf	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ ( A (,) B ) -> ( ( RR _D F ) e. ( ( A (,) B ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) ) )
72	47 70 71	sylc	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( RR _D F ) |` ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
73	69 72	eqeltrrd	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
74	65 73	cncfmpt1f	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
75		cnmbf	|- ( ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol /\ ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. MblFn )
76	52 74 75	sylancr	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. MblFn )
77	51 58	itgcl	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t e. CC )
78	77	cjcld	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) e. CC )
79		ioossre	|- ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ RR
80	79 59	sstri	|- ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ CC
81		cncfmptc	|- ( ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) e. CC /\ ( ( 1st ` x ) (,) ( 2nd ` x ) ) C_ CC /\ CC C_ CC ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
82	80 60 81	mp3an23	|- ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) e. CC -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
83	78 82	syl	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
84		nfcv	|- F/_ s ( ( RR _D F ) ` t )
85		nfcsb1v	|- F/_ t [_ s / t ]_ ( ( RR _D F ) ` t )
86		csbeq1a	|- ( t = s -> ( ( RR _D F ) ` t ) = [_ s / t ]_ ( ( RR _D F ) ` t ) )
87	84 85 86	cbvmpt	|- ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( RR _D F ) ` t ) ) = ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> [_ s / t ]_ ( ( RR _D F ) ` t ) )
88	87 73	eqeltrrid	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> [_ s / t ]_ ( ( RR _D F ) ` t ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
89	83 88	mulcncf	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) )
90		cnmbf	|- ( ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) e. dom vol /\ ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) -cn-> CC ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. MblFn )
91	52 89 90	sylancr	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( s e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( ( * ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) x. [_ s / t ]_ ( ( RR _D F ) ` t ) ) ) e. MblFn )
92	51 58 76 91	itgabsnc	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) <_ S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( abs ` ( ( RR _D F ) ` t ) ) _d t )
93	51	abscld	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) e. RR )
94		fvexd	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> ( ( RR _D F ) ` t ) e. _V )
95	94 58 76	iblabsnc	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) |-> ( abs ` ( ( RR _D F ) ` t ) ) ) e. L^1 )
96	51	absge0d	|- ( ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) /\ t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ) -> 0 <_ ( abs ` ( ( RR _D F ) ` t ) ) )
97	93 95 96	itgposval	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( abs ` ( ( RR _D F ) ` t ) ) _d t = ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
98	92 97	breqtrd	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
99		itgeq1	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t = S. s ( ( RR _D F ) ` t ) _d t )
100	99	fveq2d	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) = ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) )
101		eleq2	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) <-> t e. s ) )
102	101	ifbid	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) = if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) )
103	102	mpteq2dv	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) = ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) )
104	103	fveq2d	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
105	100 104	breq12d	|- ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( ( abs ` S. ( ( 1st ` x ) (,) ( 2nd ` x ) ) ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. ( ( 1st ` x ) (,) ( 2nd ` x ) ) , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) <-> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
106	98 105	syl5ibcom	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( ( 1st ` x ) (,) ( 2nd ` x ) ) = s -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
107	33 106	sylbid	|- ( ( ph /\ x e. ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( ( (,) ` x ) = s -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
108	107	rexlimdva	|- ( ph -> ( E. x e. ( ( A [,] B ) X. ( A [,] B ) ) ( (,) ` x ) = s -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
109	27 108	syl5	|- ( ph -> ( s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) -> ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) ) )
110	109	ralrimiv	|- ( ph -> A. s e. ( (,) " ( ( A [,] B ) X. ( A [,] B ) ) ) ( abs ` S. s ( ( RR _D F ) ` t ) _d t ) <_ ( S.2 ` ( t e. RR |-> if ( t e. s , ( abs ` ( ( RR _D F ) ` t ) ) , 0 ) ) ) )
111	17 1 2 3 18 20 5 22 110	ftc1anc	|- ( ph -> ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) e. ( ( A [,] B ) -cn-> CC ) )
112		cncff	|- ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
113	6 112	syl	|- ( ph -> F : ( A [,] B ) --> CC )
114	113	feqmptd	|- ( ph -> F = ( x e. ( A [,] B ) |-> ( F ` x ) ) )
115	114 6	eqeltrrd	|- ( ph -> ( x e. ( A [,] B ) |-> ( F ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
116	14 16 111 115	cncfmpt2f	|- ( ph -> ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
117	59	a1i	|- ( ph -> RR C_ CC )
118		iccssre	|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
119	1 2 118	syl2anc	|- ( ph -> ( A [,] B ) C_ RR )
120		fvexd	|- ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) x ) ) -> ( ( RR _D F ) ` t ) e. _V )
121	2	adantr	|- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
122	121	rexrd	|- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
123		elicc2	|- ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
124	1 2 123	syl2anc	|- ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
125	124	biimpa	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
126	125	simp3d	|- ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
127		iooss2	|- ( ( B e. RR* /\ x <_ B ) -> ( A (,) x ) C_ ( A (,) B ) )
128	122 126 127	syl2anc	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) C_ ( A (,) B ) )
129		ioombl	|- ( A (,) x ) e. dom vol
130	129	a1i	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( A (,) x ) e. dom vol )
131		fvexd	|- ( ( ( ph /\ x e. ( A [,] B ) ) /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
132	56	adantr	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) B ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
133	128 130 131 132	iblss	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( t e. ( A (,) x ) |-> ( ( RR _D F ) ` t ) ) e. L^1 )
134	120 133	itgcl	|- ( ( ph /\ x e. ( A [,] B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
135	113	ffvelcdmda	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
136	134 135	subcld	|- ( ( ph /\ x e. ( A [,] B ) ) -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) e. CC )
137		tgioo4	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
138		iccntr	|- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
139	1 2 138	syl2anc	|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
140	117 119 136 137 14 139	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 ) ) ) ) )
141		reelprrecn	|- RR e. { RR , CC }
142	141	a1i	|- ( ph -> RR e. { RR , CC } )
143		ioossicc	|- ( A (,) B ) C_ ( A [,] B )
144	143	sseli	|- ( x e. ( A (,) B ) -> x e. ( A [,] B ) )
145	144 134	sylan2	|- ( ( ph /\ x e. ( A (,) B ) ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t e. CC )
146	22	ffvelcdmda	|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
147	17 1 2 3 4 5	ftc1cnnc	|- ( ph -> ( RR _D ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t ) ) = ( RR _D F ) )
148	117 119 134 137 14 139	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 ) ) )
149	22	feqmptd	|- ( ph -> ( RR _D F ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
150	147 148 149	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 ) ) )
151	144 135	sylan2	|- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
152	114	oveq2d	|- ( ph -> ( RR _D F ) = ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) )
153	117 119 135 137 14 139	dvmptntr	|- ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( F ` x ) ) ) = ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) )
154	152 149 153	3eqtr3rd	|- ( ph -> ( RR _D ( x e. ( A (,) B ) |-> ( F ` x ) ) ) = ( x e. ( A (,) B ) |-> ( ( RR _D F ) ` x ) ) )
155	142 145 146 150 151 146 154	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 ) ) ) )
156	146	subidd	|- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) = 0 )
157	156	mpteq2dva	|- ( ph -> ( x e. ( A (,) B ) |-> ( ( ( RR _D F ) ` x ) - ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> 0 ) )
158	140 155 157	3eqtrd	|- ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( x e. ( A (,) B ) |-> 0 ) )
159		fconstmpt	|- ( ( A (,) B ) X. { 0 } ) = ( x e. ( A (,) B ) |-> 0 )
160	158 159	eqtr4di	|- ( ph -> ( RR _D ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ) = ( ( A (,) B ) X. { 0 } ) )
161	1 2 116 160	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 ) } ) )
162	161	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 ) )
163		oveq2	|- ( x = B -> ( A (,) x ) = ( A (,) B ) )
164		itgeq1	|- ( ( A (,) x ) = ( A (,) B ) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
165	163 164	syl	|- ( x = B -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
166		fveq2	|- ( x = B -> ( F ` x ) = ( F ` B ) )
167	165 166	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 ) ) )
168		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 ) ) )
169		ovex	|- ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) e. _V
170	167 168 169	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 ) ) )
171	10 170	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 ) ) )
172	162 171	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 ) ) )
173		lbicc2	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
174	7 8 3 173	syl3anc	|- ( ph -> A e. ( A [,] B ) )
175		oveq2	|- ( x = A -> ( A (,) x ) = ( A (,) A ) )
176		iooid	|- ( A (,) A ) = (/)
177	175 176	eqtrdi	|- ( x = A -> ( A (,) x ) = (/) )
178		itgeq1	|- ( ( A (,) x ) = (/) -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
179	177 178	syl	|- ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = S. (/) ( ( RR _D F ) ` t ) _d t )
180		itg0	|- S. (/) ( ( RR _D F ) ` t ) _d t = 0
181	179 180	eqtrdi	|- ( x = A -> S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t = 0 )
182		fveq2	|- ( x = A -> ( F ` x ) = ( F ` A ) )
183	181 182	oveq12d	|- ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = ( 0 - ( F ` A ) ) )
184		df-neg	|- -u ( F ` A ) = ( 0 - ( F ` A ) )
185	183 184	eqtr4di	|- ( x = A -> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) = -u ( F ` A ) )
186		negex	|- -u ( F ` A ) e. _V
187	185 168 186	fvmpt	|- ( A e. ( A [,] B ) -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
188	174 187	syl	|- ( ph -> ( ( x e. ( A [,] B ) |-> ( S. ( A (,) x ) ( ( RR _D F ) ` t ) _d t - ( F ` x ) ) ) ` A ) = -u ( F ` A ) )
189	13 172 188	3eqtr3d	|- ( ph -> ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) = -u ( F ` A ) )
190	189	oveq2d	|- ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = ( ( F ` B ) + -u ( F ` A ) ) )
191	113 10	ffvelcdmd	|- ( ph -> ( F ` B ) e. CC )
192		fvexd	|- ( ( ph /\ t e. ( A (,) B ) ) -> ( ( RR _D F ) ` t ) e. _V )
193	192 56	itgcl	|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t e. CC )
194	191 193	pncan3d	|- ( ph -> ( ( F ` B ) + ( S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t - ( F ` B ) ) ) = S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t )
195	113 174	ffvelcdmd	|- ( ph -> ( F ` A ) e. CC )
196	191 195	negsubd	|- ( ph -> ( ( F ` B ) + -u ( F ` A ) ) = ( ( F ` B ) - ( F ` A ) ) )
197	190 194 196	3eqtr3d	|- ( ph -> S. ( A (,) B ) ( ( RR _D F ) ` t ) _d t = ( ( F ` B ) - ( F ` A ) ) )