Metamath Proof Explorer


Theorem dvmptresicc

Description: Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptresicc.f F = x A
dvmptresicc.a φ x A
dvmptresicc.fdv φ D F = x B
dvmptresicc.b φ x B
dvmptresicc.c φ C
dvmptresicc.d φ D
Assertion dvmptresicc φ dx C D A d x = x C D B

Proof

Step Hyp Ref Expression
1 dvmptresicc.f F = x A
2 dvmptresicc.a φ x A
3 dvmptresicc.fdv φ D F = x B
4 dvmptresicc.b φ x B
5 dvmptresicc.c φ C
6 dvmptresicc.d φ D
7 1 reseq1i F C D = x A C D
8 5 6 iccssred φ C D
9 ax-resscn
10 9 a1i φ
11 8 10 sstrd φ C D
12 11 resmptd φ x A C D = x C D A
13 7 12 eqtrid φ F C D = x C D A
14 13 oveq2d φ D F C D = dx C D A d x
15 8 resabs1d φ F C D = F C D
16 15 eqcomd φ F C D = F C D
17 16 oveq2d φ D F C D = D F C D
18 2 1 fmptd φ F :
19 18 10 fssresd φ F :
20 ssidd φ
21 eqid TopOpen fld = TopOpen fld
22 21 tgioo2 topGen ran . = TopOpen fld 𝑡
23 21 22 dvres F : C D D F C D = F int topGen ran . C D
24 10 19 20 8 23 syl22anc φ D F C D = F int topGen ran . C D
25 reelprrecn
26 25 a1i φ
27 ssidd φ
28 3 dmeqd φ dom F = dom x B
29 4 ralrimiva φ x B
30 dmmptg x B dom x B =
31 29 30 syl φ dom x B =
32 28 31 eqtr2d φ = dom F
33 10 32 sseqtrd φ dom F
34 dvres3 F : dom F D F = F
35 26 18 27 33 34 syl22anc φ D F = F
36 iccntr C D int topGen ran . C D = C D
37 5 6 36 syl2anc φ int topGen ran . C D = C D
38 35 37 reseq12d φ F int topGen ran . C D = F C D
39 ioossre C D
40 resabs1 C D F C D = F C D
41 39 40 mp1i φ F C D = F C D
42 3 reseq1d φ F C D = x B C D
43 ioosscn C D
44 resmpt C D x B C D = x C D B
45 43 44 mp1i φ x B C D = x C D B
46 42 45 eqtrd φ F C D = x C D B
47 38 41 46 3eqtrd φ F int topGen ran . C D = x C D B
48 17 24 47 3eqtrd φ D F C D = x C D B
49 14 48 eqtr3d φ dx C D A d x = x C D B