Metamath Proof Explorer

Theorem dveq0

Description: If a continuous function has zero derivative at all points on the interior of a closed interval, then it must be a constant function. (Contributed by Mario Carneiro, 2-Sep-2014) (Proof shortened by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses dveq0.a 
|- ( ph -> A e. RR )
dveq0.b 
|- ( ph -> B e. RR )
dveq0.c 
|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
dveq0.d 
|- ( ph -> ( RR _D F ) = ( ( A (,) B ) X. { 0 } ) )
Assertion dveq0 
|- ( ph -> F = ( ( A [,] B ) X. { ( F ` A ) } ) )

Proof

Step Hyp Ref Expression
1 dveq0.a 
 |-  ( ph -> A e. RR )
2 dveq0.b 
 |-  ( ph -> B e. RR )
3 dveq0.c 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
4 dveq0.d 
 |-  ( ph -> ( RR _D F ) = ( ( A (,) B ) X. { 0 } ) )
5 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
6 3 5 syl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
7 6 ffnd 
 |-  ( ph -> F Fn ( A [,] B ) )
8 fvex 
 |-  ( F ` A ) e. _V
9 fnconstg 
 |-  ( ( F ` A ) e. _V -> ( ( A [,] B ) X. { ( F ` A ) } ) Fn ( A [,] B ) )
10 8 9 mp1i 
 |-  ( ph -> ( ( A [,] B ) X. { ( F ` A ) } ) Fn ( A [,] B ) )
11 8 fvconst2 
 |-  ( x e. ( A [,] B ) -> ( ( ( A [,] B ) X. { ( F ` A ) } ) ` x ) = ( F ` A ) )
12 11 adantl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( ( A [,] B ) X. { ( F ` A ) } ) ` x ) = ( F ` A ) )
13 6 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> F : ( A [,] B ) --> CC )
14 1 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
15 14 rexrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR* )
16 2 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
17 16 rexrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
18 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
19 1 2 18 syl2anc 
 |-  ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
20 19 biimpa 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
21 20 simp1d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
22 20 simp2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A <_ x )
23 20 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
24 14 21 16 22 23 letrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A <_ B )
25 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
26 15 17 24 25 syl3anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. ( A [,] B ) )
27 13 26 ffvelrnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` A ) e. CC )
28 6 ffvelrnda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
29 27 28 subcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( F ` A ) - ( F ` x ) ) e. CC )
30 simpr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
31 26 30 jca 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A e. ( A [,] B ) /\ x e. ( A [,] B ) ) )
32 4 dmeqd 
 |-  ( ph -> dom ( RR _D F ) = dom ( ( A (,) B ) X. { 0 } ) )
33 c0ex 
 |-  0 e. _V
34 33 snnz 
 |-  { 0 } =/= (/)
35 dmxp 
 |-  ( { 0 } =/= (/) -> dom ( ( A (,) B ) X. { 0 } ) = ( A (,) B ) )
36 34 35 ax-mp 
 |-  dom ( ( A (,) B ) X. { 0 } ) = ( A (,) B )
37 32 36 eqtrdi 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
38 0red 
 |-  ( ph -> 0 e. RR )
39 4 fveq1d 
 |-  ( ph -> ( ( RR _D F ) ` y ) = ( ( ( A (,) B ) X. { 0 } ) ` y ) )
40 33 fvconst2 
 |-  ( y e. ( A (,) B ) -> ( ( ( A (,) B ) X. { 0 } ) ` y ) = 0 )
41 39 40 sylan9eq 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( RR _D F ) ` y ) = 0 )
42 41 abs00bd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` y ) ) = 0 )
43 0le0 
 |-  0 <_ 0
44 42 43 eqbrtrdi 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` y ) ) <_ 0 )
45 1 2 3 37 38 44 dvlip 
 |-  ( ( ph /\ ( A e. ( A [,] B ) /\ x e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` A ) - ( F ` x ) ) ) <_ ( 0 x. ( abs ` ( A - x ) ) ) )
46 31 45 syldan 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( ( F ` A ) - ( F ` x ) ) ) <_ ( 0 x. ( abs ` ( A - x ) ) ) )
47 14 recnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. CC )
48 21 recnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
49 47 48 subcld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A - x ) e. CC )
50 49 abscld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( A - x ) ) e. RR )
51 50 recnd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( A - x ) ) e. CC )
52 51 mul02d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( 0 x. ( abs ` ( A - x ) ) ) = 0 )
53 46 52 breqtrd 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( ( F ` A ) - ( F ` x ) ) ) <_ 0 )
54 29 absge0d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> 0 <_ ( abs ` ( ( F ` A ) - ( F ` x ) ) ) )
55 29 abscld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( ( F ` A ) - ( F ` x ) ) ) e. RR )
56 0re 
 |-  0 e. RR
57 letri3 
 |-  ( ( ( abs ` ( ( F ` A ) - ( F ` x ) ) ) e. RR /\ 0 e. RR ) -> ( ( abs ` ( ( F ` A ) - ( F ` x ) ) ) = 0 <-> ( ( abs ` ( ( F ` A ) - ( F ` x ) ) ) <_ 0 /\ 0 <_ ( abs ` ( ( F ` A ) - ( F ` x ) ) ) ) ) )
58 55 56 57 sylancl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( abs ` ( ( F ` A ) - ( F ` x ) ) ) = 0 <-> ( ( abs ` ( ( F ` A ) - ( F ` x ) ) ) <_ 0 /\ 0 <_ ( abs ` ( ( F ` A ) - ( F ` x ) ) ) ) ) )
59 53 54 58 mpbir2and 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( ( F ` A ) - ( F ` x ) ) ) = 0 )
60 29 59 abs00d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( F ` A ) - ( F ` x ) ) = 0 )
61 27 28 60 subeq0d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` A ) = ( F ` x ) )
62 12 61 eqtr2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) = ( ( ( A [,] B ) X. { ( F ` A ) } ) ` x ) )
63 7 10 62 eqfnfvd 
 |-  ( ph -> F = ( ( A [,] B ) X. { ( F ` A ) } ) )