Metamath Proof Explorer

Theorem ftc1

Description: The Fundamental Theorem of Calculus, part one. The function formed by varying the right endpoint of an integral is differentiable at C with derivative F ( C ) if the original function is continuous at C . This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses ftc1.g 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1.a 
|- ( ph -> A e. RR )
ftc1.b 
|- ( ph -> B e. RR )
ftc1.le 
|- ( ph -> A <_ B )
ftc1.s 
|- ( ph -> ( A (,) B ) C_ D )
ftc1.d 
|- ( ph -> D C_ RR )
ftc1.i 
|- ( ph -> F e. L^1 )
ftc1.c 
|- ( ph -> C e. ( A (,) B ) )
ftc1.f 
|- ( ph -> F e. ( ( K CnP L ) ` C ) )
ftc1.j 
|- J = ( L |`t RR )
ftc1.k 
|- K = ( L |`t D )
ftc1.l 
|- L = ( TopOpen ` CCfld )
Assertion ftc1 
|- ( ph -> C ( RR _D G ) ( F ` C ) )

Proof

Step Hyp Ref Expression
1 ftc1.g 
 |-  G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2 ftc1.a 
 |-  ( ph -> A e. RR )
3 ftc1.b 
 |-  ( ph -> B e. RR )
4 ftc1.le 
 |-  ( ph -> A <_ B )
5 ftc1.s 
 |-  ( ph -> ( A (,) B ) C_ D )
6 ftc1.d 
 |-  ( ph -> D C_ RR )
7 ftc1.i 
 |-  ( ph -> F e. L^1 )
8 ftc1.c 
 |-  ( ph -> C e. ( A (,) B ) )
9 ftc1.f 
 |-  ( ph -> F e. ( ( K CnP L ) ` C ) )
10 ftc1.j 
 |-  J = ( L |`t RR )
11 ftc1.k 
 |-  K = ( L |`t D )
12 ftc1.l 
 |-  L = ( TopOpen ` CCfld )
13 12 tgioo2 
 |-  ( topGen ` ran (,) ) = ( L |`t RR )
14 10 13 eqtr4i 
 |-  J = ( topGen ` ran (,) )
15 retop 
 |-  ( topGen ` ran (,) ) e. Top
16 14 15 eqeltri 
 |-  J e. Top
17 16 a1i 
 |-  ( ph -> J e. Top )
18 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
19 2 3 18 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
20 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
21 20 14 eleqtrri 
 |-  ( A (,) B ) e. J
22 21 a1i 
 |-  ( ph -> ( A (,) B ) e. J )
23 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
24 23 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
25 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
26 14 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
27 25 26 eqtr4i 
 |-  RR = U. J
28 27 ssntr 
 |-  ( ( ( J e. Top /\ ( A [,] B ) C_ RR ) /\ ( ( A (,) B ) e. J /\ ( A (,) B ) C_ ( A [,] B ) ) ) -> ( A (,) B ) C_ ( ( int ` J ) ` ( A [,] B ) ) )
29 17 19 22 24 28 syl22anc 
 |-  ( ph -> ( A (,) B ) C_ ( ( int ` J ) ` ( A [,] B ) ) )
30 29 8 sseldd 
 |-  ( ph -> C e. ( ( int ` J ) ` ( A [,] B ) ) )
31 eqid 
 |-  ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) = ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 31 ftc1lem6 
 |-  ( ph -> ( F ` C ) e. ( ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) )
33 ax-resscn 
 |-  RR C_ CC
34 33 a1i 
 |-  ( ph -> RR C_ CC )
35 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 
 |-  ( ph -> F : D --> CC )
36 1 2 3 4 5 6 7 35 ftc1lem2 
 |-  ( ph -> G : ( A [,] B ) --> CC )
37 10 12 31 34 36 19 eldv 
 |-  ( ph -> ( C ( RR _D G ) ( F ` C ) <-> ( C e. ( ( int ` J ) ` ( A [,] B ) ) /\ ( F ` C ) e. ( ( z e. ( ( A [,] B ) \ { C } ) |-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) ) limCC C ) ) ) )
38 30 32 37 mpbir2and 
 |-  ( ph -> C ( RR _D G ) ( F ` C ) )